Using Automatic Theorem Proving to Improve the Usability of Geometry Software

Dynamic or interactive Geometry software (DGS) is the mathematical version of vector based drawing software: the objects (points, lines, circles, conics, polygons, etc.) are both graphical and mathematical entities. This allows adding relations between the objects that govern their behavior. Thus, DGS is used as an input tool for constructions, as opposed to simple drawings. The additional information that is present in a construction can be used to greatly enhance the usability of DGS. We show how automatic theorem proving can be used to remove redundant elements in a construction that obstruct a smooth work flow clarify the semantics of user actions, and improve the graphical rendering of elements. Finally we discuss the various possibilities of transforming the mathematical tool DGS into an educational tool. Here, automatic theorem proving is used to analyze user actions and to react properly.