# On the Semantics of Hybrid ASP Systems Based on Clingo
## Appendix A Examples of Abstract Theories
Let \(v^{\prime}\) be the partial valuation that is only defined in \(\mathit{vars}(S^{\prime})\), and that satisfies \(v^{\prime}(x)=v(x)\) for all \(x\in\mathit{vars}(S^{\prime})\). Then, \(v^{\prime}\!\mid_{\mathit{vars}(X\cap\mathcal{T})}\in[\![\,s\,]\!]_{\Xi}\! \mid_{\mathit{vars}(X\cap\mathcal{T})}\) for all \(\mathfrak{s}\in S^{\prime}=X\cap\mathcal{T}\) and, thus, pair \((X\cap\mathcal{A},v^{\prime})\) belongs to \(\mathit{ans}(X)\). Proof of Proposition 8.: We start by showing that, if \((Y,v)\) is a \(\langle\mathfrak{Z},\mathcal{E}\rangle\)-answer set, then \(stb_{P}(Y,v)\) is a \(\langle\mathfrak{Z},\mathcal{E}\rangle\)-stable model \(X\) of \(P\) such that \((Y,v)\) belongs to \(\mathit{ans}(X)\). Since \((Y,v)\) is a \(\langle\mathfrak{Z},\mathcal{E}\rangle\)-answer set, there is a stable model \(X\) such that \((Y,v)\) belongs to \(\mathit{ans}(X)\). We will show that \(stb_{P}(Y,v)=X\). By definition,  
\[C ::= A\mid C\sqcap C\mid\forall R.C\mid\exists R\mid\
eg C\]7 \[C ::= A\mid C\sqcap C\mid\forall R.C\mid\exists R\mid\
eg C\]8 \[C ::= A\mid C\sqcap C\mid\forall R.C\mid\exists R\mid\
eg C\]9  
Let us now show that  
\[f_{\
u}(A) \stackrel{{\mathrm{def}}}{{=}} v(A)\qquad\text{for any concept name }A\in\mathcal{X}_{c}\]0  
Pick any theory atom \(\mathfrak{s}\in\mathcal{E}\) such that \(\mathfrak{s}\
otin X\). Since \(X\) is a stable model, 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 program (3), this implies \(\mathfrak{s}\
otin S\). Furthermore, since \(\mathcal{E}\) is closed, \(S\) is complete (Proposition 2) and thus, both \(\widehat{\mathfrak{s}}\in S\) and \(\widehat{\mathfrak{s}}\in X\) follow. Then, \(v\in[\![\,\widehat{\mathfrak{s}}\,]\! ]_{\Xi}\!\mid_{\mathit{domain}(v)}\) and since the complement is absolute, it follows that \(v\
otin[\![\,s\,]\!]_{\Xi}\!\mid_{\mathit{domain}(v)}\). Hence, \(\mathfrak{s}\
otin stb_{P}(Y,v)\cap\mathcal{E}\) and  
\[f_{\
u}(A) \stackrel{{\mathrm{def}}}{{=}} v(A)\qquad\text{for any concept name }A\in\mathcal{X}_{c}\]1  
Let us now show that  
\[f_{\
u}(A) \stackrel{{\mathrm{def}}}{{=}} v(A)\qquad\text{for any concept name }A\in\mathcal{X}_{c}\]2 (A6)  
Pick \(\mathfrak{s}\in X\cap\mathcal{F}\). Then, there is a rule \((B\to\mathfrak{s})\in P\) such that \(b\in X\) for \(b\in B\cap\mathcal{A}\) and \(b^{\prime}\
ot\in X\) for \(\
eg b^{\prime}\in B\) and \(b^{\prime}\in\mathcal{A}\). This implies that \(b\in Y\) for \(b\in B\cap\mathcal{A}\) and \(b^{\prime}\
ot\in Y\) for \(\
eg b^{\prime}\in B\) and \(b^{\prime}\in\mathcal{A}\) and, thus, \((Y,v)\models_{\mathfrak{Z}}b\) and \((Y,v)\models_{\mathfrak{Z}}\
eg b^{\prime}\). Furthermore, for every \(b\in B\cap\mathcal{T}\), we have \(b\in X\) and, by construction, \(v\in[\![\,s\,]\! ]_{\Xi}\!\mid_{\mathit{domain}(v)}\) and thus \((Y,v)\models b\). Similarly, for every \(\
eg b\in B\) and \(b\in\mathcal{T}\) it holds that \(v\
otin[\![\,s\,]\! ]_{\Xi}\!\mid_{\mathit{domain}(v)}\) and, therefore, \((Y,v)\models\
eg b\). This implies that \((Y,v)\models_{\mathfrak{Z}}B\) and, thus, that \(\mathfrak{s}\in stb_{P}(Y,v)\cap\mathcal{F}\). Now, the other way around. Pick \(\mathfrak{s}\in\mathcal{F}\) such that \((B\to\mathfrak{s})\in P\text{ and }(Y,v)\models_{\mathfrak{Z}}B\). Then, \(B\cap\mathcal{A}\subseteq Y\subseteq X\), \(b^{\prime}\
ot\in Y\) for \(\
eg b^{\prime}\in B\) and \(b^{\prime}\in\mathcal{A}\) implying \(b^{\prime}\
ot\in X\), \(v\in[\![\,b\,]\! ]_{\Xi}\!\mid_{\mathit{domain}(v)}\) for \(b\in B\cap\mathcal{T}\) implying \(b\in X\cap\mathcal{T}\), and, \(v\
ot\in[\![\,b^{\prime}\,]\! ]_{\Xi}\!\mid_{\mathit{domain}(v)}\) for \(\
eg b^{\prime}\in B\) and \(b^{\prime}\in\mathcal{T}\) implying \(b^{\prime}\
ot\in X\cap\mathcal{T}\). Therefore, \(X\) satisfies rule body \(B\) and must include \(\mathfrak{s}\) since \(X\) is a stable model of \(P\).