logi programs3
, and give an alternative denition of stable models based on the lassi al models of the ompletion of a program (Clark 1978) and its loop formulas (Lin and Zhao 2004). The splitting-set theorem an be used to simplify the omputation of stable models by splitting a program into parts, and it is also a useful tool for stru turing mathemati al proofs for properties of logi programs.

Denition 3.4 A splitting set for a normal logi program P is any set U ⊆ At(P)
su h that for every rule r in P it holds that At(r) ⊆ U if **Head(**r) ∈ U .

The set of rules r ∈ P su
h that At(r) ⊆ U is the bottom of P relative to U ,
denoted by bU (P). The set tU (P) = P \ bU (P) is the top of P relative to U whi
h an be partially evaluated with respe t to an interpretation X ⊆ U . The result is a program e(tU (P), X) dened as
{Head(r) ← (Body+(r) \ U), ∼**(Body**−(r) \ U) | r ∈ tU (P),
Body+(r) ∩ U ⊆ X and **(Body**−(r) ∩ U) ∩ X = ∅}.

```
A solution to a program with respe
                    t to a splitting set is a pair 
                                     onsisting of a stable
                                                

```

model X for the bottom and a stable model Y for the top partially evaluated with respe t to X .

Denition 3.5 Given a splitting set U for a normal logi program P , a solution to P with respe
t to U is a pair h**X, Y** i su
h that
(i) X ⊆ U is a stable model of bU (P), and
(ii) Y ⊆ At(P) \ U is a stable model of e(tU (P), X).

Solutions and stable models relate as follows.

Theorem 3.6 (The splitting-set theorem (Lifs hitz and Turner 1994))

Let U be a splitting set for a normal logi program P and M ⊆ At(P) an interpretation. Then M ∈ SM(P) if and only if the pair hM ∩ **U, M** \ Ui is a solution to P
with respe t to U .

The splitting-set theorem an also be used in an iterative manner, if there is a monotone sequen e of splitting sets {U1, . . . , Ui**, . . .**}, that is, Ui ⊂ Uj if **i < j** ,
for program P . This is 
alled a splitting sequen
e and it indu
es a 
omponent stru ture for P . The splitting-set theorem generalizes to a splitting sequen
e theorem (Lifs hitz and Turner 1994), and given a splitting sequen e, the stable models of a program P 
an be 
omputed iteratively bottom-up.

Lin and Zhao present an alternative denition of stable models for normal logi 

```
programs based on the 
                    lassi
                        al models of the 
                                       ompletion of a program (Clark 1978)
                                                                      

```

and its loop formulas (Lin and Zhao 2004). We will apply this denition later on in the proof of the module theorem (Theorem 4.14).

