A refutational approach to geometry theorem proving

摘要

A refutational method for proving universally quantified formulae in algebraic geometry is proposed. A geometry statement to be proved is usually stated as a finite set of hypotheses implying a conclusion. A hypothesis is either a polynomial equation expressing a geometric relation or a polynomial inequation (the negation of a polynomial equation) expressing a subsidiary condition that rules out degenerate cases and perhaps some general cases. A conclusion is a polynomial equation expressing a geometry relation to be derived. Instead of showing that the conclusion directly follows from the hypothesis equations and inequations, the proof-by-contradiction technique is employed. It is checked whether the negation of the conclusion is inconsistent with the hypotheses. This can be done by converting the hypotheses and the negation of the conclusion into a finite set of polynomial equations and checking that they do not have a common solution. There exist many methods for this check, thus giving a complete decision procedure for such geometry statements. This approach has been recently employed to automatically prove a number of interesting theorems in plane Euclidean geometry. A Gröbner basis algorithm is used to check whether a finite set of polynomial equations does not have a solution. Two other formulations of geometry problems are also discussed and complete methods for solving them using the Gröbner basis computations are given.