Automatic theorem generation in plane geometry is a topic that deserves study. Some fruitful attempts have already been made by Bagai, Shanbhogue, Żytkow and Chou (2005), based on a conceptual framework for discovery of theorems in geometry, and a mechanism which systematically discovers such theorems.

Our present work, similarly to the abovementioned one, has its background in Wu's algebraic method, but, by contrast, it has a widely disseminated dynamic geometry engine, GeoGebra. In our work a geometric construction can be opened in a web page, and can be investigated on having usual relations like collinear points, parallel or perpendicular lines, isosceles triangles, and so on, automatically. The relations to observe can be fine-tuned by the user, to avoid explosion of combinatorial complexity. On the other hand, the input construction can be extended by a configurable set of newly added objects to obtain a wider set of possible results.

GeoGebra's high level user interface (UI) and JavaScript application programming interface (API) make it possible to study planar geometry theorems in an automated but still convenient and modern way. Further improvements of our approach, namely, to consider false statements and automatically compute an extension of the hypothesis set, in order to get true statements, are promising horizons towards an Automated Geometer tool, cf. Guzmán (2002).

All of these efforts are based on GeoGebra's recent improvements, the "Automated Reasoning Tools".

• Francisco Botana [email protected]
• Zoltán Kovács [email protected]
• Tomás Recio [email protected]

This program uses the combinations.js and sprintf.js JavaScript libraries, written by Akseli Palén and Alexandru Mărășteanu, respectively.