157
Supported Model Semantics
5.2.10 Theorem Let P be a normal logic program, and let M be the least
fixed point of the operator Φ P,3,2 . Then, in the knowledge ordering, M is the
greatest model among all three-valued models I for which there exists an Ipartial level mapping l for P such that P satisfies (F 32 ) with respect to I and
l.
Proof: Let M P be the least fixed point of the operator Φ P,3,2 , 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 Φ P ↑ (α + 1). The proof proceeds by
established the following facts. (1) P satisfies (F 32 ) with respect to M 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 32 ) with respect to I and l, then I ⊆ M P .
(1) Let A ∈ dom(l P ), and suppose that l P (A) = α. We consider two cases.
Case i. If A ∈ M P , then Table 5.1 together with the definition of l P yields
that A satisfies (Fi) with respect to M P and l P . It also yields that l(L) < α
for each literal L in the body of any clause from ground(P ) with head A.
Case ii. If ¬A ∈ M P , then again Table 5.1 together with the definition of
l P yields that A satisfies (Fii) with respect to M P and l P . As before, it also
yields l(L) < α for each literal L in the body of any clause from ground(P )
with head A. This completes the proof of (1).
(2) Similarly to the proof of Step (2) in the proof of Theorem 2.4.9, it can
be shown via transfinite induction on α = l(A) that: whenever A ∈ I we have
A ∈ Φ P,3,2 ↑ (α + 1) and whenever ¬A ∈ I we have ¬A ∈ Φ P,3,2 ↑ (α + 1). This
concludes the proof.
•
5.2.11 Corollary A logic program P is acyclic if and only if Φ P,3,2 ↑ ω is
total, and is locally hierarchical if and only if Φ P,3,2 ↑ α is total for some
ordinal α.
Proof: Let P be such that Φ P,3,2 ↑ α is total for some α. Then by Theorem
5.2.10 and Definition 5.2.9 it follows that P is locally hierarchical with respect
to the level mapping l P as defined in the proof of Theorem 5.2.10.
Conversely, let P be locally hierarchical with level mapping l. Then, by
Theorem 5.1.6, P has a unique supported model M , that is, M is the unique
fixed point of the operator T P . We show that P satisfies (F 32 ) with respect to
I = M ∪ ¬(B P \ M ) and l. For this it suffices to show that for each A ∈ B P ,
conditions (Fi) and (Fii) hold with respect to I. This, however, is an immediate
consequence of the fact that M is a fixed point of T P and that P is locally
hierarchical.
The argument to show that P is acyclic if and only if Φ P,3,2 ↑ ω is total is
similar.
•
Supported Model Semantics
5.2.10 Theorem Let P be a normal logic program, and let M be the least
fixed point of the operator Φ P,3,2 . Then, in the knowledge ordering, M is the
greatest model among all three-valued models I for which there exists an Ipartial level mapping l for P such that P satisfies (F 32 ) with respect to I and
l.
Proof: Let M P be the least fixed point of the operator Φ P,3,2 , 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 Φ P ↑ (α + 1). The proof proceeds by
established the following facts. (1) P satisfies (F 32 ) with respect to M 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 32 ) with respect to I and l, then I ⊆ M P .
(1) Let A ∈ dom(l P ), and suppose that l P (A) = α. We consider two cases.
Case i. If A ∈ M P , then Table 5.1 together with the definition of l P yields
that A satisfies (Fi) with respect to M P and l P . It also yields that l(L) < α
for each literal L in the body of any clause from ground(P ) with head A.
Case ii. If ¬A ∈ M P , then again Table 5.1 together with the definition of
l P yields that A satisfies (Fii) with respect to M P and l P . As before, it also
yields l(L) < α for each literal L in the body of any clause from ground(P )
with head A. This completes the proof of (1).
(2) Similarly to the proof of Step (2) in the proof of Theorem 2.4.9, it can
be shown via transfinite induction on α = l(A) that: whenever A ∈ I we have
A ∈ Φ P,3,2 ↑ (α + 1) and whenever ¬A ∈ I we have ¬A ∈ Φ P,3,2 ↑ (α + 1). This
concludes the proof.
•
5.2.11 Corollary A logic program P is acyclic if and only if Φ P,3,2 ↑ ω is
total, and is locally hierarchical if and only if Φ P,3,2 ↑ α is total for some
ordinal α.
Proof: Let P be such that Φ P,3,2 ↑ α is total for some α. Then by Theorem
5.2.10 and Definition 5.2.9 it follows that P is locally hierarchical with respect
to the level mapping l P as defined in the proof of Theorem 5.2.10.
Conversely, let P be locally hierarchical with level mapping l. Then, by
Theorem 5.1.6, P has a unique supported model M , that is, M is the unique
fixed point of the operator T P . We show that P satisfies (F 32 ) with respect to
I = M ∪ ¬(B P \ M ) and l. For this it suffices to show that for each A ∈ B P ,
conditions (Fi) and (Fii) hold with respect to I. This, however, is an immediate
consequence of the fact that M is a fixed point of T P and that P is locally
hierarchical.
The argument to show that P is acyclic if and only if Φ P,3,2 ↑ ω is total is
similar.
•