A complete and practical algorithm for geometric theorem proving (extended abstract)
Ashutosh Rege · 1995
This paper describes a complete and practical algorithm for the problem of geometric theorem proving.The algorithm works over algebraically closed fields as well as over the reals and takes care of degenerate cases.Our work ismotivated by several recent improvements in algorithms for sign determination and symbolic-numeric computation.Based on these, we provide an algorithm for solving triangular systems efficiently using straightline program arithmetic.The report concludes with a description of an implementation and provides preliminary benchmarks from the same.The basic problem we consider is the following : given a system of hypotheses polynomial equations in triangular form, determine whether the set of their common zeros over the reals M contained in the set of real zeros of the conclusion polynomial.(One can use any standard algorithm for triangulating if the hypotheses are not triangular to begin with, see e.g.[4]).The observation here is that, in order to prove a theorem or refute it, one is only interested in the sign (+, -or O) of the conclusion polynomial at the real zeros of the hypotheses polynomials.We provide an efficient method to encode the roots of a triangular system using the Sylvester resultant.To determine the signs, we make use of Sturm sequences which enable us to determine the number of real roots of the hypotheses where the conclusion is non-zero.Thus our algorithm can determine