183
Stable and Perfect Model Semantics
established in Corollary 6.3.5 (a) and define the level mapping l mapping to
pairs of ordinals as follows. For A ∈ I [P ] let l(A) = (l
' (A), m), where m is
least such that A ∈ I [l / (A)+1,m+1] . For A ∈ I [P ] let l(A) = (l
' (A) + 1, 0). The
recursion equations from Corollary 6.3.5 (a) together with the fact that P is
locally stratified thus allow us to conclude that (WSi), (WSiib), or (WSiic)
is always satisfied with respect to I [P ] and l. Since I [P ] is total, we obtain by
A
b
Theorem 2.5.9 that I [P ] ∪ B P \ I [P ] is the (total) weakly perfect model for
P . Since every program has only one weakly perfect model, and we have just
seen that the weakly perfect model for P coincides with I [P ] , we conclude that
the model I [P ] as constructed by Theorem 6.3.7 is independent of the choice
of level mapping with respect to which P is locally stratified.
•
6.3.12 Example Consider Tweety2 from Example 2.5.3 again. It is (locally)
stratified with respect to the level mapping given in Example 6.3.3. We calculate the perfect model for Tweety2 by employing powers of the operator T P
as discussed just prior to the statement of Theorem 6.3.9. Indeed, with the
notation used there, we obtain
M 1 = {penguin(tweety)},

M 2 = {bird(bob), bird(tweety), penguin(tweety)},

M 3 = M Tweety2 , and

M 4 = M 3.

As discussed in Example 2.5.3, the latter model is the perfect model for
Tweety2.