Parametric Root Finding for Supporting Proving and Discovering Geometric Inequalities in GeoGebra

TL;DR

This paper presents a new parametric root finding method integrated into GeoGebra for efficiently proving and discovering geometric inequalities, replacing more computationally intensive approaches and enabling practical educational applications.

Contribution

The paper introduces a parametric root finding algorithm for GeoGebra that improves efficiency over traditional real quantifier elimination methods in geometric inequality reasoning.

Findings

The new method avoids high-dimensional cell decomposition.

It computes Groebner bases for discriminant varieties.

It integrates with existing GeoGebra tools and solvers.

Abstract

We introduced the package/subsystem GeoGebra Discovery to GeoGebra which supports the automated proving or discovering of elementary geometry inequalities. In this case study, for inequality exploration problems related to isosceles and right angle triangle subclasses, we demonstrate how our general real quantifier elimination (RQE) approach could be replaced by a parametric root finding (PRF) algorithm. The general RQE requires the full cell decomposition of a high dimensional space, while the new method can avoid this expensive computation and can lead to practical speedups. To obtain a solution for a 1D-exploration problem, we compute a Groebner basis for the discriminant variety of the 1-dimensional parametric system and solve finitely many nonlinear real (NRA) satisfiability (SAT) problems. We illustrate the needed computations by examples. Since Groebner basis algorithms are available in Giac (the underlying free computer algebra system in GeoGebra) and freely available efficient NRA-SAT solvers (SMT-RAT, Tarski, Z3, etc.) can be linked to GeoGebra, we hope that the method could be easily added to the existing reasoning tool set for educational purposes.