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

elimination. For this automatic solution he has used all three quantifier elimina-
tion methods, namely quantifier elimination by virtual substitution, Hermitian
quantifier elimination, and quantifier elimination by partial cylindrical algebraic
decomposition as well as the simplification methods described in [11].
The definition, development and implementation of new paradigms related to
quantifier elimination algorithms have been very successful in the past. Extended
quantifier elimination provides not only an equivalent formula but sample solu-
tions. It can be applied e.g. in the area of generalized constraint solving yielding
optimal solutions [12].
Generic quantifier elimination was introduced for the virtual substitution
method by the first author together with Sturm and Weispfenning [13]. Let ϕ be
an input formula with quantified variables x 1 ,..., x n and parameters u 1 ,..., u m .
Recall that regular quantifier elimination computes from ϕ aquantifier-freefor-
mula ϕ such that for all real values c 1 , ..., c m for the parameters u 1 , ..., u m
both ϕ and ϕ ϕ ( c 1 ,...,c m ). In

the case of generic quantifier elimination we compute additionally a conjunction
Θ of non-trivial negated-equations, such that

are equivalent, i.e we have ϕ ( c 1 ,...,c m ) ←→

ϕ ) .
In other words, Θ restricts the parameter space. Note that Θ cannot become
inconsistent, and moreover, the complement of the set described by Θ has a lower
dimension than the complete parameter space. Thus it restricts our parameter
space only slightly.
The idea behind the generic quantifier elimination is to add assumptions to
Θ whenever this may either speed up the computation or may cause the algo-
rithm to produce a shorter result formula ϕ . The paradigm of generic quantifier
elimination was introduced in [13] in the area of automated geometry proving.
The key idea here is to express a geometric theorem as a quantified formula
and then verify it by quantifier elimination. Regular quantifier elimination may
fail due to lack of resources or if the theorem does not hold. In the latter case
it may be false only for some degenerated situations, as for empty triangles
or rectangles instead of arbitrary triangles. Generic quantifier elimination is in
this area superior to the regular one for two reasons: The computations are in
general much faster and the assumptions made in Θ may exclude degenerated
situations in which the theorem is false. In the above cited paper, which is based
on quantifier elimination by virtual substitution, it was heuristically shown that
for this generic quantifier elimination in fact Θ contains mostly non-degeneracy
conditions.
Meanwhile, using a generic projection operator, the concept of generic quan-
tifier elimination was also successfully applied to quantifier elimination by partial
cylindrical algebraic decomposition [14]. Seidl and Sturm study the general ap-
plicability of generic quantifier elimination in contrast to the regular one. As for
regular quantifier elimination by cylindrical algebraic decomposition, this ap-
proach is successful mostly for problems containing only a few variables. This
restricts the applicability of the generic projection operator to the area of auto-
mated theorem proving.

Θ −→ ( ϕ ←→