On the application of Buchberger's algorithm to automated geometry theorem proving (Q1094149)

In this paper we present a new approach to automated geometry theorem proving that is based on Buchberger's Gröbner bases method. The goal is to automatically prove geometry theorems whose hypotheses and conjecture can be expressed algebraically, i.e. by polynomial equations. After shortly reviewing the problem considered and discussing some new aspects of confirming theorems, we present two different methods to applying Buchberger's algorithm to geometry theorem proving, each of them being more efficient than the other on a certain class of problems. The second method requires a new notion of reduction, which we call pseudoreduction. This pseudoreduction yields results on polynomials over some rational function field by computations that are done merely over the rationals and, therefore, is of general interest also. Finally, computing time statistics on 70 non-trivial examples are given, based on an implementation of the methods in the computer algebra system SAC-2 on an IBM 4341.