An Elimination Method Based on Seidenberg’s Theory and Its Applications

In this paper we present an elimination method for algebraically closed fields based on Seidenberg’s theory. The method produces, for any pair [PS, QS] of sets of multivariate polynomials, a sequence of triangular forms TF₁,…, TF_e and polynomial sets US₁,…, US_e such that the difference set of common zeros of PS and QS is the same as the union of the difference sets of common zeros of TF_i and US_i. Moreover, the triangular forms TF_i and polynomial sets US_i can be so computed as to give a necessary and sufficient condition for the given system to have algebraic zeros for some prescribed variables. This method has a number of applications such as to solving systems of polynomial equations and inequalities, mechanical theorem proving in geometry, irreducible decomposition of algebraic varieties and constructive proof of Hilbert’s Nullstellensatz which are partially discussed in the paper. Preliminary experiments show that the efficiency of this method is at least comparable with that of the well-known methods of characteristic sets and Gröbner bases for some applications. A few illustrative yet encouraging examples performed by a draft implementation of the method are given.