Information Technology Reference
In-Depth Information
c
d
=0to
Θ
and assume in the following computation steps that the head term
of
p
is
t
d
.
We denote by
a suitable heuristic to decide an implication: If
γ
α
,then
we have the validity of
γ
α
. Note that the construction of a Grobner system
requires that this heuristic can actually decide some implications.
The first algorithm extends a partial Grobner system by an additional poly-
nomial. Note that we assume that the theory
Θ
to be computed is globally
available.
We use the following notations: HC(
f
) is the head or leading coecient of
f
w.r.t. our fixed term order, Red(
f
) is the polynomial up to the head monomial,
Var(
f
) is the set of variables actually occurring in
f
.
−→
Algorithm 1 (extend)
Input: A partial system
S
, a branch
(
γ,G
)
,andtwo
polynomials
h
and
h
. Output: An extended partial system.
1
if
h
=0
then
return
S
∪{
(
γ,G
)
}
else if
Var
HC(
h
)
⊆{
2
v
1
,...,v
m
}
then
3
(HC(
h
)
Θ
:=
Θ
∧
=0)
4
∪
γ, G
}
return
S
∪{
h
5
HC(
h
)
else if
γ
∧
Θ
=0
then
6
∪
γ, G
}
return
S
∪{
h
7
HC(
h
)=0
then
else if
γ
∧
Θ
8
return extend(
S
,(
γ,G
),
h
,Red(
h
))
9
else
S
:=
γ
}
10
HC(
h
)
∧
=0
,G
∪{
h
11
return extend(
S
,(
γ
HC(
h
)=0
,G
),
h
,Red(
h
))
∧
12
fi
13
This algorithm differs from the algorithm for regular Grobner systems by
accessing the theory
Θ
and by the lines 3 and 4 for generating new assumptions.
For computing a Grobner system we start with computing an initial partial
system
S
by calling the following algorithm Initialize with input
G
.
Algorithm 2 (Initialize)
Input: A finite set
H
of polynomials. Output: A par-
tial system.
1
begin
S
:=
{
(true
,
∅
)
}
2
for each
h
∈
H
do
3
for each
(
γ,G
)
∈
S
do
4
S
:=
S
\{
(
γ,G
)
}
5
S := extend(
S
,(
γ,G
),
h
,
h
)
6
od
7
od
8
end
9
For computing the Grobner system from the partial system we proceed as
follows: We select a branch (
γ,G
)of
S
, compute
S
=
S
\{
(
γ,G
)
}
.Thenwe
Search WWH ::
Custom Search