159
Supported Model Semantics
5.2.4 Φ ∗ -Accessible Programs
We next give the analogue of Definition 5.2.9 for Φ
∗ -accessible programs.
In order to make it more concise, we have chosen to rearrange the statements
of the conditions slightly. The reader will easily identify the parts which correspond to conditions (Fi) and (Fii).
5.2.15 Definition Let P be a normal logic program, let I be a model for P ,
and let l be an I-partial level mapping for P . We say that P satisfies (F 12 ) with
respect to I and l if for each A ∈ dom(l) and for all clauses A ← L 1 , . . . , L n
one of the following conditions (F 12 i), (F 12 ii) holds. Furthermore, if A ∈ I,
there must be at least one clause which satisfies (F 12 i), and if ¬A ∈ I, there
must be no clauses which satisfy (F 12 i).
(F 12 i) L i ∈ I and l(A) > l(L i ) for all i.
(F 12 ii) There exists i with ¬L i ∈ I and l(A) > l(L i ).
The proof of the following theorem is very similar to the proof of Theorem
5.2.10 and is therefore omitted.
5.2.16 Theorem Let P be a normal logic program, and let M be the least
fixed point of the operator Φ P,1,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 12 ) with respect to I and
l.
The proof of the following corollary is similar to the proof of Corollary
5.2.14 and is therefore omitted.
5.2.17 Corollary A normal logic program P is Φ
∗ -accessible if and only if
Φ P,1,2 ↑ α is total for some ordinal α.
5.2.5 Φ-Accessible Programs
Results for Φ-accessible programs corresponding to those for Φ
∗ -accessible
programs in Section 5.2.4 have already been obtained, and we refrain from
repeating them here. Theorem 5.2.16 finds its analogue in Theorem 2.4.9, and
the analogue of Corollary 5.2.17 can be found in Definition 5.1.15.
5.3 A Hierarchy of Logic Programs
In Figure 5.1, we present an overview of the relationships between the
main classes of normal logic programs discussed in this book. Note that different branches of the graph shown are not necessarily disjoint. For example,
Supported Model Semantics
5.2.4 Φ ∗ -Accessible Programs
We next give the analogue of Definition 5.2.9 for Φ
∗ -accessible programs.
In order to make it more concise, we have chosen to rearrange the statements
of the conditions slightly. The reader will easily identify the parts which correspond to conditions (Fi) and (Fii).
5.2.15 Definition Let P be a normal logic program, let I be a model for P ,
and let l be an I-partial level mapping for P . We say that P satisfies (F 12 ) with
respect to I and l if for each A ∈ dom(l) and for all clauses A ← L 1 , . . . , L n
one of the following conditions (F 12 i), (F 12 ii) holds. Furthermore, if A ∈ I,
there must be at least one clause which satisfies (F 12 i), and if ¬A ∈ I, there
must be no clauses which satisfy (F 12 i).
(F 12 i) L i ∈ I and l(A) > l(L i ) for all i.
(F 12 ii) There exists i with ¬L i ∈ I and l(A) > l(L i ).
The proof of the following theorem is very similar to the proof of Theorem
5.2.10 and is therefore omitted.
5.2.16 Theorem Let P be a normal logic program, and let M be the least
fixed point of the operator Φ P,1,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 12 ) with respect to I and
l.
The proof of the following corollary is similar to the proof of Corollary
5.2.14 and is therefore omitted.
5.2.17 Corollary A normal logic program P is Φ
∗ -accessible if and only if
Φ P,1,2 ↑ α is total for some ordinal α.
5.2.5 Φ-Accessible Programs
Results for Φ-accessible programs corresponding to those for Φ
∗ -accessible
programs in Section 5.2.4 have already been obtained, and we refrain from
repeating them here. Theorem 5.2.16 finds its analogue in Theorem 2.4.9, and
the analogue of Corollary 5.2.17 can be found in Definition 5.1.15.
5.3 A Hierarchy of Logic Programs
In Figure 5.1, we present an overview of the relationships between the
main classes of normal logic programs discussed in this book. Note that different branches of the graph shown are not necessarily disjoint. For example,