Supporting Proving and Discovering Geometric Inequalities in GeoGebra by using Tarski
Christopher W. Brown (United States Naval Academy, Annapolis, MD,, USA), Zolt\'an Kov\'acs (The Private University College of Education of the, Diocese of Linz, Linz, Austria), R\'obert Vajda (Bolyai Institute, University, of Szeged, Szeged, Hungary)
TL;DR
This paper presents GeoGebra Discovery, a software system integrating GeoGebra, Tarski, and QEPCAD B to automatically prove and discover complex geometric inequalities in Euclidean plane geometry.
Contribution
It introduces an integrated toolset that automates the proving and discovering of geometric inequalities, enhancing capabilities in Euclidean geometry analysis.
Findings
Successfully solves non-trivial geometric inequality problems
Automates proof and discovery processes in Euclidean geometry
Extends GeoGebra with Tarski and QEPCAD B for advanced reasoning
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.