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

set Ξ [18]. Let w.l.o.g. be Ξ = { x 1 ,...,x k } . Then we apply recursively the

Hermitian quantifier elimination to

g∈G

∃ x k +1 ···∃ x n g =0 ∧ h> 0 ∧ f =0

h∈H f∈F

and obtain a quantifier-free formula ψ . Then we apply our quantifier elimination
procedure again recursively to

x k ( ψ ) ∃ x 1 ···∃

yielding ψ . Our quantifier-free result is then γ ∧ ψ . This concludes the description

of the Hermitian quantifier-elimination.

3 Generic Hermitian Quantifier Elimination

In this section we discuss our modifications to the algorithm for obtaining
a generic quantifier elimination. As already mentioned in the introduction, a
generic quantifier elimination computes for a first-order formula ϕ aquantifier-
free formula ϕ and a conjunction Θ of negated equations in the parameters u 1 ,
..., u m such that

ϕ ) . Θ −→ ( ϕ ←→

Θ is called a theory. Recall from our discussion in the previous section that our
quantifier elimination algorithm is recursive. In each recursive call we consider
variables originally bound by quantifiers as additional parameters. Obviously we
are not allowed to add assumptions about these additional parameters to Θ .To
guarantee this restriction we denote by v 1 , ..., v m the set of parameters of the
input formula. In the discussion below we will always test whether an assumption
is valid by checking whether it contains only variables from { v 1 ,...,v m } .

3.1 Generic Grobner Systems

Our first and most prominent modification to the pure elimination algorithm
is to compute in the preparation phase a generic Grobner system instead of a
regular one.
Let < be a term order and let p = c 1 t 1 + ··· + c d t d be a polynomial in

Q [ u 1 ,...,u m ][ x 1 ,...,x n ], where c 1 , ..., c d ∈ Q [ u 1 ,...,u m ]and t d > ··· >t 1

m this may or may not be
true for the polynomial p ( c ). It depends on whether c d ( c )

terms. Then the head term of p is c d .Foragiven c ∈ R

= 0 or not. During the
construction of a Grobner system we systematically construct a case distinction
about some parameters of the occurring polynomials. In each case of this case
distinction the head term of all polynomials is uniformly determined.
A generic Grobner system allows us to exclude some cases by adding assump-
tions to Θ .Inparticularif c d contains only parameters from { v 1 ,...,v m } we add