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