by the property of having enough visible atoms (Janhunen and Oikarinen 2007). Intuitively, if P has enough visible atoms, the EVA property for short, then each interpretation of At v (P) uniquely determines an interpretation of At h (P). Consequently, the stable models of P can be distinguished on the basis of their visible parts. Although verifying the EVA property can be hard in general (Janhunen and Oikarinen 2007, Proposition 4.14), there are syntactic subclasses of SMODELS programs with the EVA property. The use of visible atoms remains unlimited and thus the full expressiveness of SMODELS programs remains at programmer's disposal. Also note that the EVA property can always be achieved by declaring sufficiently many atoms visible. For smodels programs with the EVA property, the verification of visible equivalence is a coNP-complete decision problem (Janhunen and Oikarinen 2007).

Eiter et al. (2005) introduce a very general framework based on equivalence frames to capture various kinds of equivalence relations. All the equivalence relations defined in this section can be defined using the framework. Visible equivalence, however, is exceptional in the sense that it does not fit into equivalence frames based on projected answer sets. As a consequence, the number of answer sets may not be preserved which is somewhat unsatisfactory because of the general nature of answer set programming as discussed in the previous section. Under the EVA assumption, however, the projective variant of visible equivalence defined by

## {M N At X (P) | M E Sm(P)} = {N N At X (Q) | N E Sm(Q)} Coincides With Visible Equivalence.

Recently Woltran presented another general framework characterizing (H,B)-
equivalence (Woltran 2007). {H,B}-equivalence is defined similarly to strong equivalence, but the set of possible contexts is restricted by limiting the head and body occurrences of atoms in a context program R by H and B , respectively. Thus, programs P and Q are ⟨ H, B ⟩ -equivalent if and only if P ∪ R ≡ Q ∪ R for all R such that Head( R ) ⊆ H and Body( R ) ⊆ B . Several notions of equivalence such as weak equivalence together with (relativized) strong and (relativized) uniform equivalence can be seen as special cases of (H, B) -equivalence by varying the sets H and B.

## 4 Smodels Program Modules

We start this section by introducing the syntax and the stable model semantics for an individual smodels program module, and then formalize the conditions for module composition. One of the main results is the module theorem showing that module composition is suitably restricted so that compositionality of stable model semantics for smodels programs is achieved. We also introduce an equivalence relation for modules, and propose a general translation-based scheme for introducing syntactical extensions for the module theorem. The scheme is then utilized in the proof of the module theorem. We end this section with a brief comparison between our module architecture and other similar proposals. 12