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

In this note we introduce a generic variant of Hermitian quantifier elimination
and apply it in the area of automated theorem proving. This generic quantifier
elimination is not degree restricted as the method based on virtual substitution,
and it can handle in general, more variables than the method based on cylindri-
cal algebraic decomposition. Hermitian quantifier elimination is, however, well
suited for formulas containing many equations as in the case of automated geo-
metric theorem proving. Nevertheless the generic Hermitian quantifier elimina-
tion is well suited in many other application areas, e.g., in physical applications
in which a equation between two different values is always of no meaning.
The plan of the paper is as follows: In the next Section 2 we sketch the Hermi-
tian quantifier elimination algorithm. In Section 3 we discuss three parts of the
algorithm where the concept of generic quantifier elimination can be successfully
applied. After describing the generic algorithm we show in Section 4 the scope
of our method by computation examples. In the final Section 5 we conclude and
summarize our results.

2 The Basic Algorithm

We want to eliminate the quantifiers from an arbitrary first-order formula in the
language of ordered rings. In our discussion we restrict our attention to the main
parts of the Hermitian quantifier elimination with some improvements. Given an
arbitrary first-order formula, we first compute an equivalent prenex normal form
of the form

Q n x n 1 ··· Q n x nm n ··· Q 2 x 21 ··· Q 2 x 2 m 2 Q 1 x 11 ··· Q 1 x 1 m 1 ( ψ ) , Q i ∈{∃ , ∀} ,

with and ψ quantifier-free.

Our elimination algorithm eliminates the quantifier blocks, block by block,
beginning with the innermost one, i.e., we compute first a quantifier-free equiv-
alent of

Q i − 1 = Q i for i ∈{ 2 ,...,n }

Q 1 x 11 ··· Q 1 x 1 m 1 ( ψ ) .

Using the equivalence

∀ x 1 ... ∀ x n ( ψ ) ←→ ¬ ∃ x 1 ... ∃ x n ( ¬ ψ ) ,

we can obviously restrict our discussion to the case of one existential quantifier
block, i.e. . We can furthermore assume without lost of generality (for

short w.l.o.g.) that ψ contains only atomic formulas of the form t =0, t> 0and
t

Q 1 = ∃

=0andthat ψ is in disjunctive normal form. By applying the equivalence

x n ψ i

k k

i =1 ∃

∃ x 1 ... ∃ ←→ x 1 ... ∃ x n ( ψ i )

i =1

we assume in the following that ψ is a conjunction of atomic formulas of the
above form.