Using Automated Reasoning Tools to Explore Geometric Statements and Conjectures

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 technologymediated educational framework, where GeoGebra could play the role of a mentor, helping students bothto 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.