45
The Semantics of Logic Programs
2.5.3 Example Tweety2 (Program 2.3.9) is locally stratified, indeed stratified, since flies depends both on penguin and on bird, where “depends
on” is defined below, bird depends only on penguin, and penguin does not
depend on any predicate symbol other than itself. We will see in Example
6.3.12 that it has M from Example 2.2.7 as its perfect model.
Tweety3 (Program 2.3.10) is obviously not locally stratified.
We will see later in Section 6.3 that every locally stratified program has
a unique perfect model and that this model is independent of the choice of
the level mapping with respect to which the program is locally stratified. In
fact, we are more interested here in a generalization of the perfect model
semantics to three-valued logic, and of course the objective underlying this
generalization is the usual one, namely, to provide a single intended model for
each given program.
We will proceed next with presenting the rather involved definition of the
weakly perfect model due to Przymusinska and Przymusinski.
12 For ease of
notation, it will be convenient to consider (countably infinite) propositional
programs instead of programs over a first-order language, and we recall that
we have already observed in Section 2.1 that this results in no loss of generality
for our purposes.
Let P be a (countably infinite propositional) normal logic program. We
say that an atom A ∈ B P refers to an atom B ∈ B P if either B or ¬B occurs
as a body literal in a clause A ← body in P with head A. We say that A refers
negatively to B if ¬B occurs as a body literal in such a clause. We say that A
depends on B, written B ≤ A, if the pair (A, B) is in the transitive closure of
the relation refers to. We say that A depends negatively on B, written B < A,
if there are C, D ∈ B P such that C refers negatively to D and the following
conditions hold: (1) C ≤ A or C = A (the latter meaning identity), and (2)
B ≤ D or B = D. For A, B ∈ B P , we write A ∼ B if either A = B or A and B
depend negatively on each other, so that A < B and B < A both hold in this
latter case.
13 The relation ∼ is an equivalence relation, and its equivalence
classes are called components of P . A component is trivial if it consists of a
single element A with A < A.
Notice that the definitions above can be viewed in a rather intuitive way
by means of the dependency graph G P of a program P , defined as follows. The
vertices of G P are the ground atoms appearing in P ; for each clause A ← body
in ground(P ) there is a positive directed edge in G P from B to A if B occurs
in body, and there is a negative directed edge from B to A in G P if ¬B occurs
in body. Then, in these terms, we have B ≤ A if and only if there is a directed
path in G P from B to A, and we have B < A if and only if there is a directed
path in G P from B to A passing through a negative edge.
12 The notions of weak stratification and the weakly perfect model were introduced in the
paper [Przymusinska and Przymusinski, 1990].
13 It is noted in [Przymusinska and Przymusinski, 1990] that such mutual recursion is the
primary cause of difficulties in defining declarative semantics for logic programs.
The Semantics of Logic Programs
2.5.3 Example Tweety2 (Program 2.3.9) is locally stratified, indeed stratified, since flies depends both on penguin and on bird, where “depends
on” is defined below, bird depends only on penguin, and penguin does not
depend on any predicate symbol other than itself. We will see in Example
6.3.12 that it has M from Example 2.2.7 as its perfect model.
Tweety3 (Program 2.3.10) is obviously not locally stratified.
We will see later in Section 6.3 that every locally stratified program has
a unique perfect model and that this model is independent of the choice of
the level mapping with respect to which the program is locally stratified. In
fact, we are more interested here in a generalization of the perfect model
semantics to three-valued logic, and of course the objective underlying this
generalization is the usual one, namely, to provide a single intended model for
each given program.
We will proceed next with presenting the rather involved definition of the
weakly perfect model due to Przymusinska and Przymusinski.
12 For ease of
notation, it will be convenient to consider (countably infinite) propositional
programs instead of programs over a first-order language, and we recall that
we have already observed in Section 2.1 that this results in no loss of generality
for our purposes.
Let P be a (countably infinite propositional) normal logic program. We
say that an atom A ∈ B P refers to an atom B ∈ B P if either B or ¬B occurs
as a body literal in a clause A ← body in P with head A. We say that A refers
negatively to B if ¬B occurs as a body literal in such a clause. We say that A
depends on B, written B ≤ A, if the pair (A, B) is in the transitive closure of
the relation refers to. We say that A depends negatively on B, written B < A,
if there are C, D ∈ B P such that C refers negatively to D and the following
conditions hold: (1) C ≤ A or C = A (the latter meaning identity), and (2)
B ≤ D or B = D. For A, B ∈ B P , we write A ∼ B if either A = B or A and B
depend negatively on each other, so that A < B and B < A both hold in this
latter case.
13 The relation ∼ is an equivalence relation, and its equivalence
classes are called components of P . A component is trivial if it consists of a
single element A with A < A.
Notice that the definitions above can be viewed in a rather intuitive way
by means of the dependency graph G P of a program P , defined as follows. The
vertices of G P are the ground atoms appearing in P ; for each clause A ← body
in ground(P ) there is a positive directed edge in G P from B to A if B occurs
in body, and there is a negative directed edge from B to A in G P if ¬B occurs
in body. Then, in these terms, we have B ≤ A if and only if there is a directed
path in G P from B to A, and we have B < A if and only if there is a directed
path in G P from B to A passing through a negative edge.
12 The notions of weak stratification and the weakly perfect model were introduced in the
paper [Przymusinska and Przymusinski, 1990].
13 It is noted in [Przymusinska and Przymusinski, 1990] that such mutual recursion is the
primary cause of difficulties in defining declarative semantics for logic programs.