
| Benchmark   | ephp-13   | mutex3   | p hi3   | s-----   |
|-------------|-----------|----------|---------|----------|
| nr          | nm        |          |         |          |
| 1           | 14 4 74   | 6 7  749 | 2 811   | 2 969    |
| 2           | 7 0 14    | 2 757    | 1 434   |          |
| 3 -4        | 12 680    | 41       | 1 962   |          |
| 5-8         | 149       | 30 798   | 2       |          |
| 9-16        | 6 18      | 255      | 6       |          |
| 17-32       | 582       | 11       |         |          |
| 3-64        | 1         |          |         |          |
| 65-128      | 134       |          |         |          |
| 129-512     | 296       |          |         |          |
| 513-1 024   | 1         | 9        |         |          |
| 2           |           |          |         |          |
| over 1 0 24 | 1         | 2        |         |          |

Table 2. Distribution of the sizes of modules (see Table 1 for legends) to the computation of stable models. Nevertheless, we intend to exploit these tools in order to modularize different tasks in ASP such as verifying ordinary/modular equivalence and program optimization . The existence of such tools enables modular program development and the creation of module libraries for smodels programs, and thus puts forward the use of module architectures in the realm of ASP.

## 7 Conclusions

In this paper, we introduce a simple and intuitive notion of a logic program module that interacts with other modules through a well-defined input/output interface. The design has its roots in a module architecture proposed for conventional logic programs (Gaifman and Shapiro 1989), but as regards our contribution, we tailor the architecture in order to better meet the criteria of ASP. Perhaps the most important objective in this respect is to achieve the compositionality of stable model semantics, that is, the semantics of an entire program depends directly on the semantics assigned to its modules. To this end, the main result of this paper is formalized as the module theorem (Theorem 4.14) which links program-level stability with module-level stability. The theorem holds under the assumption that positively interdependent atoms are always placed in the same module. The join operation U defined for program modules effectively formalizes this constraint— which we find acceptable when it comes to good programming style in ASP.

The module theorem is also a proper generalization of the splitting-set theorem (Lifschitz and Turner 1994) recast for smodels programs. The main difference is that splitting-sets do not enable any kind of recursion between modules.

Even though the module theorem is proved to demonstrate the feasibility of the respective module architecture, it is also applied as a tool to simplify mathematical proofs in this paper and recently also in (Oikarinen and Janhunen 2008a;