# On the Semantics of Hybrid ASP Systems Based on Clingo
## 3 Transformation-Based Semantics Revisited
### Abstract Theories  
An _abstract theory_\(\mathfrak{T}\) is a triple \(\langle\mathcal{T},\mathit{Sat},\widehat{\cdot}\rangle\) where \(\mathcal{T}\) is the set of _theory atoms_ we can handle in the theory, \(\mathit{Sat}\subseteq 2^{\mathcal{T}}\) is the set of \(\mathfrak{T}\)_-satisfiable_ sets of theory atoms, and \(\widehat{\cdot}\colon\mathcal{T}\to\mathcal{T}\) is a function mapping theory atoms to their _complement_ such that \(\widehat{\widehat{\mathsf{s}}}=\mathsf{s}\) for any \(\mathsf{s}\in\mathcal{T}\). We define \(\widehat{S}=\{\widehat{\mathsf{s}}\mid\mathsf{s}\in S\}\) for any set \(S\subseteq\mathcal{T}\). Note that the set \(\mathit{Sat}\) acts as an oracle whose rationality is beyond our reach: to see if some set \(S\) of theory atoms is satisfiable, we may only check \(S\in\mathit{Sat}\). Despite the limited structure of such theories, some simple properties can be formulated: a set \(S\subseteq\mathcal{T}\) of theory atoms is  
* _inconsistent_, if both \(\mathsf{s}\in S\) and \(\widehat{\mathsf{s}}\in S\) for some atom \(\mathsf{s}\), (_consistent_ otherwise)
* \(\mathcal{Z}\)_-complete_ for some subset \(\mathcal{Z}\subseteq\mathcal{T}\), if for all \(\mathsf{s}\in\mathcal{Z}\), either \(\mathsf{s}\in S\) or \(\widehat{\mathsf{s}}\in S\), and
* _closed_, if \(\mathsf{s}\in S\) implies \(\widehat{\mathsf{s}}\in S\). The definition of completeness is relative to some subset \(\mathcal{Z}\subseteq\mathcal{T}\) of theory atoms, but when \(\mathcal{Z}=\mathcal{T}\), we simply say that \(S\) is _complete_. An abstract theory \(\mathfrak{T}=\langle\mathcal{T},\mathit{Sat},\widehat{\cdot}\rangle\) is _consistent_ or _complete_ if all its \(\mathfrak{T}\)-satisfiable sets \(S\in\mathit{Sat}\) are _consistent_ or _complete_, respectively. Note that any non-empty closed set \(S\
eq\emptyset\) is inconsistent but can be \(\mathfrak{T}\)-satisfiable (e.g., for paraconsistent theories). We mostly use closed sets to describe subtypes of theory atoms rather than satisfiable solutions. As an example, consider an abstract theory \(\mathfrak{L}=\langle\mathcal{T},\mathit{Sat},\widehat{\cdot}\rangle\) of linear equations that can be used to capture clingconprograms, where  
* \(\mathcal{T}\) is the set of all expressions of form (1),* _Sat_ is the set of all subsets \(S\subseteq\mathcal{T}\) of expressions of form (1) for which there exists an assignment of integer values to their variables that satisfies all the linear equations in \(S\) with their usual meaning, and
* the complement function is defined such as \(\widehat{\texttt{\&sum}\{\dots\}}\prec c\) is \(\widehat{\texttt{\&sum}\{\dots\}}\prec c\) with \(\overline{\prec}\) defined according to the following table: \begin{tabular}{|c|c|c|c|c|c|} \hline \(\prec\) & \(<=\) & \(=\) & \(!=\) & \(<\) & \(>\) & \(>=\) \\ \hline \(\prec\) & \(>\) & \(!=\) & \(=\) & \(>=\) & \(<=\) & \(<\) \\ \hline \end{tabular}  Note that the set of theory atoms in \(\mathfrak{E}\) is closed. Similarly, to cover \(\texttt{clingo[OI]}\)-programs, we introduce abstract theory \(\mathfrak{D}\) capturing _difference constraints_ over integers, which is a subset of the already seen abstract theory \(\mathfrak{L}\) where theory atoms have the fixed form \(\texttt{\&sum}\{1*x;(-1)*y\}\!<=k\) but are rewritten instead as:  
\[\texttt{\&diff}\{x-y\}\!<=k \tag{6}\]  
where \(x\) and \(y\) are integer variables and \(k\in\mathbb{Z}\). Even though this definition of abstract theories is limited to a minimum set of requirements (no particular syntax, a set _Sat_ used for satisfiability testing and a complement function), we can already define an abstract form of entailment as follows. **Definition 1** (Abstract Entailment). : _Let \(\mathfrak{T}=\langle\,\mathcal{T},\mathcal{S},\mathcal{T}\,\rangle\) be an abstract theory. We say that a set \(S\subseteq\mathcal{T}\) of theory atoms entails a theory atom \(s\in\mathcal{T}\), written \(S\mathrel{\left|\vbox to 0.0 pt{\hbox{\scriptsize$\approx$}}\right.