# On the Semantics of Hybrid ASP Systems Based on Clingo
## 2 Background
In step (2), an external theory \(\mathfrak{T}\) is used to eliminate any stable model \(X\) whose theory atoms \(X\cap\mathcal{T}\) are not _in accord_ with \(\mathfrak{T}\). Suppose step (1) yields a stable model of a clingcon-programcontaining both atoms &sum\(\{x;2*y\}\)>9 and &sum\(\{2*x;4*y\}\) <=6. This stable model would not pass theory certification since no values for integer variables \(x\) and \(y\) can satisfy both corresponding linear equations, viz. \(x+2y>9\) and \(2x+4y\leq 6\) (note that the latter is equivalent to \(x+2y\leq 3\)). In fact, the treatment of each theory atom \(\mathsf{s}\) (as obtained in the stable model) leaves room for different semantic options [16]. The first option is about the justification for the truth of \(\mathsf{s}\) in step (1). A theory atom \(\mathsf{s}\) is called _defined_ if its truth must be derived through the program's rules. Otherwise, \(\mathsf{s}\) is said to be _external_, and we are always free to add it to the program without further justification. A second semantic option has to do with how we treat \(\mathsf{s}\
ot\in X\) for a stable model \(X\) in step (2). We say that \(\mathsf{s}\) is _strict_ when \(\mathsf{s}\
ot\in X\) implies that the theory check requires the \"opposite\" constraint of \(\mathsf{s}\) to be satisfied. Otherwise, we say that \(\mathsf{s}\) is _non-strict_, and the fact \(\mathsf{s}\
ot\in X\) has no relevant effect during theory certification. Of course, in both cases, \(\mathsf{s}\in X\) implies that the constraint of \(\mathsf{s}\) is satisfied. As an example, suppose that \(\mathsf{s}\) is the strict atom &sum\(\{2*x;4*y\}\)<=6, and we get \(\mathsf{s}\
ot\in X\) in some stable model \(X\). Then, step (2) imposes the same constraint as if we had obtained atom &sum\(\{2*x;4*y\}\)>6 in \(X\). [PERSON] et al. [14] argue that combinations (non-strict,defined) and (strict,external) are the only sensible ones for linear equation theories. With our focus on these theories, we follow this proposition, and partition the set \(\mathcal{T}\) of theory atoms into two disjoint sets, \(\mathcal{E}\) and \(\mathcal{F}\), standing for _external_ and _founded_ atoms, respectively. Intuitively, each external atom in \(\mathcal{E}\) is interpreted as (strict,external), so its truth requires no justification, whereas if we decide to make it false, then its corresponding opposite constraint must be considered in step (2). On the other hand, founded atoms in \(\mathcal{F}\) are those interpreted in a (non-strict,defined) manner, so they must be derived by the \(\mathcal{T}\)-logic program, and when they remain eventually false, they do not impose any additional constraint on the final solution. Additionally, we require that founded atoms do not occur in the rule bodies, that is, \(B(P)\cap\mathcal{F}=\emptyset\), for any program \(P\). We do allow external atoms to occur in the head, but, as we see later, they can always be equivalently shifted to the body. For the sake of brevity, we assume that an atom that only occurs in rule heads (but not in bodies) is founded unless explicitly stated otherwise. Let us emphasize that any atom that occurs in some body is mandatorily external, as discussed above. The signature of a program, \(P\), as described above, is denoted as \(\langle\mathcal{A},\mathcal{T},\mathcal{E}\rangle\), leaving \(\mathcal{F}\) implicit. With this restriction to two interpretations of theory atoms, we can formulate clingo's semantics for \(\mathcal{T}\)-logic programs as follows [16]: Informally speaking, a \(\mathfrak{T}\)-solution \(S\) is a subset \(S\subseteq\mathcal{T}\) of theory atoms whose associated constraints are \"sanctioned\" by abstract theory \(\mathfrak{T}\); this is made precise in Section 3.