50
Mathematical Aspects of Logic Programming Semantics
M P . Then, in the knowledge ordering [ k , M P is the greatest model among all
models I for which there exists an I-partial level mapping l for P such that
P satisfies (WS) with respect to I and l.
We prepare for the proof of Theorem 2.5.9 by introducing some notation
which will help make the presentation transparent.
It will be convenient to consider level mappings which map into pairs (β, n)
of ordinals, where n ≤ ω. So let α be a (countable) ordinal, and consider the
set A of all pairs (β, n), where β < α and n ≤ ω. Of course, A endowed with
the lexicographic ordering is isomorphic to an ordinal. So any mapping from
B P to A can be considered to be a level mapping.
Let P be a program with (partial) weakly perfect model M P . We define
the M P -partial level mapping l P as follows: l P (A) = (β, n), where A ∈ S β ∪R β
and n is least with A ∈ T L β ↑ (n + 1), if such an n exists, and n = ω otherwise.
We observe that if l P (A) = l P (B), then there exists α with A, B ∈ S α ∪ R α ,
and if A ∈ S α ∪ R α and B ∈ S β ∪ R β with α < β, then l(A) < l(B).
The following notion will help to ease later notation.
2.5.10 Definition Let P and Q be two programs, and let I be an interpretation.
(1) Suppose that C 1 = (A ← L 1 , . . . , L n ) and C 2 = (B ← K 1 , . . . , K m ) are
two clauses. Then we say that C 1 subsumes C 2 , written C 1 � C 2 , if A = B
and {L 1 , . . . , L n } ⊆ {K 1 , . . . , K m }.
(2) We say that P subsumes Q, written P � Q, if for each clause C 1 in P
there exists a clause C 2 in Q with C 1 � C 2 .
(3) We say that P subsumes Q model-consistently (with respect to I), written
P � I Q, if the following conditions hold.
(i) For each clause C 1 = (A ← L 1 , . . . , L n ) in P , there exists a clause
C 2 = (B ← K 1 , . . . , K m ) in Q with C 1 � C 2 and {K 1 , . . . , K m } \
{L 1 , . . . , L n } ⊆ I.
(ii) For each clause C 2 = (B ← K 1 , . . . , K m ) in Q which satisfies
{K 1 , . . . , K m } ⊆ I and B ∈ I, there exists a clause C 1 in P such
that C 1 � C 2 .
Definition 2.5.10 will facilitate the proof of Theorem 2.5.9 by employing
the following lemma.
2.5.11 Lemma With the notation established in Definition 2.5.4, we have
P/N α � Nα P for all α.
Proof: Condition 3(i) of Definition 2.5.10 holds because every clause C 1 =
(A ← L 1 , . . . , L n ) in P/N α is obtained from a clause C 2 = (A ← K 1 , . . . , K m )
in P by deleting body literals which are contained in N α . Clearly, C 1 � C 2 ,
Mathematical Aspects of Logic Programming Semantics
M P . Then, in the knowledge ordering [ k , M P is the greatest model among all
models I for which there exists an I-partial level mapping l for P such that
P satisfies (WS) with respect to I and l.
We prepare for the proof of Theorem 2.5.9 by introducing some notation
which will help make the presentation transparent.
It will be convenient to consider level mappings which map into pairs (β, n)
of ordinals, where n ≤ ω. So let α be a (countable) ordinal, and consider the
set A of all pairs (β, n), where β < α and n ≤ ω. Of course, A endowed with
the lexicographic ordering is isomorphic to an ordinal. So any mapping from
B P to A can be considered to be a level mapping.
Let P be a program with (partial) weakly perfect model M P . We define
the M P -partial level mapping l P as follows: l P (A) = (β, n), where A ∈ S β ∪R β
and n is least with A ∈ T L β ↑ (n + 1), if such an n exists, and n = ω otherwise.
We observe that if l P (A) = l P (B), then there exists α with A, B ∈ S α ∪ R α ,
and if A ∈ S α ∪ R α and B ∈ S β ∪ R β with α < β, then l(A) < l(B).
The following notion will help to ease later notation.
2.5.10 Definition Let P and Q be two programs, and let I be an interpretation.
(1) Suppose that C 1 = (A ← L 1 , . . . , L n ) and C 2 = (B ← K 1 , . . . , K m ) are
two clauses. Then we say that C 1 subsumes C 2 , written C 1 � C 2 , if A = B
and {L 1 , . . . , L n } ⊆ {K 1 , . . . , K m }.
(2) We say that P subsumes Q, written P � Q, if for each clause C 1 in P
there exists a clause C 2 in Q with C 1 � C 2 .
(3) We say that P subsumes Q model-consistently (with respect to I), written
P � I Q, if the following conditions hold.
(i) For each clause C 1 = (A ← L 1 , . . . , L n ) in P , there exists a clause
C 2 = (B ← K 1 , . . . , K m ) in Q with C 1 � C 2 and {K 1 , . . . , K m } \
{L 1 , . . . , L n } ⊆ I.
(ii) For each clause C 2 = (B ← K 1 , . . . , K m ) in Q which satisfies
{K 1 , . . . , K m } ⊆ I and B ∈ I, there exists a clause C 1 in P such
that C 1 � C 2 .
Definition 2.5.10 will facilitate the proof of Theorem 2.5.9 by employing
the following lemma.
2.5.11 Lemma With the notation established in Definition 2.5.4, we have
P/N α � Nα P for all α.
Proof: Condition 3(i) of Definition 2.5.10 holds because every clause C 1 =
(A ← L 1 , . . . , L n ) in P/N α is obtained from a clause C 2 = (A ← K 1 , . . . , K m )
in P by deleting body literals which are contained in N α . Clearly, C 1 � C 2 ,