Supporting Proving and Discovering Geometric Inequalities in GeoGebra by using Tarski

Christopher W. Brown
(United States Naval Academy, Annapolis, MD, USA)
Zoltán Kovács
(The Private University College of Education of the Diocese of Linz, Linz, Austria)
Róbert Vajda
(Bolyai Institute, University of Szeged, Szeged, Hungary)

We introduce a system of software tools that can automatically prove or discover geometric inequalities. The system, called GeoGebra Discovery, consisting of an extended version of GeoGebra, a controller web service realgeom, and the computational tool Tarski (with the extensive help of the QEPCAD B system) successfully solves several non-trivial problems in Euclidean planar geometry related to inequalities.

In Predrag Janičić and Zoltán Kovács: Proceedings of the 13th International Conference on Automated Deduction in Geometry (ADG 2021), Hagenberg, Austria/virtual, September 15-17, 2021, Electronic Proceedings in Theoretical Computer Science 352, pp. 156–166.
Published: 30th December 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.352.18 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org