Rewriting input expressions in complex algebraic geometry provers (Q2631957)

The use of dynamic geometry by complex algebraic provers help to understand both the input and the output of classical theorems that involve Euclidean geometry. For dynamic geometry to exist, there must be an algebraic formulation behind. This may seem simple, but it is highly complex. The programmer has to consider degenerate situations and different situations over the complex numbers when formulating correctly. This work offers illustrative examples of this problem and its authors are experts in this field. By using classical tools of commutative algebra, such as elimination ideals and Groebner basis, in Section 4 the authors present an algorithm to convert expressions having non-negative quantities (like distances) in Euclidean geometry theorems to be usable in a complex algebraic geometry prover.