60
Mathematical Aspects of Logic Programming Semantics
Since ¬C ∈ I, and l(C) = 0, we have that C satisfies (WFiia) with respect to
I and l, and so condition (US2) is satisfied showing that U is an unfounded
set of P with respect to I. Assume now that the induction hypothesis holds
for all B ∈ B P with l(B) < α. We consider two cases.
Case i. A ∈ I. Then A satisfies (WFi) 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 ⊆ W P ↑ α, and we obtain A ∈ T (W P ↑ α), as
P
required.
Case ii. ¬A ∈ I. Consider the set U of all atoms B with l(B) = α and
¬B ∈ I. We show that U is an unfounded set of P with respect to W P ↑ α,
and this suffices since it implies ¬A ∈ W P ↑ (α + 1) by the fact that A ∈ U .
So let C ∈ U , and let C ← body be a clause in ground(P ). Since ¬C ∈ I,
we have that C satisfies (WFii) with respect to I and l. If there is a literal
L ∈ body with ¬L ∈ I and l(L) < l(C), then by the induction hypothesis
we obtain ¬L ∈ W P ↑ α, and therefore condition (US1) is satisfied for the
clause C ← body with respect to W P ↑ α and U . In the remaining case, we
have that C satisfies condition (WFiia), and there exists an atom B ∈ body
with ¬B ∈ I and l(B) = l(C). Hence, B ∈ U showing that condition (US2) is
satisfied for the clause C ← body with respect to W P ↑ α and U . Hence, U is
an unfounded set of P with respect to W P ↑ α.
•
As a special case, we immediately obtain the following corollary.
2.6.9 Corollary A normal logic program P has a total well-founded model
if and only if there is a total model I for P and a (total) level mapping l such
that P satisfies (WF) with respect to I and l.
The well-founded model is in general different from the weakly perfect
model, but always contains it.
2.6.10 Proposition Let P be a program, let M 1 be its (partial) weakly perfect model, and let M 2 be its well-founded model. Then M 1 ⊆ M 2 .
Proof: Let l 1 be an M 1 -partial level mapping such that P satisfies (WS) with
respect to M 1 and l 1 . Then P satisfies (WF) with respect to M 1 and l 1 , as
noted earlier. By Theorem 2.6.8, M 2 is largest among all models I for which
there exists an I-partial level mapping l for P such that P satisfies (WF) with
respect to I and l, and hence M 1 ⊆ M 2 .
•
2.6.11 Program Let P be the program consisting of the two clauses
p ← q, ¬p
q ← p
Then the reduct P 1 of P with respect to the empty set is P itself, that is,
Mathematical Aspects of Logic Programming Semantics
Since ¬C ∈ I, and l(C) = 0, we have that C satisfies (WFiia) with respect to
I and l, and so condition (US2) is satisfied showing that U is an unfounded
set of P with respect to I. Assume now that the induction hypothesis holds
for all B ∈ B P with l(B) < α. We consider two cases.
Case i. A ∈ I. Then A satisfies (WFi) 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 ⊆ W P ↑ α, and we obtain A ∈ T (W P ↑ α), as
P
required.
Case ii. ¬A ∈ I. Consider the set U of all atoms B with l(B) = α and
¬B ∈ I. We show that U is an unfounded set of P with respect to W P ↑ α,
and this suffices since it implies ¬A ∈ W P ↑ (α + 1) by the fact that A ∈ U .
So let C ∈ U , and let C ← body be a clause in ground(P ). Since ¬C ∈ I,
we have that C satisfies (WFii) with respect to I and l. If there is a literal
L ∈ body with ¬L ∈ I and l(L) < l(C), then by the induction hypothesis
we obtain ¬L ∈ W P ↑ α, and therefore condition (US1) is satisfied for the
clause C ← body with respect to W P ↑ α and U . In the remaining case, we
have that C satisfies condition (WFiia), and there exists an atom B ∈ body
with ¬B ∈ I and l(B) = l(C). Hence, B ∈ U showing that condition (US2) is
satisfied for the clause C ← body with respect to W P ↑ α and U . Hence, U is
an unfounded set of P with respect to W P ↑ α.
•
As a special case, we immediately obtain the following corollary.
2.6.9 Corollary A normal logic program P has a total well-founded model
if and only if there is a total model I for P and a (total) level mapping l such
that P satisfies (WF) with respect to I and l.
The well-founded model is in general different from the weakly perfect
model, but always contains it.
2.6.10 Proposition Let P be a program, let M 1 be its (partial) weakly perfect model, and let M 2 be its well-founded model. Then M 1 ⊆ M 2 .
Proof: Let l 1 be an M 1 -partial level mapping such that P satisfies (WS) with
respect to M 1 and l 1 . Then P satisfies (WF) with respect to M 1 and l 1 , as
noted earlier. By Theorem 2.6.8, M 2 is largest among all models I for which
there exists an I-partial level mapping l for P such that P satisfies (WF) with
respect to I and l, and hence M 1 ⊆ M 2 .
•
2.6.11 Program Let P be the program consisting of the two clauses
p ← q, ¬p
q ← p
Then the reduct P 1 of P with respect to the empty set is P itself, that is,