Proof Let P1 and P2 be smodels program modules su
h that P1 ⊕ P2 is dened. We 
an show SM(P1 ⊕P2) 6= SM(P1) ⋊⋉ SM(P2) by 
hoosing M ⊆ At(P1 ⊕P2) and 
he
king that

- M ∈ SM(P1 ⊕ P2) and M ∩ At(P1) 6∈ SM(P1); or
- M ∈ SM(P1 ⊕ P2) and M ∩ At(P2) 6∈ SM(P2); or - M 6∈ SM(P1 ⊕ P2), M ∩ At(P1) ∈ SM(P1), and M ∩ At(P2) ∈ SM(P2).

On e we have hosen M , these tests 
an be performed in polynomial time, whi
h shows that the problem is in **coNP**. To establish **coNP**-hardness we present a redu tion from **3SAT**. Consider a nite set S = {C1**, . . . , C**n} of three-literal 
lauses Ci of the form l1 ∨ l2 ∨ l3 where ea
h li is either an atom a or its 
lassi
al negation
¬a. Ea
h 
lause Ci is translated into rules ri,j of the form ci ← fj , where 1 ≤ j ≤ 3, and fj = a if lj = a and fj = ∼a if lj = ¬a. The intuitive reading of ci is that lause Ci is satised. We dene modules P1 = h{e ← d.}, {d}, {e}, ∅i and

$\mathbb{P}_{2}=\langle\{r_{i,j}\mid1\leq i\leq n,1\leq j\leq3\}\cup\{d\gets e,c_{1},\ldots,c_{n}.\},$
  **At(S) U $\{e\}$, $\{d\}$, $\{e_{1},\ldots,e_{n}\}$.**
Now P1 ⊕ P2 is dened, and SM(P1) = {∅, {**d, e**}}. There is M ∈ SM(P2) that is ompatible with {**d, e**} if and only if S ∈ **3SAT**. Sin
e d 6∈ N and e 6∈ N for all N ∈ SM(P1⊕P2), it follows that S ∈ **3SAT** if and only if SM(P1 ⊕P2**) = SM(**P1) ⋊⋉
SM(P2).

Theorem 5.8 shows that there is a tradeo for allowing positive re ursion between modules, as more eort is needed to he k that omposition of su h modules does not ompromise the ompositionality of the stable model semanti s.

## 6 Tools And Pra Ti Al Demonstration

```
The goal of this se
               tion is to demonstrate how the module system introdu
                                                           ed in
                                                              

```

Se tion 4 an be exploited in pra tise in the ontext of the smodels system and

```
other 
      ompatible systems. In this respe
                                     t, we present tools that have been developed for the (de)
             omposition of logi
                                   programs that are represented in the internal le
                                                                                         

```

format 6 of the smodels engine. The binaries for both tools are available under the asptools olle tion7
. Moreover, we ondu t and report a pra ti al experiment whi h illustrates the performan e of the tools when pro essing substantially large ben hmark instan es, that is, smodels programs having up to millions of rules (see the asptools web page for examples).

The rst tool, namely modlist, is targeted at program de omposition based on the strongly onne ted omponents of an smodels program given as input.

In view of the ob je tives of Se tion 5.1, there are three optional out omes of the de omposition, that is, strongly onne ted omponents that take into a ount 6 The reader is referred to (Janhunen 2007) for a detailed des ription and analysis of the format.

7 http://www.t s.hut.fi/Software/asptools/