33
The Semantics of Logic Programs
2.3.1 Program Let P be the program consisting of the single clause p ← p.
Then both ∅ and {p} are supported models for P .
This unsatisfactory situation is resolved by the introduction of stable models. Before we give the definition, let us make the following observation.
2.3.2 Proposition The least model T P ↑ ω for a definite program P is the
unique model M for P satisfying the following condition: there exists a mapping l : B P → α, for some ordinal α, such that for each A ∈ M there is a
clause A ← body in ground(P ) with M (body) = t and l(B) < l(A) for each
B ∈ body.
Proof: To start with, take M to be the least model T P ↑ ω, choose α = ω,
and define l : B P → α by setting l(A) = min{n | A ∈ T P ↑ (n + 1)}, if A ∈ M ,
and by setting l(A) = 0, if A ∈ M . Since ∅ ⊆ T P ↑ 1 ⊆ . . . ⊆ T P ↑ n ⊆ . . . ⊆
T P ↑ m, for each n, we see that l is well-defined and that the
T P ↑ ω = m<ω
least model T P ↑ ω for P has the desired properties.
Conversely, if M is a model for P which satisfies the given condition for
some mapping l : B P → α, then it is easy to show, by induction on l(A), that
A ∈ M implies A ∈ T P ↑ (l(A) + 1). This yields that M ⊆ T P ↑ ω and hence
that M = T P ↑ ω by minimality of the model T P ↑ ω.
•
Mappings l from B P into an ordinal are commonly called level mappings.
They will play an important role in several places in the book. On occasions,
we will need to extend such mapping to literals, and unless stated to the
contrary, we will always assume that the extension satisfies l(¬A) = l(A) for
all atoms A.
The following definition of stable model merges the property of M P just
established with that of supportedness.
8
2.3.3 Definition An interpretation I for a program P is called a wellsupported interpretation if there exists a level mapping l : B P → α, for some
ordinal α, with the property that, for each A ∈ I, there is a clause C in
ground(P ) of the form A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k such that the body of
C is true in I and l(A i ) < l(A) for i = 1, . . . , n. A well-supported model for P
is called a stable model for P .
2.3.4 Theorem The following statements hold.
(a) Every stable model is supported, but not vice-versa.
(b) Every stable model is a minimal model, but not vice-versa.
(c) Every definite program has a unique stable model, which is its least model.
8 It is shown in [Fages, 1994] that stable models can be introduced as in Definition 2.3.3.
The original formulation used the Gelfond–Lifschitz operator from Definition 2.3.6.
The Semantics of Logic Programs
2.3.1 Program Let P be the program consisting of the single clause p ← p.
Then both ∅ and {p} are supported models for P .
This unsatisfactory situation is resolved by the introduction of stable models. Before we give the definition, let us make the following observation.
2.3.2 Proposition The least model T P ↑ ω for a definite program P is the
unique model M for P satisfying the following condition: there exists a mapping l : B P → α, for some ordinal α, such that for each A ∈ M there is a
clause A ← body in ground(P ) with M (body) = t and l(B) < l(A) for each
B ∈ body.
Proof: To start with, take M to be the least model T P ↑ ω, choose α = ω,
and define l : B P → α by setting l(A) = min{n | A ∈ T P ↑ (n + 1)}, if A ∈ M ,
and by setting l(A) = 0, if A ∈ M . Since ∅ ⊆ T P ↑ 1 ⊆ . . . ⊆ T P ↑ n ⊆ . . . ⊆
T P ↑ m, for each n, we see that l is well-defined and that the
T P ↑ ω = m<ω
least model T P ↑ ω for P has the desired properties.
Conversely, if M is a model for P which satisfies the given condition for
some mapping l : B P → α, then it is easy to show, by induction on l(A), that
A ∈ M implies A ∈ T P ↑ (l(A) + 1). This yields that M ⊆ T P ↑ ω and hence
that M = T P ↑ ω by minimality of the model T P ↑ ω.
•
Mappings l from B P into an ordinal are commonly called level mappings.
They will play an important role in several places in the book. On occasions,
we will need to extend such mapping to literals, and unless stated to the
contrary, we will always assume that the extension satisfies l(¬A) = l(A) for
all atoms A.
The following definition of stable model merges the property of M P just
established with that of supportedness.
8
2.3.3 Definition An interpretation I for a program P is called a wellsupported interpretation if there exists a level mapping l : B P → α, for some
ordinal α, with the property that, for each A ∈ I, there is a clause C in
ground(P ) of the form A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k such that the body of
C is true in I and l(A i ) < l(A) for i = 1, . . . , n. A well-supported model for P
is called a stable model for P .
2.3.4 Theorem The following statements hold.
(a) Every stable model is supported, but not vice-versa.
(b) Every stable model is a minimal model, but not vice-versa.
(c) Every definite program has a unique stable model, which is its least model.
8 It is shown in [Fages, 1994] that stable models can be introduced as in Definition 2.3.3.
The original formulation used the Gelfond–Lifschitz operator from Definition 2.3.6.