# On the Semantics of Hybrid ASP Systems Based on Clingo
## Appendix A Examples of Abstract Theories
Proof of Proposition 4.: By construction, for every \(\mathfrak{T}\)-satisfiable set \(S\in\mathcal{S}\), we have \(\bigcap_{\mathsf{s}\in S}[\,\mathsf{s}\,]_{\mathfrak{T}}\
eq\emptyset\). Then, there exists a valuation \(v\in\bigcap_{\mathsf{s}\in S}[\,\mathsf{s}\,]_{\mathfrak{T}}\) and \(v\in[\,\mathsf{s}\,]_{\mathfrak{T}}\) for every \(\mathsf{s}\in S\). This implies that \(\mathfrak{T}\) is compositional. Let us show that \(\mathfrak{T}\) is consistent. Suppose, for the sake of contradiction, that there exists a \(\mathfrak{T}\)-satisfiable set \(S\in\mathcal{S}\) such that \(\{\mathsf{s},\widehat{\mathsf{s}}\}\in S\) for a \(s\in\mathcal{T}\). Then, since \(\mathfrak{T}\) is compositional (as shown above), there has to exist a valuation, \(v\), such that \(v\in[\,\mathsf{s}\,]\) and \(v\in[\,\widehat{\mathsf{s}}\,]\). By definition of the denotation \([\,\cdot\,]_{\mathfrak{T}}\), this implies that \(v\) needs to satisfy both \(\sum_{1\leq i\leq n}c_{i}\ast v(x_{i})\prec c_{0}\) and \(\sum_{1\leq i\leq n}c_{i}\ast v(x_{i})\prec c_{0}\), which is a contradiction. Therefore, every \(\mathfrak{T}\)-satisfiable set \(S\in\mathcal{S}\) is consistent, and then \(\mathfrak{T}\) is consistent. Proof of Proposition 5.: We proceed by contraposition: suppose \([\,S\,]_{\mathfrak{T}}\subseteq[\,\mathsf{s}\,]_{\mathfrak{T}}\) and \(S\
ot\in_{\mathfrak{T}}^{\prime}s\). Then \(S\cup\widehat{S}\) is satisfiable, that is, there exists a valuation \(v\in[\,S\,]_{\mathfrak{T}}\cap[\,\widehat{\mathsf{s}}\,]\). However, then, on the one hand, \(v\in\bigcap_{v^{\prime}\in S}[\,s^{\prime}\,]_{\mathfrak{T}}\) and the latter is included in \([\,\mathsf{s}\,]_{\mathfrak{T}}\), so we obtain \(v\in[\,\mathsf{s}\,]_{\mathfrak{T}}\). On the other hand, \(v\in[\,\widehat{\mathsf{s}}\,]_{\mathfrak{T}}\) and so \(v\in[\,s\,]_{\mathfrak{T}}\cap[\,\widehat{\mathsf{s}}\,]_{\mathfrak{T}}\), meaning that \(\{s,\widehat{s}\}\) is satisfiable and contradicts the consistency of \(\mathfrak{T}\). Proof of Proposition 6.: Since \(\mathfrak{T}\) is compositional, proving \((S\cup\{\widehat{\mathsf{s}}\})\
ot\in\mathcal{S}\) amounts to checking \([\,S\cup\{\widehat{\mathsf{s}}\}\,]_{\mathfrak{T}}=\emptyset\). For the left to right direction, \(S\models_{\Xi}s\) is equivalent to \([\![\,S\,]\!]_{\Xi}\subseteq[\![\,s\,]\!]_{\Xi}\). However, then \([\![\,S\,]\!]_{\Xi}\cap[\![\,\widehat{\mathfrak{s}}\,]\!]_{\Xi}\subseteq[\![\,s\,]\! ]_ {\Xi}\cap[\![\,\widehat{\mathfrak{s}}\,]\! ]_{\Xi}=\emptyset\) and so \([\![\,S\,]\!]_{\Xi}\cap[\![\,\widehat{\mathfrak{s}}\,]\!]_{\Xi}=[\! [\,S\cup\{ \widehat{\mathfrak{s}}\,\}\,]\!]_{\Xi}=\emptyset\). For the right to left direction, we proceed by contraposition. Suppose there is some \(v\in[\![\,S\,]\! ]_{\Xi}\) such that \(v\
ot\in[\![\,s\,]\!]_{\Xi}\). If the complement is absolute, the latter means \(v\in[\![\,\widehat{\mathfrak{s}}\,]\! ]_{\Xi}\) and so \(v\in[\![\,S\,]\!]_{\Xi}\cap[\![\,\widehat{\mathfrak{s}}\,]\!]_{\Xi}=[\! [\,S\cup \{\widehat{\mathfrak{s}}\,\}\,]\! ]_{\Xi}\) and so \([\![\,S\cup\{\widehat{\mathfrak{s}}\,\}\,]\! ]_{\Xi}\
eq\emptyset\). Proof of Proposition 7.: Let \(X\) be some \(\langle\mathfrak{Z},\mathcal{E}\rangle\)-stable model. By definition, there is some \(\langle\mathfrak{Z},\mathcal{E}\rangle\)-solution \(S\) such that \(X\) is a stable model of the program in (3). By construction of this program, it follows \(S\cap\mathcal{E}=X\cap\mathcal{E}\) and \(S\cap\mathcal{F}\supseteq X\cap\mathcal{F}\). In addition, since \(S\) is a \(\langle\mathfrak{Z},\mathcal{E}\rangle\)-solution, it follows that \(S\) is \(\mathfrak{Z}\)-satisfiable (\(S\) is complete by Proposition 2 and the fact that \(\mathcal{E}\) is closed). Let \(S^{\prime}=X\cap\mathcal{T}\). Then, \(S^{\prime}\subseteq S\) and, since \(\mathfrak{Z}\) is compositional and \(S\) is \(\mathfrak{Z}\)-satisfiable, it follows that \(S^{\prime}\) is also \(\mathfrak{Z}\)-satisfiable. That is, there is some valuation, \(v\), such that \(v\in[\![\,s\,]\! ]\) for all \(\mathfrak{s}\in S^{\prime}=X\cap\mathcal{T}\).