Information Technology Reference

In-Depth Information

2.1

Preparation

We assume that our input formula has the following form

,

∃

x
1
...

∃

x
n

(
g
=0)

∧

(
h>
0)

∧

(
f

=0)

G

h∈H

f∈F

g

∈

where
G
,
H
,and
F
are finite sets of polynomials in

[
u
1
,...,u
m
][
x
1
,...,x
n
]. We

can obviously evaluate each variable-free atomic formula to a truth value making

itself superfluous or the whole conjunction contradictive. Thus we can w.l.o.g. as-

sume that each polynomial is an element of

Q

Q

[
u
1
,...,u
m
][
x
1
,...,x
n
]

\
Q

.

m

For a polynomial
g

∈
Q

[
u
1
,...,u
m
][
x
1
,...,x
n
]and(
c
1
,...,c
m
)

∈
R

we

denote by
g
(
c
1
,...,c
m
) the polynomial in

R

[
x
1
,...,x
n
] constructed from
g
by

plugging in the
c
i
for
u
i
with
i

∈{

1
,...,m

}

. We extend this notation in the

natural manner to sets of polynomials.

If the set
G
is empty, we proceed with our quantifier elimination as described

in Section 2.3. If
G
is not empty, we compute a Grobner system [15] w.r.t. an

arbitrary but fixed term order. This term order is also fixed for all subsequent

computations in the following paragraphs.

The concept of Grobner systems generalizes the concept of Grobner bases to

the parametric case. With the term “parametric case” we describe situations in

which the coecient of the polynomials are given parametric as polynomials in

some variables, e.g.
mx
+
b
is a univariate polynomial in
x
with the parametric

coecients
m
and
b
.

AGrobner system
S
is a finite set of pairs (
γ,G
), called branches of the

Grobner system. Each branch consists of a quantifier-free formula
γ
in the
u
1
,

...,
u
m
and a finite set of polynomials

m

there is one branch (
γ,G
) such that
γ
(
c
)holds,wehaveId
G
(
c
)
=Id
G
(
c
)
,

and
G
(
c
)isaGrobner basis. In fact, all computations used for our algorithm

can be performed parametrically using
G
.

Note, that for every (
γ,G
)and
c

Q

[
u
1
,...,u
m
][
x
1
,...,x
n
]. For each
c

∈
R

with
γ
(
c
)wehavethat
G
(
c
),
G
(
c
)

m

∈
R

and Id
G
(
c
)
have the same zeroes. By switching from

(
g
=0) to

γ

∧

(
g
=0)

G

(
γ,G
)

∈

S

g∈G

g∈

and interchanging the disjunction with the existential quantifier block it suces

to eliminate the quantifiers from

=0
.

h>
0

f∈F

γ

∧∃

x
1
···∃

x
n

g
=0

∧

f

g∈G

h∈H

Let
d
be the dimension of Id
G
(
c
)
with
c

m
and
γ
(
c
). Note that this di-

mension is uniquely determined by
γ
. According to the dimension
d
we proceed

as follows: If the ideal is zero dimensional, i.e.,
d
= 0, we eliminate the complete

block of existential quantifiers as described in the next Section 2.2. If the dimen-

sion is

∈
R

−

1, i.e., the ideal is actually the entire polynomial ring, and thus there

Search WWH ::

Custom Search