Chapter 5
Supported Model Semantics
Among the various semantics for normal logic programs discussed in Chapter
2, the supported model semantics, whether in two-valued or in three-valued
form, is most fundamental: stable and perfect models are two-valued supported models; and well-founded and weakly perfect models are three-valued
supported models. Furthermore, as shown in Theorem 2.6.14, if the Fitting
model for a program P is total, then P has a unique two-valued supported
model which coincides with the unique model assigned to P by the Fitting,
the well-founded, the weakly perfect, and the stable semantics: the semantics
in this case is unambiguous.
Programs which have unique supported models together with those which
have total Fitting models can therefore be considered to be of fundamental
importance for understanding logic programming semantics as presented in
Chapter 2. The former, namely, programs with unique supported models, are
called by us uniquely determined , while we call the latter Φ-accessible programs. We know from Theorem 2.6.14, as just noted, that every Φ-accessible
program has a unique supported model. The converse, however, is not true in
general, as the following example shows.
5.0.1 Program The program
p ← p
p ← ¬p
has a unique supported model {p} and Fitting model ∅.
In this chapter, we study supported models in two-valued and three-valued
logic, with particular emphasis on uniquely determined and Φ-accessible programs. In particular, in Section 5.1 we consider two-valued supported models
and apply generalized metric fixed-point theorems from Chapter 4 in order
to show that certain classes of programs are uniquely determined. As is to
be expected, more general fixed-point theorems allow the treatment of more
general classes of programs, so that the hierarchy of fixed-point theorems from
Section 4.7 gives rise to a hierarchy of program classes, each of which has the
property that all programs in the class have unique supported models. Such
program classes are consequently called unique supported model classes.
The same hierarchy of unique supported model classes will be considered
139
Supported Model Semantics
Among the various semantics for normal logic programs discussed in Chapter
2, the supported model semantics, whether in two-valued or in three-valued
form, is most fundamental: stable and perfect models are two-valued supported models; and well-founded and weakly perfect models are three-valued
supported models. Furthermore, as shown in Theorem 2.6.14, if the Fitting
model for a program P is total, then P has a unique two-valued supported
model which coincides with the unique model assigned to P by the Fitting,
the well-founded, the weakly perfect, and the stable semantics: the semantics
in this case is unambiguous.
Programs which have unique supported models together with those which
have total Fitting models can therefore be considered to be of fundamental
importance for understanding logic programming semantics as presented in
Chapter 2. The former, namely, programs with unique supported models, are
called by us uniquely determined , while we call the latter Φ-accessible programs. We know from Theorem 2.6.14, as just noted, that every Φ-accessible
program has a unique supported model. The converse, however, is not true in
general, as the following example shows.
5.0.1 Program The program
p ← p
p ← ¬p
has a unique supported model {p} and Fitting model ∅.
In this chapter, we study supported models in two-valued and three-valued
logic, with particular emphasis on uniquely determined and Φ-accessible programs. In particular, in Section 5.1 we consider two-valued supported models
and apply generalized metric fixed-point theorems from Chapter 4 in order
to show that certain classes of programs are uniquely determined. As is to
be expected, more general fixed-point theorems allow the treatment of more
general classes of programs, so that the hierarchy of fixed-point theorems from
Section 4.7 gives rise to a hierarchy of program classes, each of which has the
property that all programs in the class have unique supported models. Such
program classes are consequently called unique supported model classes.
The same hierarchy of unique supported model classes will be considered
139