zbMATH — the first resource for mathematics

What does “without loss of generality” mean, and how do we detect it. (English) Zbl 1425.68464
Summary: 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)?

68W30 Symbolic computation and algebraic computation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Ábrahám, E.: Building bridges between symbolic computation and satisfiability checking. In: Robertz, D. (ed.) Proceedings ISSAC 2015, pp. 1-6 (2015) · Zbl 1344.68198
[2] Ábrahám, E; Becker, B; Bigatti, A; Buchberger, B; Cimatti, C; Davenport, JH; 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) · Zbl 1344.68198
[3] 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) · Zbl 1352.68291
[4] 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) · Zbl 1425.68464
[5] England, M; Wilson, DJ; Bradford, R; Davenport, JH, Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting, Proc. ICMS, 2014, 458-465, (2014) · Zbl 1437.14008
[6] 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) · Zbl 1252.68254
[7] Kutzler, B; Stifter, S, On the application of buchberger’s algorithm to automated theorem proving, J. Symb. Comput., 2, 389-397, (1986) · Zbl 0629.68086
[8] McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. Ph.D. thesis, University of Wisconsin-Madison Computer Science (1984) · Zbl 0900.68279
[9] Mou, C.: Software library for triangular decompositions. Talk at ICMS 2016 (2016)
[10] McCallum, S., Parusinski, A., Paunescu, L.: Validity proof of Lazard’s method for CAD construction. https://arxiv.org/abs/1607.00264 (2016) · Zbl 0629.68086
[11] 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)
[12] Wang, D.: GEOTHER: A geometry theorem prover. In: Proceedings International Conference on Automated Deduction, pp. 166-170 (1996) · Zbl 1412.68266
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.