Session A2 - Computational Algebraic Geometry
July 11, 17:00 ~ 17:25 - Room B5
Automated Reasoning Tools in GeoGebra
Universidad de Cantabria, Spain - firstname.lastname@example.org
GeoGebra (see Hohenwarter, 2002) is a dynamic geometry software with tenths of millions users worldwide. Despite its original merely graphical flavor, successful attempts were performed during the last years towards combining standard dynamic geometry approaches with automated reasoning methods using computer algebra tools. Since Automated Theorem Proving (ATP) in geometry has reached a rather mature stage, an Austro-Spanish group (see Botana & al., 2015) started in 2010 a project of incorporating and testing a number of different automated geometry provers in GeoGebra. This collaboration was built upon previous approaches and achievements of a large community of researches, involving different techniques from algebraic geometry and computer algebra. Moreover, various symbolic computation, open source, packages have been involved, most importantly the Singular (Decker & al., 2012) and the Giac (Parisse, 2013) computer algebra systems. See Kovács, 2015a and Kovács, 2015b for a more detailed overview. As a result of this collaboration, we have been able to recently announce the implementation (Abanades et. al. 2016) of three automated reasoning tools (ART) in GeoGebra, all of them working in the desktop, web, tablet or smartphone versions of GeoGebra: the automated derivation of (numerical) properties in a given construction, by means of the Relation Tool; the verification of the symbolic truth of these properties, by means of the Prove and ProveDetails tools; and the discovery of missing hypotheses for a conjectural statement to hold true, through the LocusEquation tool. The Relation Tool, in its original form, allows selecting two geometrical objects in a construction, and then to check for typical relations among them, including perpendicularity, parallelism, equality or incidence. Finally, it shows a message box with the obtained information (yes/no the relation holds). GeoGebra version 5 now displays an extra button in the message box with the caption “More...” which results in some symbolic computations when pressed. That is, by pressing the “More...” button, GeoGebra's Automatic Theorem Proving subsystem starts and selects (by some heuristics) an appropriate prover method to decide if the numerically obtained property is indeed absolutely true in general. The current version of GeoGebra is capable of choosing a) the Gröbner basis method, b) Wu's characteristic method, c) the area method, or d) sufficient number of exact checks, deterministic method (see Kovacs et. al. 2012, Weitzhofer, 2013), as the underlying ATP technique addressed by the Prove command. See Kovacs 2015b for more details on this portfolio prover. Moreover, if the conjectured relation does not (mathematically speaking) hold, the first two methods can determine some geometrical extra-conditions, which need to hold true in order to make the given statement generally correct, either using the ProveDetails tool (in the generally true case) or the LocusEquation tool (in the generally false case). In the talk I will outline, through examples, some features of the ART in GeoGebra, providing some details on the underlying algebraic methods and reporting on our current work-in-progress concerning this topic.
Acknowledgement: Partially supported by the Spanish Ministerio de Economía y Competitividad and by the European Regional Development Fund (ERDF), under the Project MTM2014-54141-P.
References: 1) Abánades, M.A., Botana, F., Kovács, Z., Recio, T., & Sólyom-Gecse, C. (2016). Development of automatic reasoning tools in GeoGebra. In: ACM Communications in Computer Algebra 50(3):85-88, November 2016. 2) Botana, F., Hohenwarter, M., Janicic, P., Kovács Z., Petrovic, I., Recio, T., Weitzhofer, S. (2015). Automated theorem proving in GeoGebra: current achievements. Journal of Automated Reasoning (Vol. 5, Number 1, pp. 39-59). 3) Decker, W., Greuel, G.M., Pfister, G. & Schönemann, H. (2012). Singular 3-1-6 –A computer algebra system for polynomial computations. http://www.singular.uni-kl.de 4) Hohenwarter, M. (2002). Ein Softwaresystem für dynamische Geometrie und Algebra der Ebene. Master’s thesis. Salzburg: Paris Lodron University. 5) Kovács, S., Recio, T., Weitzhofer, S. (2012): Implementing theorem proving in GeoGebra by exact check of a statement in a bounded number of test cases. In: Proceedings EACA 2012, Libro de Resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones. Universidad de Alcalá, pp. 123–126. 6) Kovács, Z. (2015a). Computer based conjectures and proofs. Dissertation. Linz: Johannes Kepler University. 7) Kovács, Z. (2015b). The Relation Tool in GeoGebra 5. In Botana, F., Quaresma, P. (Eds.), Post-conference Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), 9-11 July 2014, Lecture Notes in Artificial Intelligence 9201 (pp. 53-71). Springer. 8) Parisse, B. (2013). Giac/Xcas, a free computer algebra system. Available at http://www-fourier.ujf-grenoble.fr/~parisse/giac.html 9)Weitzhofer, S. (2013): Mechanic proving of theorems in plane geometry. Master’s thesis, Johannes Kepler University, Linz, Austria. http://test.geogebra.org/~kovzol/guests/SimonWeitzhofer/DiplArbeit.pdf