Stable and Perfect Model Semantics
171
6.1.4 Theorem For any normal logic program P and (two-valued) interpretation I, we have
GL P (I) = T fix(P ) (I).
Proof: We show first that for every A ∈ GL P (I) there exists a clause in fix(P )
with head A whose body is true in I, and hence A ∈ T fix(P ) (I). We show this
by induction on the powers of T P/I ; recall that GL P (I) = T P/I ↑ ω.
For the base case T P/I ↑ 0 = ∅, there is nothing to show.
So assume now that for all A ∈ T P/I ↑ n there exists a clause in fix(P )
with head A whose body is true in I. For A ∈ T P/I ↑ (n + 1), there exists a
clause A ← A 1 , . . . , A n in P/I such that A 1 , . . . , A n ∈ T P/I ↑ n, and hence
by construction of P/I there is a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) with B 1 , . . . , B m ∈ I. By our induction hypothesis, we obtain
that for each i = 1, . . . , n there exists a clause A i ← body i in fix(P ) with
'
I |= body i , and hence A i ∈ T fix(P ) (I). So by definition of T the clause
P
A ← body 1 , . . . , body , ¬B 1 , . . . , ¬B m is contained in fix(P ). From I |= body i
n
and B 1 , . . . , B m ∈ I, we obtain A ∈ T fix(P ) (I), as desired. This finishes the
induction argument, and hence GL P (I) ⊆ T fix(P ) (I).
Now conversely, assume that A ∈ T fix(P ) (I). We show that A ∈ GL P (I)
by proving inductively on k that T T / ↑k (I) ⊆ GL P (I) for all k ∈ N.
For the base case, we have T T / ↑0
P
(I) = ∅, so there is nothing to show.
So assume now that T T / ↑k (I) ⊆
P
GL P (I), and let A ∈ T T / ↑(k+1) (I)\T T / ↑k (I).
'
Then there is a clause A
P
← body 1 , . . . , body , ¬B 1 , . . . , ¬
P
B m in T ↑ (
P
k + 1)
n
P
whose body is true in I. Thus, B 1 , . . . , B m ∈ I, and for each i = 1, . . . , n
'
there is a clause A i ← body i in T ↑ k with body i true in I. So A i ∈
P
'
T T / ↑k (I) ⊆ GL P (I). Furthermore, by definition of T , there exists a clause
P
A
P
← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(P ), and since B 1 , . . . , B m ∈ I, we
obtain A ← A 1 , . . . , A n ∈ P/I. Since we know that A 1 , . . . , A n ∈ GL P (I),
we obtain A ∈ GL P (I), and hence T T / ↑(k+1) (I) ⊆ GL P (I). This finishes the
P
induction argument, and we obtain T fix(P ) (I) ⊆ GL P (I).
•
The following corollary is an immediate consequence of Theorem 6.1.4.
6.1.5 Corollary Let P be a normal logic program. Then the stable models
of P are exactly the supported models of fix(P ).
6.2 Stable Model Semantics
Theorem 6.1.4 enables us to carry over results on the single-step operator
and on the supported model semantics to the Gelfond–Lifschitz operator, respectively, the stable model semantics. We will first consider continuity issues.
The following observation is of technical importance.
171
6.1.4 Theorem For any normal logic program P and (two-valued) interpretation I, we have
GL P (I) = T fix(P ) (I).
Proof: We show first that for every A ∈ GL P (I) there exists a clause in fix(P )
with head A whose body is true in I, and hence A ∈ T fix(P ) (I). We show this
by induction on the powers of T P/I ; recall that GL P (I) = T P/I ↑ ω.
For the base case T P/I ↑ 0 = ∅, there is nothing to show.
So assume now that for all A ∈ T P/I ↑ n there exists a clause in fix(P )
with head A whose body is true in I. For A ∈ T P/I ↑ (n + 1), there exists a
clause A ← A 1 , . . . , A n in P/I such that A 1 , . . . , A n ∈ T P/I ↑ n, and hence
by construction of P/I there is a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) with B 1 , . . . , B m ∈ I. By our induction hypothesis, we obtain
that for each i = 1, . . . , n there exists a clause A i ← body i in fix(P ) with
'
I |= body i , and hence A i ∈ T fix(P ) (I). So by definition of T the clause
P
A ← body 1 , . . . , body , ¬B 1 , . . . , ¬B m is contained in fix(P ). From I |= body i
n
and B 1 , . . . , B m ∈ I, we obtain A ∈ T fix(P ) (I), as desired. This finishes the
induction argument, and hence GL P (I) ⊆ T fix(P ) (I).
Now conversely, assume that A ∈ T fix(P ) (I). We show that A ∈ GL P (I)
by proving inductively on k that T T / ↑k (I) ⊆ GL P (I) for all k ∈ N.
For the base case, we have T T / ↑0
P
(I) = ∅, so there is nothing to show.
So assume now that T T / ↑k (I) ⊆
P
GL P (I), and let A ∈ T T / ↑(k+1) (I)\T T / ↑k (I).
'
Then there is a clause A
P
← body 1 , . . . , body , ¬B 1 , . . . , ¬
P
B m in T ↑ (
P
k + 1)
n
P
whose body is true in I. Thus, B 1 , . . . , B m ∈ I, and for each i = 1, . . . , n
'
there is a clause A i ← body i in T ↑ k with body i true in I. So A i ∈
P
'
T T / ↑k (I) ⊆ GL P (I). Furthermore, by definition of T , there exists a clause
P
A
P
← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(P ), and since B 1 , . . . , B m ∈ I, we
obtain A ← A 1 , . . . , A n ∈ P/I. Since we know that A 1 , . . . , A n ∈ GL P (I),
we obtain A ∈ GL P (I), and hence T T / ↑(k+1) (I) ⊆ GL P (I). This finishes the
P
induction argument, and we obtain T fix(P ) (I) ⊆ GL P (I).
•
The following corollary is an immediate consequence of Theorem 6.1.4.
6.1.5 Corollary Let P be a normal logic program. Then the stable models
of P are exactly the supported models of fix(P ).
6.2 Stable Model Semantics
Theorem 6.1.4 enables us to carry over results on the single-step operator
and on the supported model semantics to the Gelfond–Lifschitz operator, respectively, the stable model semantics. We will first consider continuity issues.
The following observation is of technical importance.