�
145
Supported Model Semantics
5.1.8 Definition Let P be a program, and recall from Section 2.5 that an
atom A ∈ B P refers to an atom B ∈ B P if B or ¬B occurs as a body literal in
a clause A ← body in P . We say that A depends on B if the pair (A, B) is in
the transitive closure of the relation refers to. We further denote by Neg P the
set of predicate symbols in P which occur in a negative literal in the body of a
clause in P , and we set Neg
∗ = Neg P ∪ D, where D is the set of all predicate
P
symbols in P on which the predicate symbols in Neg P depend. Finally, by
P
− we denote the set of clauses in P whose head contains a predicate symbol
from Neg
∗
P .
Finally, a program P is called acceptable with respect to some ω-level
mapping l : B P → ω and some interpretation I ∈ I P if I is a model for P whose
restriction to the predicate symbols in Neg
∗ is a supported model for P
− , and
P
the following condition holds. For each ground instance A ← L 1 , . . . , L n of a
clause in P and for all i ∈ {1, . . . , n} we have
i−1
if I |=
L j , then l(A) > l(L i ).
(5.1)
j=1
The following is an example of an acceptable program.
5.1.9 Program Let G be an acyclic finite graph. We define the program
Game to be the program consisting of the following clauses.
4
win(X) ← move(X, Y ), ¬win(Y ).
move(a, b) ←
for all (a, b) ∈ G
Game is not acyclic. One of the ground instances of the first clause is
win(a) ← move(a, a), ¬win(a), so if Game were acyclic with respect to some
level mapping l, we would have l(win(a)) < l(win(a)), which is impossible.
In order to show that Game is acceptable, we need to find a suitable level
mapping l and a suitable model I for P . Since G is acyclic and finite, there
exists a function f which assigns a natural number to every vertex of G, and
such that for each vertex a the following holds.
0
if there is no (a, b) ∈ G,
f (a) =
1 + max{f (b) | (a, b) ∈ G} otherwise.
We now define l by setting l(move(a, b)) = f (a) and l(win(a)) = f (a) + 1
for all vertices a, b of G. From acyclicity and finiteness of G, we furthermore
obtain that there exists a function g mapping each vertex to {0, 1} satisfying
the following.
0
if there is no (a, b) ∈ G,
g(a) =
1 − min{g(b) | (a, b) ∈ G} otherwise.
4 This example is taken from [Apt and Pedreschi, 1994]. For further discussion of programs related to Game, see [Hitzler and Seda, 2003].
145
Supported Model Semantics
5.1.8 Definition Let P be a program, and recall from Section 2.5 that an
atom A ∈ B P refers to an atom B ∈ B P if B or ¬B occurs as a body literal in
a clause A ← body in P . We say that A depends on B if the pair (A, B) is in
the transitive closure of the relation refers to. We further denote by Neg P the
set of predicate symbols in P which occur in a negative literal in the body of a
clause in P , and we set Neg
∗ = Neg P ∪ D, where D is the set of all predicate
P
symbols in P on which the predicate symbols in Neg P depend. Finally, by
P
− we denote the set of clauses in P whose head contains a predicate symbol
from Neg
∗
P .
Finally, a program P is called acceptable with respect to some ω-level
mapping l : B P → ω and some interpretation I ∈ I P if I is a model for P whose
restriction to the predicate symbols in Neg
∗ is a supported model for P
− , and
P
the following condition holds. For each ground instance A ← L 1 , . . . , L n of a
clause in P and for all i ∈ {1, . . . , n} we have
i−1
if I |=
L j , then l(A) > l(L i ).
(5.1)
j=1
The following is an example of an acceptable program.
5.1.9 Program Let G be an acyclic finite graph. We define the program
Game to be the program consisting of the following clauses.
4
win(X) ← move(X, Y ), ¬win(Y ).
move(a, b) ←
for all (a, b) ∈ G
Game is not acyclic. One of the ground instances of the first clause is
win(a) ← move(a, a), ¬win(a), so if Game were acyclic with respect to some
level mapping l, we would have l(win(a)) < l(win(a)), which is impossible.
In order to show that Game is acceptable, we need to find a suitable level
mapping l and a suitable model I for P . Since G is acyclic and finite, there
exists a function f which assigns a natural number to every vertex of G, and
such that for each vertex a the following holds.
0
if there is no (a, b) ∈ G,
f (a) =
1 + max{f (b) | (a, b) ∈ G} otherwise.
We now define l by setting l(move(a, b)) = f (a) and l(win(a)) = f (a) + 1
for all vertices a, b of G. From acyclicity and finiteness of G, we furthermore
obtain that there exists a function g mapping each vertex to {0, 1} satisfying
the following.
0
if there is no (a, b) ∈ G,
g(a) =
1 − min{g(b) | (a, b) ∈ G} otherwise.
4 This example is taken from [Apt and Pedreschi, 1994]. For further discussion of programs related to Game, see [Hitzler and Seda, 2003].