55
The Semantics of Logic Programs
2.5.13 Corollary A normal logic program P is weakly stratified, that is, has
a total weakly perfect model if and only if there is a total model I for P and
a (total) level mapping l for P such that P satisfies (WS) with respect to I
and l.
The weakly perfect model is in general different from the Fitting model.
2.5.14 Proposition Let P be a program, let M 1 be its Fitting model, and
let M 2 be its (partial) weakly perfect model. Then M 1 ⊆ M 2 .
Proof: Let l 1 be an M 1 -partial level mapping such that P satisfies (F) with
respect to M 1 and l 1 . Then, trivially, P satisfies (WS) with respect to M 1 and
l 1 . Since M 2 is the largest 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, by Theorem 2.5.9, we have that M 1 ⊆ M 2 .
•
The Fitting model does not in general coincide with the (partial) weakly
perfect model, nor does it coincide in general with the perfect model for locally
stratified programs.
2.5.15 Program Let P be the program consisting of the single clause p ← p.
Then the Fitting model for P is ∅, but the (partial) weakly perfect model for
P is {¬p}. Note that P is locally stratified with perfect (two-valued) model
in which p is false.
We will see later in Section 6.3 that if P is a locally stratified program,
then P is weakly stratified, and its (total) weakly perfect model is also its
perfect model. So, the weakly perfect model semantics unifies two separate
approaches. On the one hand, it is a generalization of the Fitting semantics
and allows one to assign a single intended model to each program; on the
other hand, it generalizes the perfect model semantics for locally stratified
programs.
2.5.16 Theorem Definite programs are locally stratified and have a total
weakly perfect model.
Proof: The first statement is trivial. For the second statement, let P be a
definite program with least model I. Assign levels l(A) to all A ∈ I according
to Proposition 2.3.2, and set l(B) = 0 for all B ∈ I. Considering the characterization of the weakly perfect model from Theorem 2.5.9, we observe that
all A ∈ I satisfy (WSi), while all other atoms satisfy (WSiib), and this suffices
to establish the result.
•
The Semantics of Logic Programs
2.5.13 Corollary A normal logic program P is weakly stratified, that is, has
a total weakly perfect model if and only if there is a total model I for P and
a (total) level mapping l for P such that P satisfies (WS) with respect to I
and l.
The weakly perfect model is in general different from the Fitting model.
2.5.14 Proposition Let P be a program, let M 1 be its Fitting model, and
let M 2 be its (partial) weakly perfect model. Then M 1 ⊆ M 2 .
Proof: Let l 1 be an M 1 -partial level mapping such that P satisfies (F) with
respect to M 1 and l 1 . Then, trivially, P satisfies (WS) with respect to M 1 and
l 1 . Since M 2 is the largest 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, by Theorem 2.5.9, we have that M 1 ⊆ M 2 .
•
The Fitting model does not in general coincide with the (partial) weakly
perfect model, nor does it coincide in general with the perfect model for locally
stratified programs.
2.5.15 Program Let P be the program consisting of the single clause p ← p.
Then the Fitting model for P is ∅, but the (partial) weakly perfect model for
P is {¬p}. Note that P is locally stratified with perfect (two-valued) model
in which p is false.
We will see later in Section 6.3 that if P is a locally stratified program,
then P is weakly stratified, and its (total) weakly perfect model is also its
perfect model. So, the weakly perfect model semantics unifies two separate
approaches. On the one hand, it is a generalization of the Fitting semantics
and allows one to assign a single intended model to each program; on the
other hand, it generalizes the perfect model semantics for locally stratified
programs.
2.5.16 Theorem Definite programs are locally stratified and have a total
weakly perfect model.
Proof: The first statement is trivial. For the second statement, let P be a
definite program with least model I. Assign levels l(A) to all A ∈ I according
to Proposition 2.3.2, and set l(B) = 0 for all B ∈ I. Considering the characterization of the weakly perfect model from Theorem 2.5.9, we observe that
all A ∈ I satisfy (WSi), while all other atoms satisfy (WSiib), and this suffices
to establish the result.
•