32
Mathematical Aspects of Logic Programming Semantics
2.2.6 Proposition The supported interpretations for a program P are exactly the post-fixed points of T P . The supported models for P are exactly the
fixed points of T P .
Proof: Let I be a supported interpretation for P , and suppose that A ∈ I.
Then there is a clause A ← body in ground(P ) with I(body) = t. But then
A ∈ T P (I), showing that I ⊆ T P (I), as required to see that I is a post-fixed
point of T P .
Conversely, assume that I ⊆ T P (I) is a post-fixed point of T P , and let A ∈
I. Then A ∈ T P (I). Therefore, there exists a clause A ← body in ground(P )
with I(body) = t, showing that I is a supported model for P .
Finally, using Proposition 2.2.2, we obtain that an interpretation for P
is a supported model for P if and only if it is both a pre-fixed point and a
post-fixed point of T P , that is, if and only if it is a fixed point of T P .
•
2.2.7 Example Tweety1 from Program 2.1.2 has supported model M , where
M = {penguin(tweety), bird(bob), bird(tweety), flies(bob)}, as is easily
verified. Careful inspection will also convince the reader that M is the unique
supported model for Tweety1, and we give a formal proof of this in Example 5.1.7.
From a procedural point of view in the context of resolution-based logic
programming, supported models are better than minimal ones. They capture
the probable intention of a programmer who may think of a clause as a form
of equivalence
7 rather than as an implication.
Since the least model for a definite program is a fixed point, by Theorem 2.2.3, we obtain as a corollary that the least model is always supported.
In proving Theorem 2.2.3, we applied Kleene’s theorem. For normal programs,
this theorem is not applicable, nor is the Knaster-Tarski theorem, due to the
non-monotonicity of the immediate consequence operator in general. In order
to study the supported model semantics, that is, in order to obtain fixed points
of non-monotonic immediate consequence operators, it seems natural to employ fixed-point theorems for mappings which are not necessarily monotonic.
This is the main theme of Chapter 4.
2.3 Stable Models
One of the drawbacks of the supported model semantics is that definite
programs may have more than one supported model.
7 One formal approach to understanding clauses as equivalences is via the notion of the
Clark completion of a program and is related to SLDNF-resolution, see [Clark, 1978].
Mathematical Aspects of Logic Programming Semantics
2.2.6 Proposition The supported interpretations for a program P are exactly the post-fixed points of T P . The supported models for P are exactly the
fixed points of T P .
Proof: Let I be a supported interpretation for P , and suppose that A ∈ I.
Then there is a clause A ← body in ground(P ) with I(body) = t. But then
A ∈ T P (I), showing that I ⊆ T P (I), as required to see that I is a post-fixed
point of T P .
Conversely, assume that I ⊆ T P (I) is a post-fixed point of T P , and let A ∈
I. Then A ∈ T P (I). Therefore, there exists a clause A ← body in ground(P )
with I(body) = t, showing that I is a supported model for P .
Finally, using Proposition 2.2.2, we obtain that an interpretation for P
is a supported model for P if and only if it is both a pre-fixed point and a
post-fixed point of T P , that is, if and only if it is a fixed point of T P .
•
2.2.7 Example Tweety1 from Program 2.1.2 has supported model M , where
M = {penguin(tweety), bird(bob), bird(tweety), flies(bob)}, as is easily
verified. Careful inspection will also convince the reader that M is the unique
supported model for Tweety1, and we give a formal proof of this in Example 5.1.7.
From a procedural point of view in the context of resolution-based logic
programming, supported models are better than minimal ones. They capture
the probable intention of a programmer who may think of a clause as a form
of equivalence
7 rather than as an implication.
Since the least model for a definite program is a fixed point, by Theorem 2.2.3, we obtain as a corollary that the least model is always supported.
In proving Theorem 2.2.3, we applied Kleene’s theorem. For normal programs,
this theorem is not applicable, nor is the Knaster-Tarski theorem, due to the
non-monotonicity of the immediate consequence operator in general. In order
to study the supported model semantics, that is, in order to obtain fixed points
of non-monotonic immediate consequence operators, it seems natural to employ fixed-point theorems for mappings which are not necessarily monotonic.
This is the main theme of Chapter 4.
2.3 Stable Models
One of the drawbacks of the supported model semantics is that definite
programs may have more than one supported model.
7 One formal approach to understanding clauses as equivalences is via the notion of the
Clark completion of a program and is related to SLDNF-resolution, see [Clark, 1978].