# On the Semantics of Hybrid ASP Systems Based on Clingo
## 4 Structured Theories and Answer Sets
### Answer Sets of Logic Programs with Compositional Theories  
We can formalize the idea of an answer set as a pair containing a set of regular atoms plus an (possibly partial) assignment of values to the theory variables. The definition presented here is not tailored to any particular system but only requires that the structured theory is _consistent_, _compositional_, and has an _absolute complement_. These are three properties that the theories of the three mentioned systems share, and that may very well cover future hybrid systems based on clingo 5. To formally establish the concept of answer sets, let us introduce some notations. Given any valuation \(v\in\mathcal{V}\) and a subset of variables \(\Sigma\subseteq\mathcal{X}\), the function \(v|_{\Sigma}:\Sigma\rightarrow\mathcal{D}\) stands for the restriction of \(v\) to \(\Sigma\). Accordingly, for any set of valuations \(V\subseteq\mathcal{V}\) we define their restriction to \(\Sigma\) as \(V|_{\Sigma}\stackrel{{\text{\tiny def}}}{{\ll}}\{v|_{\Sigma}\mid v \in V\}\). Given a structured theory \(\mathfrak{T}=\langle\mathcal{T},\mathit{Sat},\widehat{\cdot}\rangle\), if \(X\subseteq\mathcal{A}\cup\mathcal{T}\) is a set of atoms, we define  
\[\mathit{ans}(X) \stackrel{{\text{\tiny def}}}{{=}} \quad\{\;(Y,v|_{\Sigma})\;\mid\;Y=X\cap\mathcal{A},\;\Sigma=\mathit{vars}(X \cap\mathcal{T}),\;v\in[\![X\cap\mathcal{T}]\!]\;\}\]  
that is, \(\mathit{ans}(X)\) collects all pairs \((Y,v^{\prime})\) where \(Y\) is fixed to the regular atoms in \(X\), and \(v^{\prime}\) varies among all valuations in \([\![X\cap\mathcal{T}]\! ]\) from the theory atoms in \(X\) but restricted to the variables occurring in those theory atoms. Note that \(v\) is only defined for a subset of variables \(\Sigma=\mathit{vars}(X\cap\mathcal{T})\subseteq\mathcal{X}\). We can also understand \(v\) as a partial valuation \(v:\mathcal{X}\twoheadrightarrow\mathcal{D}\), where \(\mathit{domain}(v)=\Sigma\), leaving all variables in \(\mathcal{X}\setminus\Sigma\) undefined. In fact, the values of these variables are irrelevant due to Condition 5 in Definition 3 for a structured theory. **Definition 5** (Answer Set): _If \(X\) is a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model of some program \(P\) and \((Y,v)\) belongs to \(\mathit{ans}(X)\), then we say that \((Y,v)\) is a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer set of \(P\)._  
For instance, in our running example, the first answer set printed by clingcon corresponds to the \(\langle\mathfrak{T},\mathcal{E}\rangle\)_-answer set_\((Y_{1},v_{11})\) where \(Y_{1}=\{a\}\) is a set of regular atoms and \(v_{11}\) is the valuation \(\{x=4,\,y=0,\,z=2\}\). Recall that the theory atoms in \(X_{1}\) are \(s_{1}\) and \(s_{2}\), and note that \(v_{11}\) satisfies both. Similarly, the second answer set printed by clingcon corresponds to the \(\langle\mathfrak{T},\mathcal{E}\rangle\)_-answer set_\  
are actually required (any arbitrary assignment forms a \(\mathfrak{D}\)-solution). Further, there are obviously infinitely many answer sets in \(ans(\{\texttt{a},\texttt{\&diff}\{\texttt{x}-\texttt{y}\}{\texttt{<=}-2\}\})\), but clingo[dl] selects a particular one for output, which we further discuss in Section 5. As may be expected, given a consistent, compositional theory \(\mathfrak{T}\), for every \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model, we always obtain at least one \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer set. Proposition 7: _Let \(\mathfrak{T}=\langle\mathcal{T},\textit{Sat},\tilde{\cdot}\rangle\) be a compositional theory and let \(\mathcal{E}\subseteq\mathcal{T}\) be a closed set of external atoms. If \(X\) is a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model of some program \(P\), then \(ans(X)\
eq\emptyset\)._  
As we show above, \(ans(X)\) is, in general, not a singleton, so the correspondence between the \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model and \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer sets is one-to-many.