This is the official GitHub repository of ADG Foundation, a Working Group on Automated Deduction in Geometry.
ADG Foundation maintains a library to provide rigorous descriptions of the axiom systems used by the different geometry automatic and interactive theorem provers, propose common input and output languages for geometry theorem provers, and establish and make available to the research community a large library of geometric problems.
The ADG Library is an initiative started by ADG Foundation members Pedro Quaresma, Predrag Janičić, Julien Narboux, Zoltán Kovács, Anna Petiurenko, Filip Marić, and Nuno Baeta. It is currently a work in progress.
ADG Foundation regularly examines, discusses and evaluates high quality computer software written to study automated deduction in geometry. In our main focus are the following software, but this list can be extended in the future. Most importantly, the items listed here are supported in the ADG Library by considering them de facto standards and providing importers and exporters for them:
- GCLC, “Geometry Constructions → LaTeX Converter”, a tool for visualizing geometry, and for producing mathematical illustrations, extended with the help of automated theorem provers.
- Java Geometry Expert, a graphical tool to study proofs of geometry theorems in Euclidean geometry. We store a stable version of the currently maintained fork and look forward to releasing new versions on this page. Also, we suggest trying an online version powered by CheerpJ.
- GeoGebra Discovery is a fork of an experimental version of the dynamic mathematics software GeoGebra. It allows the user to study proofs with various methods.