Information Technology Reference
In-Depth Information
is obviously no zero of
G
, because 1 is member of the ideal. Our elimination
result in this case is simply
false
. If the dimension is
n
, which is the number
of main variables, we have to reformulate the problem and call our quantifier
elimination recursively as described in Section 2.3. If, finally, the dimension is
between 1 and
n
1 then we eliminate the quantifier block with two recursive
calls of our Hermitian quantifier elimination as described in Section 2.4.
−
2.2 The Zero-Dimensional Case
We want to eliminate the quantifiers from
x
n
g∈G
h>
0
f∈F
=0
,
γ
∧∃
x
1
···∃
g
=0
∧
f
h∈H
m
where for each
c
in
R
with
γ
(
c
)wehavethat
G
(
c
)isGrobner basis of the
zero-dimensional ideal Id
G
(
c
)
. For this we use a method originally developed
for counting the real zeroes of Id
G
(
c
)
w.r.t. the side conditions generated by
H
and
F
.
The result we use was found independently by Pedersen, Roy, Szpirglas [16]
and Becker, Wormann [17] generalizing a result of Hermite for the bivariate
case. It was adapted to the parametric case including several side conditions by
Weispfenning [7] and further extended by the first author [8].
For a moment, assume that
H
=
{
h
1
,...,h
r
}
and
F
=
{
f
1
,...,f
s
}
.Let
r
.For
e
E
define
h
e
by
E
=
{
1
,
2
}
∈
r
s
h
e
=
h
e
i
i
f
i
.
·
i
=1
i
=1
For a univariate polynomial
q
define
Z
+
(
q
) as the number of positive zeroes
and
Z
−
(
q
) as the number of negative zeroes, respectively, both counted with
multiplicities.
Consider
R
=
Q
(
u
1
,...,u
m
)[
x
1
,...,x
n
]andletbe
I
=Id(
G
)and
B
=
{
-algebra with basis
B
(
c
)foreach
c
with
γ
(
c
). Note that each element in
R
can also be viewed as an
element of
R/I
.For
q
v
1
,...,v
b
}
the reduced terms of
G
.Then
R
(
c
)
/I
(
c
)isa
Q
∈
R
,themap
m
q
:
R/I
→
R/I,
m
q
(
p
)=
q
·
p
defined by
is linear. Using this definition we define for a polynomial
p
∈
R
the
b
×
b
matrix
Q
p
=(
q
ij
)by
q
ij
=trace(
m
v
i
v
j
p
)
.
Finally let
χ
(
Q
p
) be the characteristic polynomial of
Q
p
.
Then we have for each
c
m
with
γ
(
c
), that
∈
R
a
n
=0
∈
R
g
(
c
)(
a
)=0
∧
h
(
c
)(
a
)
>
0
∧
f
(
c
)(
a
)
g
∈
G
h
∈
H
f
∈
F
Z
−
(
χ
), where
χ
=
e∈E
χ
(
Q
h
e
).
equals
Z
+
(
χ
)
−
Search WWH ::
Custom Search