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

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 hi to hi-ri, 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 mathbbQ[r,r1,r2,ldots] we can find a conclusive result. It plays an important role that if r1,r2,ldots are real, r must also be real if there is a linear polynomial p(r)∈ 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.