Radical Decomposition and Geometry Theorem Proving

Michael Kalkbrener Department of Mathematics Swiss Federal Institute of Technology CH-8092 Zurich, Switzerland

Abstract

Often geometric statements are true only in a generic sense, i.e. after certain degenerate situations have been ruled out. The problem of finding nondegeneracy conditions is related to the following algorithmic problem: for a radical J in a Noetherian commutative ring R with identity and a polynomial f in R compute radicals J_{1}, J_{2} such that

J = J_{1} ∩ J_{2},  f ∈ J_{1},  J_{2} : f = J_{2}.

We show that if this “splitting” problem can be solved in R then it can be solved in R[x_{1}, …, x_{n}]. From the constructive proof we obtain an algorithm for splitting radicals in multivariate polynomial rings over fields. The basic operation in this algorithm is the computation of greatest common divisors of univariate polynomials over extension fields. No factorization or Gröbner bases computation is needed. We apply this algorithm to geometry theorem proving and show that our algorithm can not only be used for deciding correctness of geometric statements but also for constructing simplest nondegeneracy conditions with respect to lexicographical degree orderings.