
```
en
 oding des
        ribed in Example 4.2, this en
                         oding does not al low us to separate the sele
    tion of the edges to the 
                         y
                           le and the 
                                     he
                                        king of rea
                                                  hed verti
                                                          es into separate
                                                                        

```

modules as their denitions are mutual ly dependent. The input signature of HRn is the same as for Hn, that is, I
′′ = I = {arc(x, y) | 1 ≤ **x, y** ≤ n}. The output signature of HRnis the output signature of Hn ⊔ R
n, that is, O
′′ = O ∪ O
′ = {hc(x, y) | 1 ≤ x, y ≤ n**} ∪ {**reached(x) | 1 ≤ x ≤ n}.

The set R′′ 
ontains rules

$\begin{array}{ccc}\{\text{hc}(1,x)\}&\leftarrow\\ \\[-4mm]\{\text{hc}(x,y)\}&\leftarrow\\ \\[-4mm]\text{reached}(y)&\leftarrow\\ \\[-4mm]f&\leftarrow\\ f&\leftarrow\\ f&\leftarrow\\ f&\leftarrow\\ f&\leftarrow\end{array}$  . 
{hc(1, x)} ← arc(1, x)
{hc(x, y)} ← reached(x), arc(x, y) f ← ∼f, ∼reached(x) f ← ∼f, hc(x, y), hc(x, z) and (13) f ← ∼f, hc(x, y), hc(z, y) (14)
reached(y) ← hc(**x, y**)
for ea h 1 ≤ **x, y, z** ≤ n su
h that y 6= z in (13) and x 6= z in (14).

Now, one may noti e that HRnand Hn⊔R
n have the same input/output interfa e, and SM(HRn**) = SM(**Hn ⊔ R
n) whi
h implies HRn ≡m Hn ⊔ R
n . 

As regards the relationship between modular equivalen e and previously proposed notions of equivalen e, we note the following. First, if one onsiders the ful ly visible ase, that is, the restri tion Ath(P) = Ath(Q) = ∅, modular equivalen
e 
an be seen as a spe ial ase of A-uniform equivalen
e for A = I . Re
all, however, the restri
tion that input atoms may not appear in the heads of the rules as imposed by module stru ture. With a further restri tion Ati(P) = Ati(Q) = ∅, modular equivalen
e basi ally oin ides with weak equivalen e be ause At(P**) = At(**Q) 
an always be satised by extending the interfa e of the module. Setting Ati(P**) = At(**P) would in prin iple give us uniform equivalen e, but the additional ondition **Head(**R)∩I = ∅
leaves room for the empty module only.

In the general ase with hidden atoms, the problem of verifying ≡m for smodels program modules an be redu ed to verifying ≡v for smodels programs. This is a hieved by introdu ing a spe ial module GI 
ontaining a single 
hoi
e rule, whi h a ts as a ontext generator in analogy to (Woltran 2004). We say that two modules P and Q are 
ompatible if they have the same input/output interfa
e, that is, Ati(P**) = At**i(Q) and Ato(P**) = At**o(Q).

Lemma 4.23 Consider ompatible smodels program modules P and Q. Now P ≡m Q if and only if P ⊔ GI ≡v Q ⊔ GI where I = Ati(P**) = At**i(Q) and GI =
h{{I} ←}, ∅**, I,** ∅i generates al l possible input interpretations for P and Q.

Proof Noti e that P ⊔ GI and Q ⊔ GI are smodels program modules with empty input signatures, and thus they an also be viewed as smodels programs. ( =⇒ ) Assume P ≡m Q. Sin
e P ⊔ GI and Q ⊔ GI are dened, P ⊔ GI ≡m Q ⊔ GI by Theorem