Information Technology Reference
In-Depth Information
select
g
1
,
g
2
from
G
such that the normal form
h
of the
S
-polynomial of
g
1
,
g
2
is not 0. Finally we extend
S
by (
γ,G
),
h
and
h
. This process is repeated until
the normal form of all S-polynomials is 0.
As mentioned above the generic variant of the Grobner system computation
allows us to drop branches. Recall from the presentation of our quantifier elimi-
nation algorithm that we have to perform for each branch a separate quantifier
elimination. If we are on the top-level of our quantifier-elimination algorithm we
actually compute a Grobner system containing one single branch, because the
condition on line 3 of the algorithm “extend” is tautological in this situation.
This reduces, in general, both the computation time and the size of the output
formula dramatically. As a rule, observed from our sample computations, we
compute only a few assumptions which can often be easily interpreted.
3.2
Generic Equation Construction
In Section 2.3 we have discussed how to construct an equation from a set of
ordering relations. In this section we adapt this to the generic case.
Recall that we generate a complete case distinction about the highest coe
-
cient of each
h
H
. The size of this case distinction can be reduced by making
appropriate assumptions as shown below.
For
h
∈
H
let
n
h
=max
{−
∈
0
,...,d
h
}
Var(
a
h,i
)
}∪
i
v
1
,...,v
m
}
.
1
∈{
⊆{
For all
n
h
with
h
∈
H
and
n
h
≥
0weaddtheassumption
a
h,n
h
= 0 to our theory
Θ
. Let finally
D
k
=1
{
. Then we can proceed with the
transformation described in Section 2.3 using
D
instead of
D
.Notethat
D
⊆
=
×
max(0
,n
h
)
,...,d
h
}
D
and often
D
D
.
3.3
Generic Type Formula Computation
In this section we discuss an approach to computing generic type formulas.
The type formula construction presented in Section 2.2 is a primitive version
of the method used in our highly optimized Hermitian quantifier elimination. We
actually compute a type formula
τ
d
for a polynomial
p
=
i
=0
c
i
y
i
of degree
d
recursively:
τ
d
(
c
d
,...,c
0
)
.
The recursion basis are the simple type formulas up to the degree 3. The defini-
tion of
τ
d
is similar to the definition of
τ
d
, but assumes a non-vanishing constant
coecient which implies the absence of the zero 0. The formula
τ
d
is actually a
disjunctive normal form. Each constituent has the following schema
τ
d
(
c
d
,...,c
0
)
≡
(
c
0
=0)
∧
τ
d−
1
∨
c
k
1
k
1
0
∧···∧
c
k
l
k
l
0
,
where
{
k
1
,...,k
l
}⊆{
1
,...,d
}
and
k
j
∈{
<, >
}
.
Search WWH ::
Custom Search