×

Automated theorem proving in GeoGebra: current achievements. (English) Zbl 1356.68181

Summary: 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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
97Gxx Geometry education
97U70 Technological tools, calculators (aspects of mathematics education)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s Elements. Rev. Symb. Log. 2(4), 700-768 (2009) · Zbl 1188.03008
[2] Baulac, Y., Bellemain, F., Laborde, J.M.: Cabri Geometry II. Dallas, Texas Instruments (1994)
[3] 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)
[4] Bertot, Y., Guilhot, F., Pottier, L.: Visualizing geometrical statements with GeoView. Electr. Notes Theor. Comput. Sci. 103, 49-65 (2004)
[5] 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) · Zbl 0629.68087
[6] 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) · Zbl 0629.68087
[7] Botana, F., Valcarce, J.: A dynamic symbolic interface for geometric theorem discovery. Comput. Educ. 38, 21-35 (2002)
[8] Buchberger, B. In: Rice, J.R. (ed.) : Applications of Gröbner Bases in Non-Linear Computational Geometry, pp 59-87. Springer, New York (1987)
[9] Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht (1988) · Zbl 0661.14037
[10] 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)
[11] Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994) · Zbl 0941.68503
[12] 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) · Zbl 0865.68110
[13] 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) · Zbl 1412.68214
[14] Chou S.C., Gao X.S.: Automated reasoning in geometry. In: Handbook of Automated Reasoning. Elsevier, and MIT Press (2001) · Zbl 1011.68128
[15] Coelho, H., Moniz-Pereira, M.: Automated reasoning in geometry theorem proving with Prolog (1986). J. Autom. Reason. 2, 329-390 (1986) · Zbl 0642.68161
[16] CoCoATeam: CoCoA: A system for doing Computations in Commutative Algebra. Retrieved 02.09.13, from http://cocoa.dima.unige.it (2012) · Zbl 1131.68094
[17] 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)
[18] 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) · Zbl 0941.03010
[19] 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)
[20] DeVilliers, M.: Rethinking Proof with Sketchpad. Key Curriculum Press. Retrieved 02.02.13, from, http://mzone.mweb.co.za/residents/profmd/proof.pdf (1999)
[21] 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) · Zbl 1202.68378
[22] 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) · Zbl 0092.13402
[23] Gressier, J.: Geometrix IV. Retrieved 06.08.13, from, http://geometrix.free.fr (2013)
[24] 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) · Zbl 1278.68279
[25] Hanna, G.: The ongoing value of proof. J. Math. Didaktik 18(2), 171-185 (1997)
[26] Hohenwarter, M.: Ein Softwaresystem für dynamische Geometrie und Algebra der Ebene, master thesis. Paris Lodron University, Salzburg (2002)
[27] 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)
[28] Jackiw, N.R.: The Geometer’s Sketchpad, v3.0. Key Curriculum Press, Berkeley, CA (1995)
[29] Janičić, P.: Geometry constructions language. J. Autom. Reason. 44(1-2), 3-24 (2010) · Zbl 1185.68626
[30] Janičić, P., Narboux, J., Quaresma, P.: The area method: a recapitulation. J. Autom. Reason. 48(4), 489-532 (2012) · Zbl 1242.68281
[31] Kapur, D.: Using Gröbner bases to reason about geometry problems. J. Symb. Comput. 2(4), 399-408 (1986) · Zbl 0629.68087
[32] Kortenkamp, U.: Foundations of Dynamic Geometry. Ph.D. Dissertation, ETH, Zurich (1999)
[33] Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Workshop on Mathematical User Interfaces (2004) · Zbl 1188.03008
[34] 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)
[35] 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)
[36] 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) · Zbl 1434.68708
[37] 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)
[38] Luengo, V.: Cabri-Euclide: Un micromonde de Preuve intégrant la réfutation, PhD thesis. Université Joseph Fourier, Grenoble (1997)
[39] 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.htmlhttp://www.freepatentsonline.com/article/Electronic-Journal-Mathematics-Technology/270980194.html (2011) · Zbl 1182.68272
[40] 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)
[41] Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reason. 39(2), 161-180 (2007) · Zbl 1131.68094
[42] 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) · Zbl 1131.68094
[43] 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)
[44] 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 · Zbl 1278.68279
[45] Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63-82 (1999) · Zbl 0941.03010
[46] Schwartz, J. L., Yerushalmy, M.: The Geometric Supposer. Sunburst Communications, Pleasantville, NY (1983)
[47] 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)
[48] 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)
[49] The GeoGebra Team: Reference: Command Line Arguments — GeoGebraWiki (2015) [ http://wiki.geogebra.org/en/Reference:Command_Line_Arguments]
[50] 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) · Zbl 1202.68390
[51] 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) · Zbl 1202.68390
[52] Weitzhofer, S: Mechanic Proving of Theorems in Plane Geometry. Johannes Kepler University, Linz, Austria (2013). http://test.geogebra.org/∼kovzol/guests/SimonWeitzhofer/DiplArbeit.pdf
[53] Wilson, S., Fleuriot, J.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In: Workshop on User Interfaces for Theorem Provers (UITP) (2005) · Zbl 1242.68281
[54] Wolfram Research, Inc.: Mathematica, Version 3.0. Champaign, IL (1996)
[55] Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Sci. Sin. 21, 157-179 (1978)
[56] 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) · Zbl 1182.68272
[57] 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) · Zbl 1302.68247
[58] Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry. J. Autom. Reason. 45(3), 213-241 (2010) · Zbl 1211.68372
[59] Zhang, J.Z., Yang, L., Deng, M.: The parallel numerical method of mechanical theorem proving. Theor. Comput. Sci. 74(3), 253-271 (1990) · Zbl 0701.68087
[60] 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) · Zbl 1350.68246
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.