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 geomtry 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 exists many methods for this check, thus giving a complete decision procedure for such geomtry statements. This approach has been recently employed to automatically prove a number of interesting theorems in plane Eupclidean geometry. A Grobner basis algoithm 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 Grobner basis computations are given.

For a copy of this paper, email request to kapur@cs.unm.edu