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

H the formulas Γ d build a complete disjunctive case distinction of
the degree of h under specifications of the parameters. Notice that it does not

For fixed h ∈

matter at this point, if Γ d is equivalent to false .Let d ( h )= k =0 a h,k x n .We
have the equivalence

x n
h∈H

=0 x n

h∈H

=0 .

δ∈D ∃

Γ δ h ∧ ∃ h> 0 ∧ f ←→ δ h ( h ) > 0 ∧ f

f∈F f∈F

For each δ we then in turn transform the formulas

x n
h

=0

Γ δ h ∧

∃ δ h ( h ) > 0 ∧ f

∈ H f ∈ F

separately to

d f

a f,i =0 ∧

f ∈ F i =0

a h,δ h > 0 Γ δ h ∧

∨

h∈H

a h,δ h > 0) Γ δ h ∧ a h,δ h < 0 ∨ (Even( δ h ) ∧ ∨

h ∈ H

x n
h

=0

∂p
∂x n

Γ δ h ∧

Q ∃

δ h ( h ) > 0 ∧ ∨

p ∈ ∈ H

q )=0 , x n

h∈H

Γ δ h ∧

P ∃

δ h ( h ) > 0 ∧ ( p −

( p,q ) ∈

where Q = . The used predicate Even( n ) is true if and only if

n is even. Thus we have shown how to trace back this case to the case with at
least one existing equation in the input formula.
Let ϕ denote the complete transformed input formula. Then we apply the
Hermitian quantifier elimination to each quantified constituent and obtain, by
eliminating x n , a quantifier-free equivalent ψ . Finally we apply the Hermitian
quantifier elimination again recursively to

{ h ∈ H | δ h ≥ }

2

x n− 1 ( ψ )

∃ x 1 ···∃

obtaining a quantifier-free equivalent ψ . The final result of the elimination step
is then

γ ∧ ψ.

2.4 Partial Elimination

We enter this case of the Hermitian quantifier elimination if the dimension of
G is d with d ∈{ 1 ,...,n − 1 } . We compute a maximal strongly independent