Abstract
We introduce, through a computational algebraic geometry approach, the automatic reasoning handling of propositions that are simultaneously true over some relevant collections of instances and false over some relevant collections of instances. A rigorous, algorithmic criterion is presented for detecting such cases, and its performance is exemplified through the implementation of this test within the dynamic geometry program GeoGebra. Our framework has some significant differences regarding some alternative, recent formulation of the “true on components” idea; differences and similarities between both approaches are discussed here.
Similar content being viewed by others
Notes
But automatically chosen by the program. Roughly: for free points, both coordinates are added in the set. For constrained points (that is, if the point is defined as an arbitrary element of a line or circle or other one-dimensional path), the first coordinate is set to be free, and the second one is considered dependent.
See https://tinyurl.com/hilbertdim for details. The program code is an implementation of the algorithm DIMENSION_2 in [13, p. 19].
References
Botana, F., Hohenwarter, M., Janičić, J., Kovács, Z., Petrović, I., Recio, T., Weitzhofer, S.: Automated theorem proving in GeoGebra: current achievements. J. Autom. Reason. 55, 39–59 (2015)
Botana, F., Recio, T.: On the unavoidable uncertainty of truth in dynamic geometry proving. Math. Comput. Sci. 10(1), 5–25 (2016)
Chou, S.C.: Mechanical Geometry Theorem Proving. Mathematics and its Applications, vol. 41, D. Reidel Publishing Co., Dordrecht (1988)
Cox, D.A., Little, J., O’Shea, D.: Ideals, varieties, and algorithms. An introduction to computational algebraic geometry and commutative algebra. 4th revised ed. Undergraduate Texts in Mathematics. Springer, Cham (2015)
Dalzotto, G., Recio, T.: On protocols for the automated discovery of theorems in elementary geometry. J. Autom. Reason. 43, 203–236 (2009)
Kovács, Z., Recio, T., Vélez, M.P.: GeoGebra automated reasoning tools: a tutorial. https://github.com/kovzol/gg-art-doc/blob/master/pdf/english.pdf (2018). Accessed 23 March 2018
Montes, A., Recio, T.: Automatic discovery of geometry theorems using minimal canonical comprehensive Gröbner systems. In: Botana, F., Recio, T. (eds.) Proceedings Automated Deduction in Geometry 2006. Lecture Notes on Artificial Intelligence, vol. 4869, pp. 13–138. Springer, Berlin (2007)
Ladra,M., Páez-Guillán, M.P., Recio, T.: Two ways of using Rabinowitsch trick for imposing non-degeneracy conditions. In: Narboux, J., Schreck, P., Streinu I. (eds). Proceedings of ADG 2016: Eleventh International Workshop on Automated Deduction in Geometry, pp. 144–152. Strasbourg (2016). http://icubeweb.unistra.fr/adg2016/index.php/Accueil. Accessed 12 July 2018
Losada, R., Recio, T., Valcarce, J.L.: On the automatic discovery of Steiner–Lehmus generalizations (extended abstract). In: Richter-Gebert, J., Schreck, P. (eds.) Proceedings Automated Deduction in Geometry 2010, pp. 171–174. Munich (2010)
Recio, T.: Cálculo Simbólico y Geométrico. Editorial Síntesis, Madrid (1998)
Recio, T., Sterk, H., Vélez, M.P.: Automatic geometry theorem proving. In: Cohen, A.M., Cuipers, H., Sterk, H. (eds.) Some Tapas of Computer Algebra, Algorithms and Computations in Mathematics 4, pp. 276–291. Springer, Berlin (1998)
Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63–82 (1999)
Winkler, F.: Gröbner Bases – Theory and Applications. 5th SCIEnce Training School in Symbolic Computation. RISC, Univ. Linz, 28.6.–9.7.2010. https://www.risc.jku.at/projects/science/school/fifth/materials/GB.pdf (2010). Accessed 23 July 2018
Zariski, O., Samuel, P.: Commutative Algebra, Vol. 2. Graduate Text in Mathematics 29. Springer, Berlin (1960)
Zhou, J., Wang, D., Sun, Y.: Automated reducible geometric theorem proving and discovery by Gröbner basis method. J. Autom. Reason. 59(3), 331–344 (2017)
Author information
Authors and Affiliations
Corresponding author
Additional information
Partially supported by the Spanish Research Project MTM2017-88796-P.
Rights and permissions
About this article
Cite this article
Kovács, Z., Recio, T. & Vélez, M.P. Detecting truth, just on parts. Rev Mat Complut 32, 451–474 (2019). https://doi.org/10.1007/s13163-018-0286-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s13163-018-0286-1
Keywords
- Automatic deduction in geometry, automatic geometry theorem proving
- Automatic geometry theorem discovery
- Elementary geometry
- Gröbner basis
- Zero divisor
- True on parts, false on parts
- True on components
- Dynamic geometry