A refutational approach to geometry theorem proving (Q1124373)

The paper under review is an interesting contribution to the very active field of automatic theorem proving initiated by Wu Wen Tsün's refinement of Descartes's method of algebraic geometry. A lot of geometric statements in affine or euclidean plane are amenable to mechanical proving provided that they are expressible as the emptiness of the algebraic set of zeros in the associated field K of a finite set of equations over the base field \(k\subseteq K\). Taking K to be algebraically closed, the proposed approach is based on Hilbert's Nullstellensatz and is complete in Wu's geometry but, no wonder is incomplete, in Tarski's geometry. To get completeness in the latter case a real Nullstellensatz is more opportune. Unlike Wu's approach, the proposed approach uses the Gröbner basis method instead of the factorization of polynomials.