175
Stable and Perfect Model Semantics
Let P be a program with total well-founded model I ∪¬(B P \I),
where I ⊆ B P . Then GL P is strictly contracting on the spherically complete dislocated generalized ultrametric space (I P , �),
where we have �(J, K) = max{d l (J, I), d l (I, K)} for all J, K ∈
I P , and l is defined by taking l(A) to be the minimal α such
that Φ fix(P ) ↑ (α + 1)(A) = I(A).
Indeed, the program P has a total well-founded model in this case, and this
implies that fix(P ) has a total Fitting model. So l as just defined is, in fact,
well-defined, and fix(P ) satisfies (F) with respect to I ∪ ¬(B P \ I) and l. Now
apply Theorem 5.1.17.
6.3 Perfect Model Semantics
We return to matters of stratification and the perfect model semantics.
More precisely, we will describe an iterative method for obtaining the perfect
model for locally stratified programs.
5
6.3.1 Definition Let P be a normal logic program, and let l : B P → γ be a
level mapping, where γ > 1. For each n satisfying 0 < n ≤ γ, let P [n] denote
the set of all clauses in ground(P ) in which only atoms A with l(A) < n occur,
and denote by L n the set of all atoms A of level l(A) less than n. We define
T [n] : P(L n ) → P(L n ) by T [n] (I) = T P [n] (I). The mapping T [n] is called the
immediate consequence operator restricted at level n.
Thus, the idea formalized by this definition is to “cut-off” at level n.
6.3.2 Definition Let P be a locally stratified normal logic program, and let
l : B P → γ be a level mapping, where γ > 1. We construct the transfinite
sequence (I n ) n∈γ inductively as follows. For each m ∈ N, we put I [1,m] =
∞
T
m (∅) and set I 1 =
I [1,m] . If n ∈ γ, where n > 1, is a successor ordinal,
[1]
m=0
∞
then for each m ∈ N we put I [n,m] = T
m (I n−1 ) and set I n =
I [n,m] . If
[n]
m=0
n ∈ γ is a limit ordinal, we put I n =
I m . Finally, we put I [P ] =
I n .
m
6.3.3 Example Consider again the example program Tweety2, Program 2.3.9, where penguin(X) is assigned level 0, bird(X) is assigned level
1, and flies(X) is assigned level 2, for all X ∈ {tweety, bob}. We obtain the
5 For further details, we refer the reader to the paper [Seda and Hitzler, 1999b].
Stable and Perfect Model Semantics
Let P be a program with total well-founded model I ∪¬(B P \I),
where I ⊆ B P . Then GL P is strictly contracting on the spherically complete dislocated generalized ultrametric space (I P , �),
where we have �(J, K) = max{d l (J, I), d l (I, K)} for all J, K ∈
I P , and l is defined by taking l(A) to be the minimal α such
that Φ fix(P ) ↑ (α + 1)(A) = I(A).
Indeed, the program P has a total well-founded model in this case, and this
implies that fix(P ) has a total Fitting model. So l as just defined is, in fact,
well-defined, and fix(P ) satisfies (F) with respect to I ∪ ¬(B P \ I) and l. Now
apply Theorem 5.1.17.
6.3 Perfect Model Semantics
We return to matters of stratification and the perfect model semantics.
More precisely, we will describe an iterative method for obtaining the perfect
model for locally stratified programs.
5
6.3.1 Definition Let P be a normal logic program, and let l : B P → γ be a
level mapping, where γ > 1. For each n satisfying 0 < n ≤ γ, let P [n] denote
the set of all clauses in ground(P ) in which only atoms A with l(A) < n occur,
and denote by L n the set of all atoms A of level l(A) less than n. We define
T [n] : P(L n ) → P(L n ) by T [n] (I) = T P [n] (I). The mapping T [n] is called the
immediate consequence operator restricted at level n.
Thus, the idea formalized by this definition is to “cut-off” at level n.
6.3.2 Definition Let P be a locally stratified normal logic program, and let
l : B P → γ be a level mapping, where γ > 1. We construct the transfinite
sequence (I n ) n∈γ inductively as follows. For each m ∈ N, we put I [1,m] =
∞
T
m (∅) and set I 1 =
I [1,m] . If n ∈ γ, where n > 1, is a successor ordinal,
[1]
m=0
∞
then for each m ∈ N we put I [n,m] = T
m (I n−1 ) and set I n =
I [n,m] . If
[n]
m=0
n ∈ γ is a limit ordinal, we put I n =
I m . Finally, we put I [P ] =
I n .
m
6.3.3 Example Consider again the example program Tweety2, Program 2.3.9, where penguin(X) is assigned level 0, bird(X) is assigned level
1, and flies(X) is assigned level 2, for all X ∈ {tweety, bob}. We obtain the
5 For further details, we refer the reader to the paper [Seda and Hitzler, 1999b].