41
The Semantics of Logic Programs
2.4.8 Definition Let P be a normal logic program, let I be a three-valued
model for P , and let l be an I-partial level mapping for P . We say that P
satisfies (F) with respect to I and l if each A ∈ dom(l) satisfies one of the
following conditions.
(Fi) A ∈ I, and there is a clause A ← L 1 , . . . , L n in ground(P ) such that
L i ∈ I and l(A) > l(L i ) for i = 1, . . . , n.
(Fii) ¬A ∈ I, and for each clause A ← L 1 , . . . , L n in ground(P ) there exists
i ∈ {1, . . . , n} with ¬L i ∈ I and l(A) > l(L i ).
If A ∈ dom(l) satisfies (Fi), then we say that A satisfies (Fi) with respect to I
and l, with similar terminology if A ∈ dom(l) satisfies (Fii).
2.4.9 Theorem Let P be a normal logic program with Fitting model M P .
Then, in the knowledge ordering [ k , M P is the greatest model among all
three-valued models I for which there exists an I-partial level mapping l for
P such that P satisfies (F) with respect to I and l.
Proof: We have M P = Φ P ↑ α for some ordinal α, and indeed α may be
taken to be the closure ordinal for M P . Define the M P -partial level mapping
l P : B P → α as follows: l P (A) = β, where β is the least ordinal such that
A is not undefined in Φ P ↑ (β + 1). The proof will be established by showing
the following facts. (1) P satisfies (F) with respect to M P and l P . (2) If I is
a three-valued model for P and l is an I-partial level mapping such that P
satisfies (F) with respect to I and l, then I ⊆ M P .
(1) Let A ∈ dom(l P ), and suppose that l P (A) = β. We consider the two
cases corresponding to (Fi) and (Fii).
'
Case (Fi). If A ∈ M P , then A ∈ T (Φ P ↑ β). Hence, there exists a clause
P
A ← body in ground(P ) such that body is true in Φ P ↑ β. Therefore, for all
L i ∈ body, we have that L i ∈ Φ P ↑ β, and hence l P (L i ) < β, and also that
L i ∈ M P for all i. Consequently, A satisfies (Fi) with respect to M P and l P .
Case (Fii). If ¬A ∈ M P , then A ∈ F P (Φ P ↑ β). Hence, for each clause
A ← body in ground(P ), there is a literal L ∈ body with ¬L ∈ Φ P ↑ β. But
then l P (L) < β and ¬L ∈ M P . Consequently, A satisfies (Fii) with respect to
M P and l P , and we have established that fact (1) holds.
(2) We show via transfinite induction on β = l(A) that, whenever A ∈ I,
or ¬A ∈ I, we have A ∈ Φ P ↑ (β + 1), or ¬A ∈ Φ P ↑ (β + 1)), respectively. For
the base case, note that if l(A) = 0, then A ∈ I implies that A occurs as the
head of a fact in ground(P ), hence A ∈ Φ P ↑ 1, and ¬A ∈ I implies that there
is no clause with head A in ground(P ), hence ¬A ∈ Φ P ↑ 1. So assume now
that the induction hypothesis holds for all B ∈ B P with l(B) < β and that
l(A) = β. We consider two cases.
Case i. If A ∈ I, then it satisfies (Fi) with respect to I and l. Hence, there
is a clause A ← body in ground(P ) such that body ⊆ I and l(K) < β for all
K ∈ body. Hence, body ⊆ M P by the induction hypothesis, and since M P is
a model for P , we obtain A ∈ M P .
The Semantics of Logic Programs
2.4.8 Definition Let P be a normal logic program, let I be a three-valued
model for P , and let l be an I-partial level mapping for P . We say that P
satisfies (F) with respect to I and l if each A ∈ dom(l) satisfies one of the
following conditions.
(Fi) A ∈ I, and there is a clause A ← L 1 , . . . , L n in ground(P ) such that
L i ∈ I and l(A) > l(L i ) for i = 1, . . . , n.
(Fii) ¬A ∈ I, and for each clause A ← L 1 , . . . , L n in ground(P ) there exists
i ∈ {1, . . . , n} with ¬L i ∈ I and l(A) > l(L i ).
If A ∈ dom(l) satisfies (Fi), then we say that A satisfies (Fi) with respect to I
and l, with similar terminology if A ∈ dom(l) satisfies (Fii).
2.4.9 Theorem Let P be a normal logic program with Fitting model M P .
Then, in the knowledge ordering [ k , M P is the greatest model among all
three-valued models I for which there exists an I-partial level mapping l for
P such that P satisfies (F) with respect to I and l.
Proof: We have M P = Φ P ↑ α for some ordinal α, and indeed α may be
taken to be the closure ordinal for M P . Define the M P -partial level mapping
l P : B P → α as follows: l P (A) = β, where β is the least ordinal such that
A is not undefined in Φ P ↑ (β + 1). The proof will be established by showing
the following facts. (1) P satisfies (F) with respect to M P and l P . (2) If I is
a three-valued model for P and l is an I-partial level mapping such that P
satisfies (F) with respect to I and l, then I ⊆ M P .
(1) Let A ∈ dom(l P ), and suppose that l P (A) = β. We consider the two
cases corresponding to (Fi) and (Fii).
'
Case (Fi). If A ∈ M P , then A ∈ T (Φ P ↑ β). Hence, there exists a clause
P
A ← body in ground(P ) such that body is true in Φ P ↑ β. Therefore, for all
L i ∈ body, we have that L i ∈ Φ P ↑ β, and hence l P (L i ) < β, and also that
L i ∈ M P for all i. Consequently, A satisfies (Fi) with respect to M P and l P .
Case (Fii). If ¬A ∈ M P , then A ∈ F P (Φ P ↑ β). Hence, for each clause
A ← body in ground(P ), there is a literal L ∈ body with ¬L ∈ Φ P ↑ β. But
then l P (L) < β and ¬L ∈ M P . Consequently, A satisfies (Fii) with respect to
M P and l P , and we have established that fact (1) holds.
(2) We show via transfinite induction on β = l(A) that, whenever A ∈ I,
or ¬A ∈ I, we have A ∈ Φ P ↑ (β + 1), or ¬A ∈ Φ P ↑ (β + 1)), respectively. For
the base case, note that if l(A) = 0, then A ∈ I implies that A occurs as the
head of a fact in ground(P ), hence A ∈ Φ P ↑ 1, and ¬A ∈ I implies that there
is no clause with head A in ground(P ), hence ¬A ∈ Φ P ↑ 1. So assume now
that the induction hypothesis holds for all B ∈ B P with l(B) < β and that
l(A) = β. We consider two cases.
Case i. If A ∈ I, then it satisfies (Fi) with respect to I and l. Hence, there
is a clause A ← body in ground(P ) such that body ⊆ I and l(K) < β for all
K ∈ body. Hence, body ⊆ M P by the induction hypothesis, and since M P is
a model for P , we obtain A ∈ M P .