Information Technology Reference
In-Depth Information
C
=
P
(
t
)
⇐
i
=1
Q
i
(
x
i
),
l
is a non-root position in
t
,theterm
t
Case 2:
|
l
/
∈
Vars
Vars
(
t
). The conclusions of
D
1
,...,D
k
are
Q
1
(
t
1
)
,...,
Q
k
(
t
k
), respectively. It holds
t
=
t
and
{
x
1
,...,x
k
}⊆
{
x
i
→
t
i
|
i
=1
,...,k
}
.Since
S
is saturated,
the following Horn clauses are members of
S
:
P
t
[
]
l
{x
i
→Q
i
|i
=1
,...,k}
(
x
)
∧
i∈{
1
,...,k|x
i
∈
Vars
(
t|
l
)
}
C
1
:=
P
(
t
[
x
]
l
)
⇐
Q
i
(
x
i
)
|
l
)
⇐
i∈{
1
,...,k|x
i
∈
Vars
(
t|
l
)
}
C
2
:=
P
t
[
]
l
{x
i
→Q
i
|i
=1
,...,k}
(
t
Q
i
(
x
i
)
Vars
(
t
).Let
Here,
x/
∈
{
a
1
,...,a
s
}∪{
b
1
,...,b
r
}
=
{
1
,...,k
}
such that
Vars
(
t
a
1
,...,a
s
,b
1
,...,b
r
are pair-wise distinct,
x
a
1
,...,x
a
s
∈
/
|
l
) and further-
Vars
(
t
more
x
b
1
,...,x
b
r
∈
|
l
). We can replace the sub-derivation
D
with the
smaller derivation
D
b
1
···
D
b
r
C
2
P
t
[
]
l
{x
i
→Q
i
|i
=1
,...,k}
(
t
|
l
{
x
i
→
t
i
|
i
=1
,...,k
}
)
D
a
1
···
D
a
s
.
C
1
P
(
t
)
Thus we have constructed a smaller derivation for
P
(
t
) — contradiction.
The other cases, which are similar to those encountered for classes like
H
1
, can also be
treated straightforwardly.
Lemma 1 and Lemma 2 finally imply our main theorem:
Theorem 1.
Let
S
and
S
be sets of linear Horn clauses such that
S
∗
S
holds and
S
is saturated. Then
H
S
(
P
)
is tree regular for
every predicate
P
which occurs in
S
, i.e., the least model is tree regular.
H
S
(
P
)=
H
S
∩N
(
P
)
holds and thus
Because of the above theorem, our normalization semi-procedure does not terminate, if
one applies it to a finite set of Horn clauses whose least model is not tree regular. The
least model of the finite set
S
=
{
P
(
a, a
)
⇐
, P
(
f
(
x
)
,f
(
y
))
⇐
P
(
x, y
)
}
P
(
f
i
(
a
)
,f
i
(
a
))
|
of linear Horn clauses, for instance, is
and thus not
tree regular. There are nonetheless finite sets of linear Horn clauses, whose least model
is tree regular, while our normalization semi-procedure still does not terminate. It will
for instance not terminate on the set
H
S
=
{
i
∈
N
}
S
:=
S
∪{
P
(
f
(
x
)
,y
)
⇐
P
(
x, y
)
,P
(
x, f
(
y
))
⇐
P
(
x, y
)
}
of linear Horn clauses, since
S
is a superset of
S
. Nonetheless, the least model
P
(
f
i
(
a
)
,f
j
(
a
))
|
H
S
=
{
is tree regular.
Our normalization semi-procedure can be improved in several directions. We can,
for instance, augment our normalization semi-procedure with
subsumption
, i.e., in each
normalization step we can delete
subsumed
Horn clauses. For instance, the Horn clause
H
i, j
∈
N
}
⇐B∧
Q
(
x
) is subsumed, after we apply the rule (
elim
). In the present paper we
Search WWH ::
Custom Search