Abstract
When one goes from a geometrical statement to an algebraic statement, the
immediate translation is to replace every point by a pair of coordinates, if in the plane (or more as required). A statement with N points is then a statement with 2N (or 3N or more) variables, and the complexity of tools like cylindrical algebraic decomposition is doubly exponential in the number of variables. Hence one says "without loss of generality, A is at (0,0)" and so on.
How might one automate this, in particular the detection that a "without loss of generality" argument is possible, or turn it into a procedure (and possibly even a
formal proof)?
immediate translation is to replace every point by a pair of coordinates, if in the plane (or more as required). A statement with N points is then a statement with 2N (or 3N or more) variables, and the complexity of tools like cylindrical algebraic decomposition is doubly exponential in the number of variables. Hence one says "without loss of generality, A is at (0,0)" and so on.
How might one automate this, in particular the detection that a "without loss of generality" argument is possible, or turn it into a procedure (and possibly even a
formal proof)?
Original language  English 

Pages (fromto)  297303 
Journal  Mathematics in Computer Science 
Volume  11 
Issue number  34 
Early online date  25 Apr 2017 
DOIs  
Publication status  Epub ahead of print  25 Apr 2017 
Bibliographical note
Based on a presentation at ACA 2016 and at SYNASC 2016Keywords
 Symmetry; Generality; Cylindrical Algebraic Decomposition
Fingerprint
Dive into the research topics of 'What does “without loss of generality” mean, and how do we detect it'. Together they form a unique fingerprint.Datasets

Dataset supporting 'What Does "Without Loss of Generality" Mean (And How Do We Detect It)'
Davenport, J. (Creator), University of Bath, Mar 2017
Dataset