module. The latter strategy used in Example 4.31 works even if there is negative recursion between the modules, as already shown in Example 4.18.

The module theorem strengthens an earlier version given in (Janhunen 2006)
to cover programs that involve positive body literals, too. The independent sets proposed by Faber et al. (2005) push negative recursion inside modules which is unnecessary in view of our results. Their version of the module theorem is also weaker than Theorem 4.14.

The approach to modularity based on lp-functions (Gelfond and Gabaldon 1999; Baral 2003) has features similar to our approach. The components presented by lp-functions have an input/output interface and a domain reflecting the possible input interpretations. The functional specification requires an lp-function to have a consistent answer set for any interpretation in its domain. This is something that is not required in our module system. Lp-functions are flexible in the sense that there are several operators for refining them. However, the composition operator for lp-functions allows only incremental compositions, which again basically reflects the splitting-set theorem.

## 5 More On Program (De)Composition

So far we have established a module architecture for the class SMODELS programs, in which modules interact through an input/output interface and the stable model semantics is fully compatible with the architecture. In this section we investigate further the ways to understand the internal structure of logic programs by seeing them as compositions of logic program modules. First, we use the conditions for module composition to introduce a method for decomposing an SMODELS program into modules. A more detailed knowledge of the internal structure of a program (or a module) might reveal ways to improve search for stable models. Another application can be found in modularization of the translation-based equivalence verification method in (Oikarinen and Janhunen 2008b). Second, we consider possibilities of relaxing the conditions for module composition, that is, whether it is possible to allow positive recursion between modules in certain cases.

## 5.1 Finding A Program Decomposition

Recall that any smodels program P can be viewed as a module ⟨ P, ∅, At( P), ∅⟩, and thus we consider here a more general case of finding a module decomposition for an arbitrary smodels program module P = ⟨ R, I, O, H ⟩ . The first step is to exploit the strongly connected components D 1 , . . . , D n of Dep + ( P ) and define submodules P i by grouping the rules so that for each D i all the rules r ∈ R such that Head( r ) ⊆ D i are put into one submodule.

Now, the question is whether P i 's defined this way would form a valid decomposition of P into submodules. First notice that input atoms form a special case because Head( R ) ∩ I = ∅ . Each α ∈ I ends up in its own strongly connected component and there are no rules to include into a submodule corresponding to strongly connected component { a} . Thus it is actually unnecessary to include a submodule based on