overs only positive programs under the least model semanti s. Maher (1993) forbids all re ursion between modules and onsiders Przymusinski's perfe t models

(Przymusinski 1988) rather than stable models. Etalle and Gabbrielli (1996) restri t the omposition of onstraint logi program (Jaar and Maher 1994) modules with a ondition that is lose to ours: At(P) ∩ At(Q) ⊆ Atv(P) ∩ Atv(Q) but no distin tion between input and output is made, for example, Ato(P) ∩ Ato(Q) 6= ∅

```
is allowed a
                
                 ording to their denitions.
                                                   

```

Approa hes to modularity within ASP typi ally do not allow any re ursion (negative or positive) between modules (Eiter et al. 1997; Tari et al. 2005; Lifs hitz and Turner 1994; Gelfond and Gabaldon 1999). Theorem 4.14, the module theorem, is stri tly stronger than the splitting-set theorem (Lifs hitz and Turner 1994) for normal logi programs, and the general ase allows us to generalize the splitting-set theorem for smodels programs. Consider rst the ase of normal logi programs. A splitting of a program an be used as a basis for a module stru ture. If U is a splitting set for a normal logi program P , then we 
an dene

## P = B ⊔ T = Hbu (P), ∅, U, ∅I ⊔ Htu (P), U, At(P) \ U, ∅I.

It follows dire tly from Theorems 3.6 and 4.14 that M1 ∈ SM(B) and M2 ∈ SM(T)
are ompatible if and only if hM1, M2 \ Ui is a solution for P with respe
t to U .

Example 4.31 Consider a normal logi program P = {a ← ∼b. b ← ∼**a. c** ← a.}.

The set U = {**a, b**} is a splitting set for P , and therefore the splitting set-theorem
(Theorem 3.6) 
an be applied: bU (P) = {a ← ∼b. b ← ∼a.} and tU (P) = {c ←
a.}. Now M1 = {a} and M2 = {b} are the stable models of bU (P), and we 
an evaluate the top with respe t to M1 and M2, resulting in solutions hM1, {c}i and hM2, ∅i, respe
tively. On the other hand, P 
an be seen as join of modules P1 =
hbU (P), ∅**, U,** ∅i and P2 = htU (P)**, U,** {c}, ∅i. Now, we have SM(P1) = {M1, M2} and SM(P2) = {∅, {b}, {a, c}, {**a, b, c**}}. Out of eight possible pairs only hM1, {**a, c**}i and hM2, {b}i are 
ompatible.

However, it is possible to apply Theorem 4.14 similarly to the splitting-set theorem, that is, we only need to ompute the stable models of P2 
ompatible with the stable models of P1. Noti
e that when the splitting-set theorem is appli
able, the stable models of P1 ful ly dene the possible input interpretations for P2. This leaves us with stable models {**a, c**} and {b} for the 
omposition. 

On the other hand, onsider the module P1 = hbU (P), ∅**, U,** ∅i in the above example. There are no non-trivial splitting sets for the bottom program bU (P) =
{a ← ∼b. b ← ∼a.}. However, P1 
an be viewed as the join of two NLP modules Q1 = h{a ← ∼b.}, {b}, {a}, ∅i, and Q2 = h{b ← ∼a.}, {a}, {b}, ∅i to whi
h the module theorem is appli able.

In the general ase of smodels program modules we an use the module theorem to generalize the splitting-set theorem for smodels programs. Then the bottom module a ts as an input generator for the top module, and one an simply nd the stable models for the top module instantiated with the stable models of the bottom