Chapter 6
Stable and Perfect Model Semantics
The stable model semantics turns out to be the one which receives the most
attention these days. Some of the most popular implementations of nonmonotonic reasoning systems are based on it.
1 In this chapter, we provide
means to lift our results on the supported model semantics to the stable
model semantics. This is done by the so-called fixpoint completion of programs, which we will introduce in Section 6.1. This construction will enable
us to draw almost effortlessly a number of corollaries on the stable model
semantics, and we will do this in Section 6.2. Finally, in Section 6.3, we will
close our discussion with some additional observations on stratification and
the perfect model semantics.
6.1 The Fixpoint Completion
The fixpoint completion is a program transformation which is based on
the notion of unfolding, meaning the replacement of a body atom A by the
body of a clause which also has head A. In essence, the fixpoint completion of
a given program is obtained by performing (recursively) a complete unfolding
through all positive body atoms and disregarding all clauses which after this
process still contain positive body atoms. We will describe this formally in the
following definition.
6.1.1 Definition A quasi-interpretation
2 is a set of clauses of the form
A ← ¬B 1 , . . . , ¬B m , where A and B i are ground atoms for all i = 1, . . . , m.
Given a normal logic program P and a quasi-interpretation Q, we define
'
T (Q) to be the quasi-interpretation consisting of the set of all clauses
P
A ← body 1 , . . . , body , ¬B 1 , . . . , ¬B m for which there exists a clause A ←
n
A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(P ) and clauses A i ← body i in Q for all
i = 1, . . . , n. We explicitly allow the cases n = 0 or m = 0 in this definition.
1 See [Leone et al., 2006] for details of the DLV system and [Simons et al., 2002] for details
of the smodels system, for example.
2 This notion is due to [Dung and Kanchanasut, 1989]. We stick to the old terminology,
although quasi-interpretations should really be thought of as, and indeed are, programs
with negative body literals only.
169
Stable and Perfect Model Semantics
The stable model semantics turns out to be the one which receives the most
attention these days. Some of the most popular implementations of nonmonotonic reasoning systems are based on it.
1 In this chapter, we provide
means to lift our results on the supported model semantics to the stable
model semantics. This is done by the so-called fixpoint completion of programs, which we will introduce in Section 6.1. This construction will enable
us to draw almost effortlessly a number of corollaries on the stable model
semantics, and we will do this in Section 6.2. Finally, in Section 6.3, we will
close our discussion with some additional observations on stratification and
the perfect model semantics.
6.1 The Fixpoint Completion
The fixpoint completion is a program transformation which is based on
the notion of unfolding, meaning the replacement of a body atom A by the
body of a clause which also has head A. In essence, the fixpoint completion of
a given program is obtained by performing (recursively) a complete unfolding
through all positive body atoms and disregarding all clauses which after this
process still contain positive body atoms. We will describe this formally in the
following definition.
6.1.1 Definition A quasi-interpretation
2 is a set of clauses of the form
A ← ¬B 1 , . . . , ¬B m , where A and B i are ground atoms for all i = 1, . . . , m.
Given a normal logic program P and a quasi-interpretation Q, we define
'
T (Q) to be the quasi-interpretation consisting of the set of all clauses
P
A ← body 1 , . . . , body , ¬B 1 , . . . , ¬B m for which there exists a clause A ←
n
A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(P ) and clauses A i ← body i in Q for all
i = 1, . . . , n. We explicitly allow the cases n = 0 or m = 0 in this definition.
1 See [Leone et al., 2006] for details of the DLV system and [Simons et al., 2002] for details
of the smodels system, for example.
2 This notion is due to [Dung and Kanchanasut, 1989]. We stick to the old terminology,
although quasi-interpretations should really be thought of as, and indeed are, programs
with negative body literals only.
169