158
Mathematical Aspects of Logic Programming Semantics
5.2.3 Acceptable Programs
The treatment of Section 5.2.2 carries over to acceptable programs with
only minor modifications. Given a program P , an interpretation I ∈ I P,3 , and
an I-partial level mapping l, we say that a clause A ← L 1 , . . . , L n is k-safe
(with respect to I and l) if either L 1 , . . . , L n ∈ I and l(A) > l(L i ) for all
i = 1, . . . , n or ¬L k ∈ I, L 1 , . . . , L k−1 ∈ I and l(A) > l(L i ) for all i = 1, . . . , k.
This notion generalizes condition (5.1) in Definition 5.1.8 in the following
sense: a program P is acceptable with respect to some ω-level mapping l and
some interpretation I ∈ I P,2 if and only if I is a model for P whose restriction
to the predicate symbols in Neg
∗ is a supported model for P
− , and for each
P
clause in ground(P ) there exists k such that the clause is k-safe (with respect
to I ∪ ¬(B P \ I) and l).
5.2.12 Definition Let P be a normal logic program, let I be a model for P ,
and let l be an I-partial level mapping for P . We say that P satisfies (F 22 )
with respect to I and l if, for each A ∈ dom(l) and for all clauses in ground(P )
with head A, there exists k such that the clause is k-safe, and furthermore,
each A ∈ dom(l) satisfies one of the following conditions.
(Fi) A ∈ I, and there is a clause A ← L 1 , . . . , L n in ground(P ) such that
L i ∈ I and l(A) > l(L i ) for all i.
(Fii) ¬A ∈ I, and for each clause A ← L 1 , . . . , L n in ground(P ) there exists
i with ¬L i ∈ I and l(A) > l(L i ).
The proof of the following theorem is very similar to the proof of Theorem
5.2.10 and is therefore omitted.
5.2.13 Theorem Let P be a normal logic program and let M be the least
fixed point of the operator Φ P,2,2 . Then, in the knowledge ordering, M is the
greatest model among all three-valued models I for which there exists an Ipartial level mapping l for P such that P satisfies (F 22 ) with respect to I and
l.
5.2.14 Corollary A normal logic program P is acceptable if and only if
Φ P,2,2 ↑ ω is total.
Proof: Let P be such that Φ P,2,2 ↑ ω is total. From Theorem 5.2.8 we know
that P has a unique supported model whose restriction to predicate symbols
in Neg
∗ is a supported model for P
− . By Theorem 5.2.10 and Definition 5.2.9,
P
it easily follows that P is acceptable.
The proof of the converse is similar to that of Corollary 5.2.11.
•
Mathematical Aspects of Logic Programming Semantics
5.2.3 Acceptable Programs
The treatment of Section 5.2.2 carries over to acceptable programs with
only minor modifications. Given a program P , an interpretation I ∈ I P,3 , and
an I-partial level mapping l, we say that a clause A ← L 1 , . . . , L n is k-safe
(with respect to I and l) if either L 1 , . . . , L n ∈ I and l(A) > l(L i ) for all
i = 1, . . . , n or ¬L k ∈ I, L 1 , . . . , L k−1 ∈ I and l(A) > l(L i ) for all i = 1, . . . , k.
This notion generalizes condition (5.1) in Definition 5.1.8 in the following
sense: a program P is acceptable with respect to some ω-level mapping l and
some interpretation I ∈ I P,2 if and only if I is a model for P whose restriction
to the predicate symbols in Neg
∗ is a supported model for P
− , and for each
P
clause in ground(P ) there exists k such that the clause is k-safe (with respect
to I ∪ ¬(B P \ I) and l).
5.2.12 Definition Let P be a normal logic program, let I be a model for P ,
and let l be an I-partial level mapping for P . We say that P satisfies (F 22 )
with respect to I and l if, for each A ∈ dom(l) and for all clauses in ground(P )
with head A, there exists k such that the clause is k-safe, and furthermore,
each A ∈ dom(l) satisfies one of the following conditions.
(Fi) A ∈ I, and there is a clause A ← L 1 , . . . , L n in ground(P ) such that
L i ∈ I and l(A) > l(L i ) for all i.
(Fii) ¬A ∈ I, and for each clause A ← L 1 , . . . , L n in ground(P ) there exists
i with ¬L i ∈ I and l(A) > l(L i ).
The proof of the following theorem is very similar to the proof of Theorem
5.2.10 and is therefore omitted.
5.2.13 Theorem Let P be a normal logic program and let M be the least
fixed point of the operator Φ P,2,2 . Then, in the knowledge ordering, M is the
greatest model among all three-valued models I for which there exists an Ipartial level mapping l for P such that P satisfies (F 22 ) with respect to I and
l.
5.2.14 Corollary A normal logic program P is acceptable if and only if
Φ P,2,2 ↑ ω is total.
Proof: Let P be such that Φ P,2,2 ↑ ω is total. From Theorem 5.2.8 we know
that P has a unique supported model whose restriction to predicate symbols
in Neg
∗ is a supported model for P
− . By Theorem 5.2.10 and Definition 5.2.9,
P
it easily follows that P is acceptable.
The proof of the converse is similar to that of Corollary 5.2.11.
•