Generic Hermitian Quantifier Elimination - Artificial Intelligence and Symbolic Computation - page 80

Generic Hermitian Quantifier Elimination

Andreas Dolzmann 1 and Lorenz A. Gilch 2

1 University of Passau, Passau, Germany
[e-mail]
http://www.fmi.uni-passau.de/~dolzmann/
2 Graz University of Technology, Graz, Austria
[e-mail]
http://people.freenet.de/lorenzg/

Abstract. We present a new method for generic quantifier elimination
that uses an extension of Hermitian quantifier elimination. By means
of sample computations we show that this generic Hermitian quantifier
elimination is, for instance, an important method for automated theorem
proving in geometry.

1 Introduction

Ever since quantifier elimination by cad has been implemented by Collins [1],
quantifier elimination has become more and more important. This was reinforced
especially by the development and implementation of the partial cad [2] by Hong
and later Brown [3]. Beside the approach used there, quantifier elimination by
virtual substitution was published by Weispfenning [4, 5] and further developed
and implemented by the first author together with Sturm in redlog [6]. The
latter method can only be applied to degree restricted formulas. Although both
methods are implemented highly eciently, none is superior to the other one.
Moreover sometimes the methods fail solving problems which seem to be solvable
using quantifier elimination. Therefore it is necessary to develop and implement
further quantifier elimination algorithms.
The quantifier elimination by real root counting was published by Weispfen-
ning in 1998 [7], although he had already published in 1993 a technical report
describing this method. The algorithm was first implemented by the first author
in 1994 as a diploma thesis [8] in the computer algebra system mas.Numer-
ous new optimizations were developed by the authors. They were implemented
by the second author [9] in a complete reimplementation of the method in the
package redlog [6] of the computer algebra system reduce . The improved
version of this quantifier elimination is called Hermitian quantifier elimination.
The name “Hermitian” quantifier elimination was chosen to acknowledge the
influence of Hermite's work in the area of real root counting.
Hermitian quantifier elimination has been proved to be a powerful tool for
particular classes of elimination problems. In [10] the first author has used it for
the automatic solution of a real algebraic implicitization problem by quantifier