# On the Semantics of Hybrid ASP Systems Based on Clingo
## 2 Background
A set \(X\subseteq\mathcal{A}\cup\mathcal{T}\) of atoms is a \(\mathfrak{T}\)-stable model of a \(\mathcal{T}\)-logic program \(P\) over \(\langle\mathcal{A},\mathcal{T},\mathcal{E}\rangle\), if there is some \(\mathfrak{T}\)-solution \(S\) such that \(X\) is a stable model of the logic program  
\[P\cup\{\mathsf{s}\leftarrow\ |\ \ \mathsf{s}\in(S\cap\mathcal{E})\}\cup\{\bot \leftarrow\ \mathsf{s}\ |\ \ \mathsf{s}\in(\mathcal{T}\cap H(P))\setminus S\}\;. \tag{3}\]  
That is, external atoms in \(S\) are added as facts to the program, whereas for any theory atom \(\mathsf{s}\) occurring as a rule head but not in \(S\), we add the constraint \(\bot\leftarrow\mathsf{s}\). For illustration, consider the clingo-program \(P_{(4/5)}\):  
\[\mathsf{a} \leftarrow \ \&\mathsf{sum}\{x;y\}\text{=}4 \tag{4}\] \[\&\mathsf{sum}\{y;z\}\text{=}2 \leftarrow\mathsf{a} \tag{5}\]  
This program contains two theory atoms: &sum\(\{x;y\}\text{=}4\) and &sum\(\{y;z\}\text{=}2\). We refer to them by \(\mathsf{s}_{1}\) and \(\mathsf{s}_{2}\), respectively. Theory atom \(\mathsf{s}_{1}\) is external since it occurs in the body of a rule, whereas we decide that \(\mathsf{s}_{2}\) is founded. As explained above, the absence of any external atom, \(\mathsf{s}\in\mathcal{T}\), in our candidate set, \(\mathsf{s}\
ot\in S\), imposes its complementary constraint to be satisfied. This is the so-called \"strict\" behavior. For this reason, we assume that, for any external atom, there always exists another external atom that is associated with that complementary constraint, even if this complementary atom does not occur in the program. We formalize this intuition in Section 3 below. In our example, since \(\mathsf{s}_{1}\) is external, we require a second, implicit external atom \(\&\mathsf{sum}\{x;y\}\)!= 4, which we name \(\mathsf{s}_{3}\), for short, and which stands for the complement of \(\mathsf{s}_{1}\). As a result, our example deals with two external atoms \(\mathcal{E}=\{\mathsf{s}_{1},\mathsf{s}_{3}\}\) that are complementary to each other and one defined atom \(\mathcal{F}=\{\mathsf{s}_{2}\}\). Another consequence of the strict behavior is that any candidate \(\mathfrak{T}\)-solution \(S\) must contain either \(\mathsf{s}_{1}\) or \(\mathsf{s}_{3}\), because the absence of one of them implies forcing the other, whereas the two of them cannot be selected at the same time because they are inconsistent altogether. To obtain the stable models of \(P_{(4/5)}\), we must decide first which candidate set \(S\) of theory atoms are actually \(\mathfrak{T}\)-solutions. Although the definition of \(\mathfrak{T}\)-stable models starts by considering each \(\mathfrak{T}\)-solution \(S\) and builds an associated program (3) afterward, in practice, we can just start from any possible candidate set of theory atoms \(S\) to form program (3) and just check if they form a \(\mathfrak{T}\)-solution once we obtain the stable models \(X\) for that program. In our example, we are free to either add the external atom \(\mathsf{s}_{1}\) or its complement \(\mathsf{s}_{3}\) as a fact. If we decide to leave \(\mathsf{s}_{2}\
otin S\), we must add the constraint \(\leftarrow\mathsf{s}_{2}\). This amounts to two possibilities: \(X_{1}=\{\mathsf{s}_{1},\mathsf{s}_{2},\mathsf{a}\}\) and \(X_{2}=\{\mathsf{s}_{3}\}\). If \(\mathfrak{T}\) is the theory of linear equations, it is not difficult to see that \(S_{1}=X_{1}\cap\mathcal{T}=\{\mathsf{s}_{1},\mathsf{s}_{2}\}\) is a \(\mathfrak{T}\)-solution because the associated constraints \(x+y=4\) and \(y+z=2\) are satisfiable: as a justification take, for instance, the variable assignment \(\{x\mapsto 2,\,y\mapsto 2,\,z\mapsto 0\}\). When we use a variable assignment in this way, we say that it constitutes a _witness_ of satisfiability for the set of constraints.