Abstract
GeoGebra is an open-source educational mathematics software tool, with millions of users worldwide. It has a number of features (integration of computer algebra, dynamic geometry, spreadsheet, etc.), primarily focused on facilitating student experiments, and not on formal reasoning. Since including automated deduction tools in GeoGebra could bring a whole new range of teaching and learning scenarios, and since automated theorem proving and discovery in geometry has reached a rather mature stage, we embarked on a project of incorporating and testing a number of different automated provers for geometry in GeoGebra. In this paper, we present the current achievements and status of this project, and discuss various relevant challenges that this project raises in the educational, mathematical and software contexts. We will describe, first, the recent and forthcoming changes demanded by our project, regarding the implementation and the user interface of GeoGebra. Then we present our vision of the educational scenarios that could be supported by automated reasoning features, and how teachers and students could benefit from the present work. In fact, current performance of GeoGebra, extended with automated deduction tools, is already very promising—many complex theorems can be proved in less than 1 second. Thus, we believe that many new and exciting ways of using GeoGebra in the classroom are on their way.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s Elements. Rev. Symb. Log. 2(4), 700–768 (2009)
Baulac, Y., Bellemain, F., Laborde, J.M.: Cabri Geometry II. Dallas, Texas Instruments (1994)
Bernat, P.: Using dynamic geometry environments for problem solving: CHYPRE: an interactive environment for elementary geometry problem solving. Abstract of a presentation at The 8th International Congress on Math Education (ICME 8). Retrieved 06.08.13, from, http://mathforum.org/mathed/seville/bernat/abst∖_bernat.html. Seville (1996)
Bertot, Y., Guilhot, F., Pottier, L.: Visualizing geometrical statements with GeoView. Electr. Notes Theor. Comput. Sci. 103, 49–65 (2004)
Botana F., Kovács, Z., Recio, T., Weitzhofer, S.: Implementing theorem proving in GeoGebra by using a Singular webservice, or by exact check of a statement in a bounded number of test cases, http://ggb1.idm.jku.at/∼kovzol/talks/eaca12/EACA2012-BotanaKovacsRecioWeitzhofer.pdf (2012)
Botana, F., Kovács, Z., Weitzhofer, S.: Implementing theorem proving in GeoGebra by using a Singular webservice. In: Proceedings EACA 2012. Libro de Resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones, pp 67–70. Alcalá de Henáres, Universidad de Alcalá (2012)
Botana, F., Valcarce, J.: A dynamic symbolic interface for geometric theorem discovery. Comput. Educ. 38, 21–35 (2002)
Buchberger, B. In: Rice, J.R. (ed.) : Applications of Gröbner Bases in Non-Linear Computational Geometry, pp 59–87. Springer, New York (1987)
Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht (1988)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated production of traditional proofs for constructive geometry theorems. In: Vardi, M. (ed.) Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (LICS), pp 48–56. IEEE Computer Society Press (1993)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)
Chou, S.C., Gao, X.S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants (II). Theorem proving with full-angles. J. Autom. Reason. 17, 349–370 (1996)
Chou, S.C., Gao, X.S., Zhang, J.Z.: An introduction to Geometry Expert. In: McRobbie, M. A., Slaney, J. K. (eds.) CADE 13, volume 1104 of Lecture Notes in Artificial Intelligence. Springer-Verlag (1996)
Chou S.C., Gao X.S.: Automated reasoning in geometry. In: Handbook of Automated Reasoning. Elsevier, and MIT Press (2001)
Coelho, H., Moniz-Pereira, M.: Automated reasoning in geometry theorem proving with Prolog (1986). J. Autom. Reason. 2, 329–390 (1986)
CoCoATeam: CoCoA: A system for doing Computations in Commutative Algebra. Retrieved 02.09.13, from http://cocoa.dima.unige.it (2012)
Cox, D., Little, J., O’Shea, D.: Ideals, Varieties and Algorithms. An Introduction to Computational Algebraic Geometry and Commutative Algebra (Undergraduate Texts in Mathematics). Springer-Verlag, Secaucus, NJ (2008)
Decker, W., Greuel, G.-M., Pfister, G., Schönemann, H.: Singular 3-1-6 — A Computer Algebra System for Polynomial Computations. Retrieved 02.09.13, from, http://www.singular.uni-kl.de (2012)
Desfontaines, D.: Theorem proving in GeoGebra: Implementing the Area Method into OpenGeoProver (Internship report). Retrieved 02.02.13, from, http://www.eleves.ens.fr/home/desfonta/InternshipReport-v2.pdf (2012)
DeVilliers, M.: Rethinking Proof with Sketchpad. Key Curriculum Press. Retrieved 02.02.13, from, http://mzone.mweb.co.za/residents/profmd/proof.pdf (1999)
Gao, X.S., Lin, Q.: MMP/Geometer a software package for automated geometric reasoning. In: Winkler, F. (ed.) Automated Deduction in Geometry: 4th International Workshop, (ADG 2002), volume 2930 of Lecture Notes in Computer Science, 44–66. Springer-Verlag (2004)
Gelernter, H.: Realisation of a geometry-proving machine. In: Proceedings of the International Conference on Information Processing, 273–282, Paris, vol. 15-20, p 1959 (1959)
Gressier, J.: Geometrix IV. Retrieved 06.08.13, from, http://geometrix.free.fr (2013)
Hanna, G., Jahnke, H.N.: Proofs and proving. In: A.J. Bishop A.J., Clements K., Keitel C., Kilpatrick J., Laborde C. (eds.) International Handbook of Mathematics Education, Part Two, pp 877–908. Kluwer Academic Publishers, Dordrecht (1996)
Hanna, G.: The ongoing value of proof. J. Math. Didaktik 18(2), 171–185 (1997)
Hohenwarter, M.: Ein Softwaresystem für dynamische Geometrie und Algebra der Ebene, master thesis. Paris Lodron University, Salzburg (2002)
Isotani, S., Brandão, L. O.: An algorithm for automatic checking of exercises in a dynamic geometry system: iGeom. Comput. Educ. 51, 1283–1303 (2008)
Jackiw, N.R.: The Geometer’s Sketchpad, v3.0. Key Curriculum Press, Berkeley, CA (1995)
Janičić, P.: Geometry constructions language. J. Autom. Reason. 44(1-2), 3–24 (2010)
Janičić, P., Narboux, J., Quaresma, P.: The area method: a recapitulation. J. Autom. Reason. 48(4), 489–532 (2012)
Kapur, D.: Using Gröbner bases to reason about geometry problems. J. Symb. Comput. 2(4), 399–408 (1986)
Kortenkamp, U.: Foundations of Dynamic Geometry. Ph.D. Dissertation, ETH, Zurich (1999)
Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Workshop on Mathematical User Interfaces (2004)
Kovács, Z., Recio, T., Weitzhofer, S.: 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, pp 123–126. Alcalá de Henáres, Universidad de Alcalá (2012)
Kovács, Z., Weitzhofer, S., Desfontaines, D., Janičić, P.: Test cases for benchmarking statements. Retrieved 11.09.12, from, https://dev.geogebra.org/trac/browser/trunk/geogebra/test/scripts/benchmark/prover (2012)
Kovács, Z., Parisse, B.: Giac and GeoGebra — improved Gröbner basis computations, Special Semester on Applications of Algebra and Number Theory, Workshop 3 on Computer Algebra and Polynomials. Retrieved 18.10.14, from, https://www.ricam.oeaw.ac.at/specsem/specsem2013/workshop3/slides/parisse-kovacs.pdf (2013)
Kovács, Z.: Prover benchmark for GeoGebra 5.0.14.0. Retrieved 10.09.14, from, http://test.geogebra.org/∼kovzol/data/Prove-20150219/ (2014)
Luengo, V.: Cabri-Euclide: Un micromonde de Preuve intégrant la réfutation, PhD thesis. Université Joseph Fourier, Grenoble (1997)
Magajna, Z.: An observation tool as an aid for building proofs. Electronic J. of Mathematics and Technology 5/3. Retrieved 02.02.13, from, http://www.freepatentsonline.com/article/Electronic-Journal-Mathematics-Technology/270980194.html http://www.freepatentsonline.com/article/Electronic-Journal-Mathematics-Technology/270980194.html (2011)
Marić, F., Petrović, I., Petrović, D., Janičić, P.: Formalization and implementation of algebraic methods in geometry. Electron. Proc. Theor. Comput. Sci. 79, 63–81 (2011)
Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reason. 39(2), 161–180 (2007)
Narboux, J.: Geoproof, a user interface for formal proofs in geometry. In: Mathematical User-Interfaces Workshop, Schloss Hagenberg, Linz, Austria. Electronic proceedings at http://www.activemath.org/workshops/MathUI/07/proceedings/Narboux-Geoproof-MathUI07.html (2007)
Nikolić, M., Marić, F., Janičić, P.: Instance-based selection of policies for SAT Solvers. In: Theory and Applications of Satisfiability Testing – SAT 2009, volume 5584 of Lecture Notes in Computer Science, pp 326–340. Springer-Verlag (2009)
Quaresma, P., Janičić, P.: GeoThms — a web system for euclidean constructive geometry. Electron. Notes Theor. Comput. Sci. (ENTCS) 174(2), 35–48 (2007). 10.1016/j.entcs.2006.09.020
Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63–82 (1999)
Schwartz, J. L., Yerushalmy, M.: The Geometric Supposer. Sunburst Communications, Pleasantville, NY (1983)
Sutherland, I.E.: Sketchpad: A Man-Machine Graphical Communication System, Lincoln Laboratory, Massachusetts Institute of Technology via Defense Technical Information Center, Technical Report No. 296. Lexington, MA. Retrieved 02.02.13, from, http://handle.dtic.mil/100.2/AD404549 (1963)
Tall, D.: Cognitive development, representations and proof. In: Proceedings of the conference Justifying and Proving in School Mathematics, pp 27–38. Institute of Education, London (1995)
The GeoGebra Team: Reference: Command Line Arguments — GeoGebraWiki (2015) [ http://wiki.geogebra.org/en/Reference:Command_Line_Arguments]
Wang, D.: Geother 1.1: Handling and proving geometric theorems automatically. In: Automated Deduction in Geometry, volume 2930 of Lecture Notes in Artificial Intelligence, pp 194–215. Springer-Verlag (2004)
Wang, D.: Elimination Practice: Software Tools and Applications. London: Imperial College Press. Geother 1.1: Handling and proving geometric theorems automatically. In: Automated Deduction in Geometry, volume 2930 of Lecture Notes in Artificial Intelligence, pp 194–215. Springer-Verlag (2004)
Weitzhofer, S: Mechanic Proving of Theorems in Plane Geometry. Johannes Kepler University, Linz, Austria (2013). http://test.geogebra.org/∼kovzol/guests/SimonWeitzhofer/DiplArbeit.pdf
Wilson, S., Fleuriot, J.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In: Workshop on User Interfaces for Theorem Provers (UITP) (2005)
Wolfram Research, Inc.: Mathematica, Version 3.0. Champaign, IL (1996)
Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Sci. Sin. 21, 157–179 (1978)
Xu, L., Hutter, F., Hoos, H. H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. (JAIR) 32, 565–606 (2008)
Ye, Z., Chou S.C., Gao, X.S.: An Introduction to Java Geometry Expert. In: Automated Deduction in Geometry, 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008, Revised Papers, volume 6301 of Lecture Notes in Computer Science, pp 189–195. Springer-Verlag (2011)
Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry. J. Autom. Reason. 45(3), 213–241 (2010)
Zhang, J.Z., Yang, L., Deng, M.: The parallel numerical method of mechanical theorem proving. Theor. Comput. Sci. 74(3), 253–271 (1990)
Zou, Y., Zhang, J.Z.: Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method. In: Lecture Notes in Computer Science, Volume 6877, Automated Deduction in Geometry, 221–258 (2011)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Botana, F., Hohenwarter, M., Janičić, P. et al. Automated Theorem Proving in GeoGebra: Current Achievements. J Autom Reasoning 55, 39–59 (2015). https://doi.org/10.1007/s10817-015-9326-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9326-4