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)?
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ábrahám, E.: Building bridges between symbolic computation and satisfiability checking. In: Robertz, D. (ed.) Proceedings ISSAC 2015, pp. 1–6 (2015)
Ábrahám, E., Becker, B., Bigatti, A., Buchberger, B., Cimatti, C., Davenport, J.H., England, M., Fontaine, P., Forrest, S., Kroening, D., Seiler, W., Sturm, T.: SC\(^2\): satisfiability checking meets symbolic computation (project paper). Proc. CICM 2016, 28–43 (2016)
Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Feng, R., Lee, W.-s., Sato, Y. (eds.) Computer Mathematics, pp. 199–221. Springer, Berlin (2014)
Davenport, J.H.: Dataset supporting ’What Does “Without Loss of Generality” Mean (And How Do We Detect It)’. http://doi.org/10.5281/zenodo.305441 (2017)
England, M., Wilson, D.J., Bradford, R., Davenport, J.H.: Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting. Proc. ICMS 2014, 458–465 (2014)
Harrison, J.: Without loss of generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Proceedings Theorem Proving in Higher Order Logics: TPHOLs 2009, pp. 43–59 (2009)
Kutzler, B., Stifter, S.: On the application of Buchberger’s algorithm to automated theorem proving. J. Symb. Comput. 2, 389–397 (1986)
McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. Ph.D. thesis, University of Wisconsin-Madison Computer Science (1984)
Mou, C.: Software library for triangular decompositions. Talk at ICMS 2016 (2016)
McCallum, S., Parusinski, A., Paunescu, L.: Validity proof of Lazard’s method for CAD construction. https://arxiv.org/abs/1607.00264 (2016)
Sakallah, K.A.: Symmetry and satisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chapter 10, pp. 289–338. IOS Press, (2009)
Wang, D.: GEOTHER: A geometry theorem prover. In: Proceedings International Conference on Automated Deduction, pp. 166–170 (1996)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Davenport, J.H. What Does “Without Loss of Generality” Mean, and How Do We Detect It. Math.Comput.Sci. 11, 297–303 (2017). https://doi.org/10.1007/s11786-017-0316-2
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11786-017-0316-2