Automated proving in planar geometry based on the complex number identity method and elimination

TL;DR

This paper introduces a fully automated method for proving planar geometry theorems using complex number identities and elimination ideals, implemented in computer algebra systems and integrated into GeoGebra.

Contribution

It advances the complex number identity proving method by automating the elimination process and integrating it into popular geometry software.

Findings

Automated proof procedure successfully eliminates variables in geometric problems.

Implementation in Mathematica, Maple, and Giac enhances computational capabilities.

Prototype integrated into GeoGebra demonstrates practical usability.

Abstract

We improve the complex number identity proving method to a fully automated procedure, based on elimination ideals. By using declarative equations or rewriting each real-relational hypothesis $h_i$ to $h_i-r_i$, and the thesis $t$ to $t-r$, clearing the denominators and introducing an extra expression with a slack variable, we eliminate all free and relational point variables. From the obtained ideal $I$ in $\mathbb{Q}[r,r_1,r_2,\ldots]$ we can find a conclusive result. It plays an important role that if $r_1,r_2,\ldots$ are real, $r$ must also be real if there is a linear polynomial $p(r)\in I$, unless division by zero occurs when expressing $r$. Our results are presented in Mathematica, Maple and in a new version of the Giac computer algebra system. Finally, we present a prototype of the automated procedure in an experimental version of the dynamic geometry software GeoGebra.