# On the Semantics of Hybrid ASP Systems Based on Clingo
## 3 Transformation-Based Semantics Revisited
### Stable Models of Logic Programs with Abstract Theories  
With a firm definition of what constitutes a theory \(\mathfrak{T}\), we can now make precise the definition of a \(\mathfrak{T}\)-solution and \(\mathfrak{T}\)-stable model of a \(\mathcal{T}\)-logic program given in (3). For clarity, we refine those definitions by further specifying the subset of external theory atoms in \(\mathcal{E}\). Moreover, given any set \(S\) of theory atoms, we define its _(complemented) completion_ with respect to external atoms \(\mathcal{E}\), denoted by \(\mathit{Comp}_{\mathcal{E}}(S)\), as the following superset of \(S\):  
\[\mathit{Comp}_{\mathcal{E}}(S)\stackrel{{\text{def}}}{{=}}S\, \cup\,\big{(}\widehat{\mathcal{E}\setminus\widehat{S}}\big{)}\]  
In other words, we add the complement atom \(\widehat{\texttt{s}}\) for every external atom \(\texttt{s}\) that does not occur explicitly in \(S\). Note that \(S\) is \(\mathcal{E}\)-complete iff \(\mathit{Comp}_{\mathcal{E}}(S)=S\). As an example, consider an abstract theory from \(\mathfrak{L}\) with the theory atoms \(\mathcal{T}=\{\texttt{s}_{1},\texttt{s}_{2},\texttt{s}_{3},\texttt{s}_{4}\}\) given above with  
\[\texttt{s}_{1}=\left(\,\texttt{\&sum}\{x;y\}\!=\!4\,\right) \qquad\texttt{s}_{3}=\left(\,\texttt{\&sum}\{x;y\}\!\mid=\!4\,\right)\] \[\texttt{s}_{2}=\left(\,\texttt{\&sum}\{y;z\}\!=\!2\,\right) \qquad\texttt{s}_{4}=\left(\,\texttt{\&sum}\{y;z\}\!\mid=\!2\,\right)\]  
Suppose we only have one external atom \(\mathcal{E}=\{\texttt{s}_{1}\}\) and assume that the complements \(\widehat{\texttt{s}_{1}}=\texttt{s}_{3}\) and \(\widehat{\texttt{s}_{2}}=\texttt{s}_{4}\) are defined as expected. Then, set \(S=\{\texttt{s}_{2}\}\) is \(\mathcal{E}\)-incomplete because neither \(\texttt{s}_{1}\in S\) nor \(\widehat{\texttt{s}_{1}}=\texttt{s}_{3}\in S\). The completion of \(S\) corresponds to  
\[\mathit{Comp}_{\mathcal{E}}(S)=S\cup\widehat{(\mathcal{E}\setminus S)}=\{ \texttt{s}_{2},\widehat{\texttt{s}_{1}}\}=\{\texttt{s}_{2},\texttt{s}_{3}\}\]so we eventually add \(\mathtt{s}_{3}\). On the other hand, set \(S=\{\mathtt{s}_{1},\mathtt{s}_{2}\}\) is \(\mathcal{E}\)-complete because we do have information about the external atom \(\mathtt{s}_{1}\), and so, \(\widehat{\mathcal{E}\setminus S}\) does not provide any additional information. Definition 2 (\(\langle\mathfrak{T},\mathcal{E}\rangle\)-solution): Given an abstract theory \(\mathfrak{T}=\langle\mathcal{T},\mathit{Sat},\widehat{\cdot}\rangle\) and a set \(\mathcal{E}\subseteq\mathcal{T}\) of external theory atoms, we define \(S\in\mathit{Sat}\) as a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-solution, if \(\mathit{Comp}_{\mathcal{E}}(S)\in\mathit{Sat}\), that is, the completion of \(S\) is \(\mathfrak{T}\)-satisfiable. The next result shows that \(\mathcal{E}\)-complete solutions suffice when considering the existence of a solution (The proofs for all propositions can be found in Appendix B):  
Proposition 1: _Let \(\mathfrak{T}=\langle\mathcal{T},\mathit{Sat},\widehat{\cdot}\rangle\) be an abstract theory and \(\mathcal{E}\subseteq\mathcal{T}\) be a set of external atoms. For any \(\langle\mathfrak{T},\mathcal{E}\rangle\)-solution \(S\subseteq\mathcal{T}\), we have:_  
1. \(\mathit{Comp}_{\mathcal{E}}(S)\) _is_ \(\mathcal{E}\)_-complete and is also a_ \(\langle\mathfrak{T},\mathcal{E}\rangle\)_-solution._
2. _If_ \(S\) _is_ \(\mathcal{E}\)_-complete, then_ \(S\) _is_ \(\mathfrak{T}\)_-satisfiable._  
Moreover, we can identify a quite general family of consistent abstract theories for which _all_ their solutions are always \(\mathcal{E}\)-complete. Consider atoms \(\mathtt{s}_{1}=(\&\mathtt{sum}\{x;y\}=\mathtt{4})\) and its complement \(\widehat{\mathtt{s}_{1}}=\mathtt{s}_{3}=(\&\mathtt{sum}\{x;y\}\ \mathtt{1}= \mathtt{4})\) from the above example. Assume that we have some set \(S\subseteq\mathcal{T}\) that contains none of the two.