A GENERALIZED EUCLIDEAN ALGORITHM FOR GEOMETRY THEOREM-PROVING

In the first part of this paper, we present an algorithm that computes an unmixed-dimensional decomposition of a variety V. Each V-i in the decomposition V = V-1 boolean OR...boolean OR V-m is given by a finite set of polynomials which represents the generic points of the irreduc ible components of V-i. The basic operation in our algorithm is the co mputation of greatest common divisors of univariate polynomials over e xtension fields given by regular chains. No factorization is needed. I n the second part, this algorithm is applied to geometry theorem provi ng. We show that it can be used for deciding whether geometry statemen ts are generically true or whether they are true under given nondegene racy conditions. If a geometry statement is generically true, the simp lest nondegeneracy condition with respect to a lexicographical degree ordering can be constructed by means of our algorithm.