{{b}}. However, {b} is not 
ompatible with M1, and thus there is no way to nd a ompatible ol le tion of stable models for the modules starting from M1.

- We instantiate P3 with M2 ∩ Ati(P3) = ∅ = A3 and get SM(P3(A3**)) =** {{c}}.

Continuing with {c} ∩ Ati(P2) = {c} = A4, we get SM(P2(A4**)) =** {{c}}. Again, we noti e that {c} is not 
ompatible with M2, and thus it is not possible to nd a ompatible triple of stable models starting from M2 either.

Thus we an on lude SM(P) = ∅. 

## 4.3 Equivalen E Relations For Modules

The notion of visible equivalen e (Janhunen 2006) was introdu ed in order to negle t

```
hidden atoms when logi
                      programs or other theories of interest are 
                                                           ompared on the
                                                                         

```

basis of their models. The ompositionality property from Theorem 4.14 enables us to bring the same idea to the level of program modulesgiving rise to modular

```
equivalen
        e of logi
                  programs. Visible and modular equivalen
                                                       e are formulated for
                                                                         

```

smodels program modules as follows.

Denition 4.19 For two smodels program modules P and Q,

- P ≡v Q if and only if Atv(P**) = At**v(Q) and there is a bije
tion f : SM(P) → SM(Q)
su h that for al l M ∈ SM(P),
M ∩ Atv(P) = f(M) ∩ Atv(Q); and
- P ≡m Q if and only if Ati(P**) = At**i(Q) and P ≡v Q.

We note that the ondition Atv(P**) = At**v(Q) insisted on the denition of ≡v ,
implies Ato(P**) = At**o(Q) in the presen
e of Ati(P**) = At**i(Q) as required by the relation ≡m. Moreover, these relations 
oin
ide for 
ompletely spe
ied smodels programs, that is modules P with Ati(P) = ∅.

Modular equivalen e lends itself for program substitutions in analogy to strong equivalen e (Lifs hitz et al. 2001), that is, the relation ≡m is a proper 
ongruen
e for the join operator ⊔.

Theorem 4.20 (Congruen e) Let P, Q and R be smodels program modules su
h that P ⊔ R and Q ⊔ R are dened. If P ≡m Q, then P ⊔ R ≡m Q ⊔ R.

The proof of Theorem 4.20 is given in Appendix A. The following examples illus-

```
trate the use of modular equivalen
                                    e in pra
                                             ti
                                                e.
                                                 

```

Example 4.21 Re al l programs P = {a.} and Q = {a ← ∼**b. a** ← b.} from Example 3.13. We an dene modules based on them: P = hP, {b}, {a}, ∅i and Q =
hQ, {b}, {a}, ∅i. Now it is impossible to dene a module R based on R = {b ← a.}
in a way that Q ⊔ R would be dened. Moreover, it holds that P ≡m Q. 

Example 4.22 Module HRn = hR′′, I′′, O′′, {f}i is based on an alternative en
oding for Hamiltonian y le problem given in (Simons et al. 2002). In ontrast to the