# On the Semantics of Hybrid ASP Systems Based on Clingo
## 3 Transformation-Based Semantics Revisited
### Stable Models of Logic Programs with Abstract Theories
If the two atoms are considered external, that is, \(\{\mathtt{s}_{1},\mathtt{s}_{3}\}\subseteq\mathcal{E}\), then \(\mathit{Comp}_{\mathcal{E}}(S)\) must include their complements, which are the two atoms themselves again, since \(\widehat{\widehat{\mathtt{s}_{1}}}=\mathtt{s}_{1}\). However, then, \(\mathit{Comp}_{\mathcal{E}}(S)\) becomes inconsistent, and so it cannot be a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-solution for any consistent abstract theory. As a result, if the theory is consistent and \(\mathcal{E}\) is closed, that is, it contains all the complements of its elements, then all solutions must be \(\mathcal{E}\)-complete:  
Proposition 2: _Let \(\mathfrak{T}=\langle\mathcal{T},\mathit{Sat},\widehat{\cdot}\rangle\) be a consistent abstract theory with a closed set of external atoms \(\mathcal{E}\subseteq\mathcal{T}\). Then, all \(\langle\mathfrak{T},\mathcal{E}\rangle\)-solutions \(S\subseteq\mathcal{T}\) are \(\mathcal{E}\)-complete._  
In analogy to Section 2, a set \(X\subseteq\mathcal{A}\cup\mathcal{T}\) of atoms is a \(\langle\mathfrak{T},\mathcal{E}\rangle\)-_stable model_ of a \(\mathcal{T}\)-logic program \(P\), if there is some \(\langle\mathfrak{T},\mathcal{E}\rangle\)-solution \(S\) such that \(X\) is a stable model of the program in (3). As an example, take again the clingcon-program consisting of rules (4) and (5) with abstract theory \(\mathfrak{L}\), the already seen theory atoms \(\mathcal{T}=\{\mathtt{s}_{1},\mathtt{s}_{2},\mathtt{s}_{3},\mathtt{s}_{4}\}\), and the closed subset of external atoms \(\mathcal{E}=\{\mathtt{s}_{1},\mathtt{s}_{3}\}\). This program has two \(\langle\mathfrak{L},\mathcal{E}\rangle\)-stable models:  
\[X_{1} =\{\mathtt{a},\,\mathtt{s}_{1},\mathtt{s}_{2}\}=\{\mathtt{a},\, \&\mathtt{sum}\{x;y\}=\mathtt{4},\,\&\mathtt{sum}\{y;z\}=\mathtt{2}\}\text{ and } \tag{7}\] \[X_{2} =\{\mathtt{s}_{3}\}=\{\&\mathtt{sum}\{x;y\}\ \mathtt{1}= \mathtt{4}\}\]  
To verify \(X_{1}\), take the \(\langle\mathfrak{L},\mathcal{E}\rangle\)-solution \(\{\mathtt{s}_{1},\mathtt{s}_{2}\}=\{\&\mathtt{sum}\{x;y\}=\mathtt{4},\,\& \mathtt{sum}\{y;z\}=\mathtt{2}\}\) and the resulting program transformation  
a \[\leftarrow\&\mathtt{sum}\{x;y\}=\mathtt{4}\] (8) \[\&\mathtt{sum}\{y;z\}=\mathtt{2}\leftarrow\mathtt{a}\] (9) \[\&\mathtt{sum}\{x;y\}=\mathtt{4}\leftarrow\] (10)  
We see that \(X_{1}\) is a stable model of the logic program and, as such, also a \(\langle\mathfrak{L},\mathcal{E}\rangle\)-stable model. Similarly, with \(\langle\mathfrak{L},\mathcal{E}\rangle\)-solution \(\{\mathtt{s}_{3}\}=\{\&\mathtt{sum}\{x;y\}\ \mathtt{1}= \mathtt{4}\}\), we get program  
\[\mathtt{a} \leftarrow\&\mathtt{sum}\{x;y\}=\mathtt{4} \tag{11}\] \[\texttt{s}_{1}=\left(\,\texttt{\&sum}\{x;y\}\!=\!4\,\right) \qquad\texttt{s}_{3}=\left(\,\texttt{\&sum}\{x;y\}\!\mid=\!4\,\right)\]0 \[\texttt{s}_{1}=\left(\,\texttt{\&sum}\{x;y\}\!=\!4\,\right) \qquad\texttt{s}_{3}=\left(\,\texttt{\&sum}\{x;y\}\!\mid=\!4\,\right)\]1 \[\texttt{s}_{1}=\left(\,\texttt{\&sum}\{x;y\}\!=\!4\,\right) \qquad\texttt{s}_{3}=\left(\,\texttt{\&sum}\{x;y\}\!\mid=\!4\,\right)\]2Again, we have \(X_{2}\) as a stable model, confirming it as a \(\langle\mathfrak{L},\mathcal{E}\rangle\)-stable model. Notice that, in this case, the \(\langle\mathfrak{L},\mathcal{E}\rangle\)-solution \(\{\mathfrak{s}_{3}\}\) corresponding to \(X_{2}\) is not unique. For instance, we could also have the \(\langle\mathfrak{L},\mathcal{E}\rangle\)-solution \(\{\mathfrak{s}_{2},\mathfrak{s}_{3}\}=\{\&\mathtt{sum}\{y;z\}=2,\&\mathtt{sum} \{x;y\}\!=4\}\), which results in program (11). This program also has \(X_{2}\) as a stable model. As a third alternative, we could have the \(\langle\mathfrak{L},\mathcal{E}\rangle\)-solution \(\{\mathfrak{s}_{3},\mathfrak{s}_{4}\}=\{\&\mathtt{sum}\{x;y\}\!=4,\&\mathtt{sum}\{y;z\}\!=2\}\). This leads to the same program as \(\langle\mathfrak{L},\mathcal{E}\rangle\)-solution \(\{\mathfrak{s}_{3}\}\) and, therefore, it is also a valid witness for stable model \(X_{2}\).