
## 4.1 Syntax And Semanti S Of An Smodels Program Module

We dene a logi program module similarly to Gaifman and Shapiro (1989), but onsider the ase of smodels programs instead of positive normal logi programs overed in (Gaifman and Shapiro 1989). An analogous module system in the ontext of disjun tive logi programs is presented in (Janhunen et al. 2007).

Denition 4.1 An smodels program module P is a quadruple h**R, I, O, H**i where 1. R is a nite set of basi 
onstraint rules; 2. I , O, and H are pairwise disjoint sets of input, output, and hidden atoms; 3. At(R) ⊆ At(P) whi
h is dened by At(P) = I ∪ O ∪ H ; and 4. **Head(**R) ∩ I = ∅.

The atoms in Atv(P) = I ∪ O are 
onsidered to be visible and hen
e a

essible to other modules onjoined with P; either to produ
e input for P or to utilize the output of P. We use notations Ati(P) and Ato(P) for referring to the input signature I and the output signature O, respe
tively. The hidden atoms in Ath(P) = H =
At(P) \ Atv(P) are used to formalize some auxiliary 
on
epts of P whi
h may not be sensible for other modules but may save spa e substantially. The use of hidden atoms may yield exponential savings in spa e, see (Janhunen and Oikarinen 2007, Example 4.5), for instan e. The ondition **Head(**R) ∩ I = ∅ ensures that a module may not interfere with its own input by dening input atoms of I in terms of its rules. Thus input atoms are only allowed to appear as onditions in rule bodies.

```
Example 4.2 Consider the Hamiltonian 
                             y
                               le problem for dire
                                            ted graphs, that is,
                                                         

```

whether there is a y le in the graph su h that ea h node is visited exa tly on e returning to the starting node.

Let n denote the number of nodes in the graph and let arc(**x, y**) denote that there is a dire ted edge from node x to node y in the graph.

Module Hn = hR, I, O, {**c, d**}i sele
ts the edges to be taken into a 
y
le by insisting

```
that ea
        h node must have exa
                               tly one in
                                          oming and exa
                                                          tly one outgoing edge. The
                                                                                     

```

input signature of Hn is a graph represented as a set of edges: I = {arc(**x, y**) | 1 ≤ **x, y** ≤ n}. The output signature of Hnrepresents whi
h edges get sele
ted into a andidate for a Hamiltonian y le: O = {hc(x, y) | 1 ≤ **x, y** ≤ n}. The set R

ontains rules

{hc(x, y)} ← arc(**x, y**) (8)

$\mathrm{dc}(x,y)$ (9) $2\leq\{\mathsf{hc}(x,1),\ldots,\mathsf{hc}(x,n)\}$ (9) $\sim$$\mathsf{hc}(x,1),\ldots,\sim$$\mathsf{hc}(x,n)$ (10) $2\leq\{\mathsf{hc}(1,x),\ldots,\mathsf{hc}(n,x)\}$ and (11) $\sim$$\mathsf{hc}(1,x),\ldots,\sim$$\mathsf{hc}(n,x)$ (12)
$\begin{array}{ccc}?&\leftarrow\\ &\leftarrow\\ ?&\leftarrow\\ ?&\leftarrow\\ ?&\leftarrow\end{array}$  4. 
for ea h 1 ≤ **x, y** ≤ n; and a rule d ← ∼**d, c** whi
h enfor
es c to be false in every

```
stable model. The rules in (8) en
                                    ode the sele
                                                 tion of edges taken in the 
                                                                               y
                                                                                 le. The

```
