Mechanical geometry theorem proving based on Gröbner bases (Q676849)

The paper proposes a method for mechanical elementary geometry theorem proving. In more details, suppose a geometric statement is described by some polynomials \[ h_1,\ldots,h_m \in {\mathbb{Q}}[x_1,\ldots,x_n] \] and suppose the conclusion is expressed by a polynomial \(g\in {\mathbb{Q}}[x_1,\ldots,x_n]\); assume the ideal \(J=(h_1,\ldots,h_m)\) is zero-dimensional. The statement is said generally true if \(g\in \sqrt J\) and, if \({\mathcal M}\) is a minimal prime over \(J\), is said generally true on the component \(\mathcal M\) if \(g\in {\mathcal M}\). The paper gives an algorithm which computes, from the Gröbner basis of \(J\) with respect to a pure lexicographic order, the minimal primes over \(J\). In this way the author gives a method which allows to verify if a statement is generally true or generally true on some components of the ideal \(J\).