Skip to main content

Using Automated Reasoning Tools to Explore Geometric Statements and Conjectures

  • Chapter
  • First Online:
Proof Technology in Mathematics Research and Teaching

Part of the book series: Mathematics Education in the Digital Era ((MEDE,volume 14))

Abstract

GeoGebra, a very popular software tool for dynamic mathematics, has recently been extended with an automated reasoning tool (ART). A description of the ART features and some examples and reflections regarding its prospective use in the classroom are the main goals of this chapter. ART is based on automatically algebraizing a given geometric construction and then applying effective algebraic geometry tools. This robust approach has already been implemented in several programs but never, until now, with the ability to merge features of dynamic geometry and computer algebra, address non-experts, and achieve worldwide dissemination in the educational community. GeoGebra’s automatic reasoning tools allow, through the Relation command, the automatic finding of geometric conjectures and the verification or denial of these conjectures. Moreover, if the conjecture fails, GeoGebra might suggest (by means of the LocusEquation command) some extra hypotheses, in order to turn true, if suitably modified, the given statement. We argue and exemplify how these tools can be considered potentially useful in a technology-mediated educational framework, where GeoGebra could play the role of a mentor, helping students both to foster their creativity with the discovery of new geometric facts and to develop their own explanations on the truth of these facts. We conclude with some reflections on the challenges that could arise from the popularization of this new technology in mathematics education.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://en.wikipedia.org/wiki/Computer_algebra_system.

  2. 2.

    Notice that, according to the syntax of GeoGebra, the equation sign must be entered twice; this information is available in the GeoGebra Help or in Kovács (2017), but should also be remarked by the teacher in Step 0 (a).

References

  • Abánades, M., Botana, F., Kovács, Z., Recio, T., & Sólyom-Gecse, C. (2016a). Towards the automatic discovery of theorems in GeoGebra. In G. M. Greuel, T. Koch, P. Paule, & A. Sommese (Eds.), Mathematical Software—ICMS 2016. 5th International Conference, Berlin, Germany, July 11–14, 2016, Proceedings. Volume 9725 of Lecture Notes in Computer Science (pp. 37–42). Cham: Springer International Publishing.

    Google Scholar 

  • Abánades, M., Botana, F., Kovács, Z., Recio, T., & Sólyom-Gecse, C. (2016b). Development of automatic reasoning tools in GeoGebra. ACM Communications in Computer Algebra, 50, 85–88.

    Google Scholar 

  • Artigue, M. (2012). What is inquiry-based mathematics education (IBME)? In M. Artigue & P. Baptist (Eds.), Inquiry in mathematics education (pp. 3–13). Fibonacci Project.

    Google Scholar 

  • Balacheff, N. (1997). ICME 8, TG19 followup report. Computer-Based Learning Environments: “CBILE”. http://mathforum.org/mathed/seville/followup.html.

  • Baulac, Y., Bellemain, F., & Laborde, J. M. (1994). Cabri geometry II. Dallas: Texas Instruments.

    Google Scholar 

  • Botana, F., & Kovács, Z. (2016). New tools in GeoGebra offering novel opportunities to teach loci and envelopes. arXiv:1605.09153.

  • Botana, F., & Valcarce, J. L. (2002). A dynamic-symbolic interface for geometric theorem discovery. Computers and Education, 38, 21–35.

    Google Scholar 

  • Botana, F., Hohenwarter, M., Janičić, P., Kovács, Z., Petrović, I., Recio, T., et al. (2015). Automated theorem proving in GeoGebra: Current achievements. Journal of Automated Reasoning, 55, 39–59.

    Article  Google Scholar 

  • Buchberger, B., & The Theorema Working Group. (1998). Theorema: Theorem proving for the masses using Mathematica. In Invited Talk at the Worldwide Mathematica Conference, Chicago, June 18–21, 1998.

    Google Scholar 

  • Chou, S. C. (1987). Mechanical geometry theorem proving. Springer Science+Business Media.

    Google Scholar 

  • Corless, R. M. (2004). Computer-mediated thinking. http://www.apmaths.uwo.ca/~rcorless/frames/PAPERS/EDUC/CMTpaper.pdf.

  • Corpuz, J. (2017). Best math apps. https://www.tomsguide.com/us/pictures-story/1300-best-math-apps.html.

  • Davis, P. (1995, March). The rise, fall, and possible transfiguration of triangle geometry: A mini-history. The American Mathematical Monthly, 102, 204–214.

    Article  Google Scholar 

  • de Villiers, M. (1999). Rethink proof with sketchpad. Emeryville: Key Curriculum Press.

    Google Scholar 

  • de Villiers, M. (1990). The role and function of proof in mathematics. Pythagoras, 24, 17–24.

    Google Scholar 

  • Foster, C. (2013). Mathematical études: Embedding opportunities for developing procedural fluency within rich mathematical contexts. International Journal of Mathematical Education in Science and Technology, 55, 765–774.

    Article  Google Scholar 

  • Gelernter, H. (1959). Realisation of a geometry-proving machine. In Proceedings of the International Conference on Information Processing, Paris, June 15–20, 1959 (pp. 273–282).

    Google Scholar 

  • Halmos, P. R. (1982). A Hilbert space problem book (2nd ed.). New York, Heidelberg, Berlin: Springer.

    Google Scholar 

  • Hanna, G. (1995). Challenges to the importance of proof. For the Learning of Mathematics, 15, 42–49.

    Google Scholar 

  • Hašek, R., Kovács, Z., & Zahradník, J. (2017). Contemporary interpretation of a historical locus problem with the use of computer algebra. In I. S. Kotsireas & E. Martínez-Moro (Eds.), Applications of Computer Algebra: Kalamata, Greece, July 20–23, 2015. Volume 198 of Springer Proceedings in Mathematics & Statistics. Springer.

    Google Scholar 

  • Hohenwarter, M. (2002). GeoGebra: Ein Softwaresystem für dynamische Geometrie und Algebra der Ebene. Master’s thesis, Paris Lodron University, Salzburg, Austria.

    Google Scholar 

  • Hohenwarter, M., Kovács, Z., & Recio, T. (2017). Deciding geometric properties symbolically in GeoGebra. In R&E-SOURCE (2017) Special Issue #6: 13th International Congress on Mathematical Education (ICME-13).

    Google Scholar 

  • Howson, G., & Wilson, B. (1986). ICMI Study Series: School mathematics in the 1990s. Kuwait: Cambridge University Press.

    Google Scholar 

  • Jackiw, N. R. (1995). The Geometer’s Sketchpad, v3.0. Berkeley, CA: Key Curriculum Press.

    Google Scholar 

  • Jaworski, B. (1994). Investigating mathematics teaching: A constructivist enquiry. Studies in Mathematics Education Series: 5. The Falmer Press.

    Google Scholar 

  • Jones, P. L. (1996). Handheld technology and mathematics: Towards the intelligent partnership (pp. 87–96). http://ued.uniandes.edu.co/roless-calc.html.

  • Kapur, D. (1986). Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation, 2, 399–408.

    Article  Google Scholar 

  • Kortenkamp, U. (1999). Foundations of dynamic geometry. Ph.D. thesis, ETH Zürich.

    Google Scholar 

  • Kovács, Z. (2015). Computer based conjectures and proofs in teaching Euclidean geometry. Ph.D. thesis, Johannes Kepler University, Linz.

    Google Scholar 

  • Kovács, Z. (2017). Real-time animated dynamic geometry in the classrooms by using fast Gröbner basis computations. Mathematics in Computer Science, 11.

    Article  Google Scholar 

  • Kovács, Z. (2018). Automated reasoning tools in GeoGebra: A new approach for experiments in planar geometry. South Bohemia Mathematical Letters, 25.

    Google Scholar 

  • Kovács, Z., & Parisse, B. (2015) Giac and GeoGebra—Improved Gröbner basis computations. In J. Gutierrez, J. Schicho, & M. Weimann (Eds.), Computer algebra and polynomials. Lecture Notes in Computer Science (pp. 126–138). Springer.

    Google Scholar 

  • Kovács, Z., & Schiffler, K. (2017). Unterstützung des Mathematikunterrichts mit automatischem Beweisen mit GeoGebra. In: PH forscht II, Linz, Austria.

    Google Scholar 

  • Kovács, Z., & Vajda, R. (2017). A note about Euler’s inequality and automated reasoning with dynamic geometry. arXiv:1708.02993v2.

  • Kovács, Z., Recio, T., & Vélez, M. P. (2017). gg-art-doc (GeoGebra Automated Reasoning Tools. A tutorial). A GitHub project. https://github.com/kovzol/gg-art-doc.

  • Kovács, Z., Recio, T., Richard, P. R., & Vélez, M. P. (2017). GeoGebra automated reasoning tools: A tutorial with examples. In G. Aldon & J. Trgalova (Eds.), Proceedings of the 13th International Conference on Technology in Mathematics Teaching. (pp. 400–404). https://hal.archives-ouvertes.fr/hal-01632970.

  • Krause, E. F. (1975). Taxicab geometry: An adventure in non-Euclidean geometry. Addison-Wesley.

    Google Scholar 

  • Kutzler, B., & Stifter, S. (1986). On the application of Buchberger’s algorithm to automated geometry theorem proving. Journal of Symbolic Computation, 2, 389–397.

    Article  Google Scholar 

  • Lin, F. L., Yang, K. L., Lee, K. H., Tabach, M., & Stylianides, G. (2012). Principles of task design for conjecturing and proving. In G. Hanna & M. de Villiers (Eds.), Proof and Proving in Mathematics Education. The 19th ICMI Study (pp. 305–326). Springer.

    Google Scholar 

  • Lindenbauer, E., & Reichenberger, S. (2015). Voronoi-Diagramme. GeoGebra Materials. https://www.geogebra.org/m/sAaFMcTA.

  • Losada, R. (2014). El color dinámico en GeoGebra. La Gaceta de la Real Sociedad Matemática Española, 17(3), 525–547.

    Google Scholar 

  • Losada, R., Recio, T., & Valcarce, J. L. (2011). Equal bisectors at a vertex of a triangle. In B. Murgante, O. Gervasi, A. Iglesias, D. Taniar, & B. Apduhan (Eds.), Computational Science and Its Applications—ICCSA 2011. Lecture Notes in Computer Science (Vol. 6785, pp. 328–341). Berlin, Heidelberg: Springer.

    Google Scholar 

  • Martinovic, D., & Manizade, A. G. (2014). Technology as a partner in the geometry classrooms. The Electronic Journal of Mathematics and Technology, 8, 69–87.

    Google Scholar 

  • Martinovic, D., Muller, E., & Buteau, C. (2013). Intelligent partnership with technology: Moving from a math school curriculum to an undergraduate program. Comput. Schools, 30, 76–101.

    Article  Google Scholar 

  • Oldenburg, R. (2008). FeliX - mit Algebra Geometrie machen (German) (pp. 15–17). Computeralgebra Rundbrief: Sonderheft zum Jahr der Mathematik.

    Google Scholar 

  • Polya, G. (1962). Mathematical discovery: On understanding, learning, and teaching problem solving. London, UK: Wiley.

    Google Scholar 

  • Recio, T., & Vélez, M. P. (1999). Automatic discovery of theorems in elementary geometry. Journal of Automated Reasoning, 23, 63–82.

    Google Scholar 

  • Schwartz, J. L., & Yerushalmy, M. (1983). The Geometric Supposer. Pleasantville, NY: Sunburst Communications.

    Google Scholar 

  • Sinclair, N., Bartolini Bussi, M. G., de Villiers, M., Jones, K., Kortenkamp, U., Leung, A., et al. (2016). Recent research on geometry education: An ICME-13 survey team report. ZDM Mathematics Education, 48, 691–719.

    Article  Google Scholar 

  • Wu, W. T. (1978). On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica, 21(2). Reprinted In W. W. Bledsoe, & D. W. Loveland (Eds.), Automated Theorem-Proving: After 25 Years. Providence, RI: AMS (1983).

    Google Scholar 

  • Ye, Z., Chou, S. C., & Gao, X. S. (2011). An introduction to Java Geometry Expert. In Automated Deduction in Geometry, 7th International Workshop, ADG 2008, Shanghai, China, September 22–24, 2008. Revised Papers, Lecture Notes in Computer Science (Vol. 6301, pp. 189–195). Springer.

    Google Scholar 

Download references

Acknowledgements

We thank the referees for many interesting suggestions and comments and, in particular, for pointing us to several relevant bibliographic references. Special thanks to Gila Hanna, Dragana Martinovic, Chris Sangwin, Arleen Schenke, and David A. Reid for their direct help in improving the text of this chapter.

The second and third authors have been partially funded by Spanish and EDF Research Grant MTM2017-88796-P.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Zoltán Kovács .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Hohenwarter, M., Kovács, Z., Recio, T. (2019). Using Automated Reasoning Tools to Explore Geometric Statements and Conjectures. In: Hanna, G., Reid, D., de Villiers, M. (eds) Proof Technology in Mathematics Research and Teaching . Mathematics Education in the Digital Era, vol 14. Springer, Cham. https://doi.org/10.1007/978-3-030-28483-1_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-28483-1_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-28482-4

  • Online ISBN: 978-3-030-28483-1

  • eBook Packages: EducationEducation (R0)

Publish with us

Policies and ethics