42
Mathematical Aspects of Logic Programming Semantics
Case ii. If ¬A ∈ I, then A satisfies (Fii) with respect to I and l. Hence,
for each clause A ← body in ground(P ), there is K ∈ body with ¬K ∈ I and
l(K) < β. But then, by the induction hypothesis, we have ¬K ∈ M P , and
consequently for each clause A ← body in ground(P ) we obtain that body is
false in M P . Since M P = Φ P (M P ) is a fixed point of the Φ P -operator, we
obtain ¬A ∈ M P . This establishes Fact (2) and concludes the proof.
•
The following corollary follows immediately as a special case of the previous
result.
2.4.10 Corollary A normal logic program P has a total Fitting 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 (F) with respect to I and l.
2.4.11 Example Example 2.4.1 shows that Tweety1 (Program 2.1.2) has
total Fitting model M ∪ ¬(B Tweety1 \ M ), where M is as in Example 2.2.7.
Tweety2 (Program 2.3.9) has Fitting model
{penguin(tweety), bird(bob), bird(tweety), ¬flies(tweety)}.
Thus, we cannot decide whether or not bob is a penguin. Hence, the Fitting
semantics suffers from the same deficiency as the supported model semantics,
see our discussion of Program 2.3.9.
Tweety3 (Program 2.3.10) has ∅ as its Fitting model.
The Fitting operator is not ω-continuous in general, not even for definite
programs, as shown by the next example.
2.4.12 Program Consider the program P consisting of the following clauses.
p(s(X)) ← p(X)
q ← p(X)
A
b
Then Φ P ↑ n = ¬p s
k (0) | k < n for all n ∈ N and Φ P ↑ ω = {¬p(s
n (0)) |
n ∈ N}. However, Φ P ↑ (ω + 1) = {¬q, ¬p(s
n (0)) | n ∈ N} is the least fixed
point of the operator.
The Fitting operator can be thought of as an approximation to the immediate consequence operator, in the sense of the following proposition.
2.4.13 Proposition Let P be a program. Then for all I ∈ I P,3 , we have that
Φ P (I)
+ ⊆ T P (I
+ ) ⊆ B P \ Φ P (I)
− . Furthermore, the Fitting operator maps
total interpretations to total interpretations and coincides with the immediate
consequence operator on these.
Mathematical Aspects of Logic Programming Semantics
Case ii. If ¬A ∈ I, then A satisfies (Fii) with respect to I and l. Hence,
for each clause A ← body in ground(P ), there is K ∈ body with ¬K ∈ I and
l(K) < β. But then, by the induction hypothesis, we have ¬K ∈ M P , and
consequently for each clause A ← body in ground(P ) we obtain that body is
false in M P . Since M P = Φ P (M P ) is a fixed point of the Φ P -operator, we
obtain ¬A ∈ M P . This establishes Fact (2) and concludes the proof.
•
The following corollary follows immediately as a special case of the previous
result.
2.4.10 Corollary A normal logic program P has a total Fitting 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 (F) with respect to I and l.
2.4.11 Example Example 2.4.1 shows that Tweety1 (Program 2.1.2) has
total Fitting model M ∪ ¬(B Tweety1 \ M ), where M is as in Example 2.2.7.
Tweety2 (Program 2.3.9) has Fitting model
{penguin(tweety), bird(bob), bird(tweety), ¬flies(tweety)}.
Thus, we cannot decide whether or not bob is a penguin. Hence, the Fitting
semantics suffers from the same deficiency as the supported model semantics,
see our discussion of Program 2.3.9.
Tweety3 (Program 2.3.10) has ∅ as its Fitting model.
The Fitting operator is not ω-continuous in general, not even for definite
programs, as shown by the next example.
2.4.12 Program Consider the program P consisting of the following clauses.
p(s(X)) ← p(X)
q ← p(X)
A
b
Then Φ P ↑ n = ¬p s
k (0) | k < n for all n ∈ N and Φ P ↑ ω = {¬p(s
n (0)) |
n ∈ N}. However, Φ P ↑ (ω + 1) = {¬q, ¬p(s
n (0)) | n ∈ N} is the least fixed
point of the operator.
The Fitting operator can be thought of as an approximation to the immediate consequence operator, in the sense of the following proposition.
2.4.13 Proposition Let P be a program. Then for all I ∈ I P,3 , we have that
Φ P (I)
+ ⊆ T P (I
+ ) ⊆ B P \ Φ P (I)
− . Furthermore, the Fitting operator maps
total interpretations to total interpretations and coincides with the immediate
consequence operator on these.