# On the Semantics of Hybrid ASP Systems Based on Clingo
## 4 Structured Theories and Answer Sets
### Answer Sets of Logic Programs with Compositional Theories
However, if we focus on consistent, compositional theories that have an absolute complement, then we can reconstruct the \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model from any of its corresponding \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer sets. In fact, we can establish a one-to-one correspondence between the \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model of a program and a kind of equivalence class of its \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer sets. Each of the equivalence classes may contain many \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer sets, but any of them has enough information to reconstruct the corresponding \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model. We say that an answer set \((Y,v)\)_satisfies_ an atom \(b\in\mathcal{A}\cup\mathcal{T}\), written \((Y,v)\models b\), when:  
* \(b\in Y\) for regular atoms \(b\in\mathcal{A}\);
* \(v\in\llbracket b\rrbracket\)\(\bigsqcup_{\textit{domain}(v)}\) for theory atoms \(b\in\mathcal{T}\). Note that the second condition restricts the denotation \(\llbracket b\rrbracket\) to _domain\((v)\)_. This is because \(v\) can be partial and if so, we just require that there exists some complete valuation in \(\llbracket b\rrbracket\) that agrees with the values assigned by \(v\) to its defined variables _domain\((v)\)_. For any negative literal \(\
eg b\), we say that \((Y,v)\models\
eg b\) simply when \((Y,v)\
ot\models b\). If \(B\) is a rule body, we write \((Y,v)\models B\) to stand for \((Y,v)\models L\) for every literal \(L\) in \(B\). Formally, for a program \(P\) and an \(\langle\mathfrak{T},\mathcal{E}\rangle\)-_answer set_\((Y,v)\), we define  
\[stb_{P}(Y,v)\ =\ Y\ \cup\ \{\ \texttt{s}\in\mathcal{E}\ |\ v\in\llbracket \texttt{s}\,\rrbracket\bigsqcup_{\textit{domain}(v)}\ \}\ \cup\ \{\ \texttt{s}\in\mathcal{F}\ |\ (B\to\texttt{s})\in P\ \text{and}\ (Y,v)\models B\ \}\]  
We also write \((Y_{1},v_{1})\sim(Y_{2},v_{2})\) if \(stb_{P}(Y_{1},v_{1})=stb_{P}(Y_{2},v_{2})\) and say that \((Y_{1},v_{1})\) and \((Y_{2},v_{2})\) belong to the same equivalence class with respect to \(P\). Proposition 8: _Let \(\mathfrak{T}=\langle\mathcal{T},\textit{Sat},\tilde{\cdot}\rangle\) be a consistent compositional theory with an absolute complement and let \(\mathcal{E}\subseteq\mathcal{T}\) be a closed set of external atoms. Then, there is a one-to-one correspondence between the \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable models of some program \(P\) and the equivalence classes with respect to \(P\) of its \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer sets. Furthermore, if \((Y,v)\) is a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer set, then \(stb_{P}(Y,v)\) is a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model of \(P\) and \((Y,v)\) belongs to \(ans(stb_{P}(Y,v))\)._  
Despite this one-to-one correspondence, there is a crucial difference between \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable models and \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer sets: it is possible for two different programs to have the same \(\langle\mathfrak{T},\mathcal{E}\rangle\)-answer sets but different \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable models. This is a result of the use of the program to build the corresponding \(\langle\mathfrak{T},\mathcal{E}\rangle\)-stable model in function \(stb_{P}(\cdot)\). For instance, program  
\[\texttt{a} \leftarrow \tag{14}\] \[\perp \leftarrow\texttt{a},\ \&\texttt{sum}\{x\}\texttt{!=}4 \tag{15}\]  
has a unique answer set \((Y,v)\) with \(Y=\{a\}\) and \(v=\{x=4\}\). This is also the unique answer set of the program obtained by extending the above program with rule  
\[\texttt{\&sum}\{x\}\texttt{>=}4\leftarrow\texttt{a} \tag{16}\]  
However, we can easily see that (14) and (15) have the unique stable model \(\{\texttt{a},\ \&\texttt{sum}\{x\}{\texttt{=}4\}\}\), whereas (14)-(16) has the unique stable model \(\{\texttt{a},\ \&\texttt{sum}\{x\}{\texttt{=}4\},\ \&\texttt{sum}\{x\}{\texttt{>=}4\}\}\).