# On the Semantics of Hybrid ASP Systems Based on Clingo
## 2 Background  
We start considering an alphabet consisting of two disjoint sets, namely, a set \(\mathcal{A}\) of _propositional_ (_regular_) _atoms_ and a set \(\mathcal{T}\) of _theory atoms_, whose truth is governed by some external theory. Several theory atoms may represent the same theory entity. We use letters a, s, and \(b\) for atoms in \(\mathcal{A}\), \(\mathcal{T}\), and \(\mathcal{A}\cup\mathcal{T}\), respectively. In clingo, these theory atoms are expressions preceded by '&', but their internal syntax is not predetermined: it can be defined by the user to build new extensions. As an example, the system clingcon extends the input language of clingo with linear equations, represented as theory atoms of the form  
\[\&\text{sum}\{k_{1}*x_{1};\ldots;k_{n}*x_{n}\}\prec k_{0} \tag{1}\]  
where for each \(i\) such that \(0\leq i\leq n\), each \(x_{i}\) is an integer variable and each \(k_{i}\in\mathbb{Z}\) is an integer constant, whereas \(\prec\) is a comparison symbol, such as \(\prec\)=, \(\text{t=}\), \(\text{<}\), \(\text{>}\)=. As we said above, we may have two different theory atoms, such as \(\&\text{sum}\{x\}{>0}\) and \(\&\text{sum}\{x\}{>=1}\), actually representing the same condition (as a linear equation). A _literal_ is any atom \(b\in\mathcal{A}\cup\mathcal{T}\) or its default negation \(\
eg b\). A \(\mathcal{T}\)-logic program over \(\langle\mathcal{A},\mathcal{T}\rangle\) is a set of rules of the form  
\[b_{0}\gets b_{1},\ldots,b_{n},\
eg b_{n+1},\ldots,\
eg b_{m} \tag{2}\]  
where \(b_{i}\in\mathcal{A}\cup\mathcal{T}\) for \(1\leq i\leq m\) and \(b_{0}\in\mathcal{A}\cup\mathcal{T}\cup\{\bot\}\) with \(\bot\
ot\in\mathcal{A}\cup\mathcal{T}\) denoting the fall-sum constant. We let notations \(h(r)\stackrel{{\text{def}}}{{=}}b_{0}\), \(B(r)\stackrel{{\text{def}}}{{=}}\{b_{1},\ldots,b_{n}\}\), and \(B(r)\stackrel{{\text{def}}}{{=}}\{b_{n+1},\ldots,b_{m}\}\) stand for the _head_, the _positive_, and the _negative body atoms_ of a rule \(r\) of the form of (2). The set of _body atoms_ of \(r\) is just \(B(r)\stackrel{{\text{def}}}{{=}}B(r)^{+}\cup B(r)^{-}\). Finally, the sets of _body_ and _head atoms_ of a program \(P\) are respectively defined as \(B(P)\stackrel{{\text{def}}}{{=}}\bigcup_{r\in P}B(r)\) and \(H(P)\stackrel{{\text{def}}}{{=}}\{h(r)\mid r\in P\}\setminus\{\bot\}\), as expected. An example of a system using \(\mathcal{T}\)-logic programs is the aforementioned clingcon, whose theory atoms correspond to linear integer equations. We refer to logic programs augmented by such theory atoms as clingcon-programs. Next, we describe the semantics of \(\mathcal{T}\)-logic programs in clingo[16], used for several extensions such as the addition of difference constraints in clingo[DL], of linear equations over integers in clingcon, and over reals in clingo[LP]. In all these systems, we can see the role of the corresponding external theory as a kind of _\"certification authority\"_ that sanctions regular stable models whose theory atoms are in accord with their underlying constraints. To this end, we envisage a two-step process: (1) generate regular stable models and (2) select the ones passing the theory certification. In step (1), we ignore the distinction between atoms in \(\mathcal{A}\) and \(\mathcal{T}\) and plainly apply the stable model semantics [2]. More precisely, a set \(X\subseteq\mathcal{A}\cup\mathcal{T}\) of atoms is a _model_ of a \(\mathcal{T}\)-logic program \(P\) over \(\langle\mathcal{A},\mathcal{T}\rangle\), if, for every rule \(r\in P\) such that \(B(r)^{+}\subseteq X\) and \(B(r)\cap X=\emptyset\), we have \(h(r)\in X\). In the case of an integrity constraint with \(h(r)=\bot\), note that \(\bot\) does not belong to \(X\subseteq\mathcal{A}\cup\mathcal{T}\). The stable models of \(P\) are defined via the _reluct_ of \(P\) relative to a set \(X\) of atoms, viz. \[P^{X}=\{h(r)\gets B(r)^{+}\mid r\in P,\,B(r)^{-}\cap X=\emptyset\}.\]  
Then, as usual, a set, \(X\), of atoms is a _stable model_ of \(P\) if \(X\) is the least model of \(P^{X}\).