59
The Semantics of Logic Programs
in M in Kleene’s strong three-valued logic. If (US2) holds, then some atom
in body occurs in U P (M ) and, therefore, is false in M . Consequently, body is
again false in M in Kleene’s strong three-valued logic. Hence, A ∈ F P (M ), as
required.
•
We will now show formally that the well-founded model can be characterized using Definition 2.6.1.
15
2.6.8 Theorem Let P be a normal logic program with well-founded model
M . Then, in the knowledge ordering, M is the greatest model 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.
Proof: Let M P be the well-founded model for P , and define the M P -partial
level mapping l P as follows: l P (A) = α, where α is the least ordinal such that
A is not undefined in W P ↑ (α + 1). The proof will proceed by establishing the
following facts. (1) P satisfies (WF) with respect to M P and l P . (2) If I is a
model for P and l is an I-partial level mapping such that P satisfies (WF)
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 (WFi) and (WFii).
'
Case i. A ∈ M P . Then A ∈ T P (W P ↑ α). Hence, there exists a clause
A ← body in ground(P ) such that body is true in W P ↑ α. Thus, for all
L i ∈ body, we have that L i ∈ W P ↑ α. Hence, l P (L i ) < α = l P (A) and
L i ∈ M P for all i. Consequently, A satisfies (WFi) with respect to M P and
l P .
Case ii. ¬A ∈ M P . Then A ∈ U P (W P ↑ α), and so A is contained in the
greatest unfounded set of P with respect to W P ↑ α. Hence, for each clause
A ← body in ground(P ), either (US1) or (US2) holds for this clause with
respect to W P ↑ α and the unfounded set U P (W P ↑ α). If (US1) holds, then
there exists some literal L ∈ body with ¬L ∈ W P ↑ α. Hence, l P (L) < α and
condition (WFiia) holds relative to M P and l P if L is an atom, or condition
(WFiib) holds relative to M P and l P if L is a negated atom. On the other
hand, if (US2) holds, then some (non-negated) atom B in body occurs in
U P (W P ↑ α). Hence, l P (B) ≤ l P (A), and A satisfies (WFiia) with respect to
M P and l P . Thus, we have established that the statement (1) holds.
(2) We show via transfinite induction on α = l(A) that if A ∈ I, or ¬A ∈ I,
then A ∈ W P ↑ (α + 1), or ¬A ∈ W 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 ∈ W P ↑ 1. If ¬A ∈ I, then consider the set U of all
atoms B with l(B) = 0 and ¬B ∈ I. We show that U is an unfounded set of
P with respect to W P ↑ 0, 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 ).
15 A different characterization using level mappings, which is nevertheless in the same
spirit, can be found in [Lifschitz et al., 1995].
The Semantics of Logic Programs
in M in Kleene’s strong three-valued logic. If (US2) holds, then some atom
in body occurs in U P (M ) and, therefore, is false in M . Consequently, body is
again false in M in Kleene’s strong three-valued logic. Hence, A ∈ F P (M ), as
required.
•
We will now show formally that the well-founded model can be characterized using Definition 2.6.1.
15
2.6.8 Theorem Let P be a normal logic program with well-founded model
M . Then, in the knowledge ordering, M is the greatest model 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.
Proof: Let M P be the well-founded model for P , and define the M P -partial
level mapping l P as follows: l P (A) = α, where α is the least ordinal such that
A is not undefined in W P ↑ (α + 1). The proof will proceed by establishing the
following facts. (1) P satisfies (WF) with respect to M P and l P . (2) If I is a
model for P and l is an I-partial level mapping such that P satisfies (WF)
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 (WFi) and (WFii).
'
Case i. A ∈ M P . Then A ∈ T P (W P ↑ α). Hence, there exists a clause
A ← body in ground(P ) such that body is true in W P ↑ α. Thus, for all
L i ∈ body, we have that L i ∈ W P ↑ α. Hence, l P (L i ) < α = l P (A) and
L i ∈ M P for all i. Consequently, A satisfies (WFi) with respect to M P and
l P .
Case ii. ¬A ∈ M P . Then A ∈ U P (W P ↑ α), and so A is contained in the
greatest unfounded set of P with respect to W P ↑ α. Hence, for each clause
A ← body in ground(P ), either (US1) or (US2) holds for this clause with
respect to W P ↑ α and the unfounded set U P (W P ↑ α). If (US1) holds, then
there exists some literal L ∈ body with ¬L ∈ W P ↑ α. Hence, l P (L) < α and
condition (WFiia) holds relative to M P and l P if L is an atom, or condition
(WFiib) holds relative to M P and l P if L is a negated atom. On the other
hand, if (US2) holds, then some (non-negated) atom B in body occurs in
U P (W P ↑ α). Hence, l P (B) ≤ l P (A), and A satisfies (WFiia) with respect to
M P and l P . Thus, we have established that the statement (1) holds.
(2) We show via transfinite induction on α = l(A) that if A ∈ I, or ¬A ∈ I,
then A ∈ W P ↑ (α + 1), or ¬A ∈ W 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 ∈ W P ↑ 1. If ¬A ∈ I, then consider the set U of all
atoms B with l(B) = 0 and ¬B ∈ I. We show that U is an unfounded set of
P with respect to W P ↑ 0, 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 ).
15 A different characterization using level mappings, which is nevertheless in the same
spirit, can be found in [Lifschitz et al., 1995].