Y_{i-1}$. Given any two elements $x,y\in Y_{i-1}$, it is furthermore easy to
see that $\\{a_{x},a_{x}^{\prime}\\}$ and $\\{a_{y},a_{y}^{\prime}\\}$ are
disjoint, as by property 2. and 3. of the induction hypothesis, there must be
some bit $j\in\\{1,\cdots,i-1\\}$ that $x$ and $y$ assign differently, which
subsequently must then also be assigned differently by
$\\{a_{x},a_{x}^{\prime}\\}$ and $\\{a_{y},a_{y}^{\prime}\\}$ due to Claim
(3), axioms (52) and (57), and CQs (68). As, thus, $|Y_{i}|=2|Y_{i-1}|$,
property 4. of the induction hypothesis implies $|Y_{i}|=2^{i}$.

This finishes the proof of Claim (4).

We go on to identify the instances in $\mathcal{I}$ that encode pairs of
vertices:

######  Claim 5.

We can identify a set $Y\subseteq{\sf Index}_{2n}^{\mathcal{I}}$ and a
bijective function $\vartheta:Y\rightarrow V^{2}$ such that
$\vartheta(x)=(v_{k},u_{l})$ implies $(x,{\sf val}_{b})\in{\sf
hBit}_{i}^{\mathcal{I}}$ iff the $i$-th bit in $\bar{k}\cdot\bar{l}$ is $b$
for all $b\in\\{{\sf t},{\sf f}\\}$ and $i\in\\{1,\cdots,2n\\}$.

Claim (5) builds upon Claim (4); set $Y=Y_{2n}$. By property 2. of Claim (4),
each $y\in Y$ assigns a unique $b\in\\{{\sf t},{\sf f}\\}$ to every $i$-th bit
with $i\in\\{1,\cdots,2n\\}$, encoded via $(y,{\sf val}_{b})\in{\sf
hBit}_{i}^{\mathcal{I}}$. Ergo, we can find a function $\vartheta:Y\rightarrow
V^{2}$ such that $\vartheta(y)=(v_{k},u_{l})$ implies $(y,{\sf
val}_{b})\in{\sf hBit}_{i}^{\mathcal{I}}$ iff the $i$-th bit in
$\bar{k}\cdot\bar{l}$ is $b$ for all $b\in\\{{\sf t},{\sf f}\\}$ and
$i\in\\{1,\cdots,2n\\}$.

Note that $\vartheta$ must be surjective, as by $|Y|=2^{2n}$ (property 4 of
Claim (4)) and the fact that all $x,y\in Y$ pairwise assign at least one bit
differently (property 3. of Claim (4)).

To see that $\vartheta$ is injective, consider some $x,y\in Y$ with
$\vartheta(x)=(v_{k},u_{l})=\vartheta(y)$. By definition of $\vartheta$, we
have that $(x,{\sf val}_{b})\in{\sf hBit}_{i}^{\mathcal{I}}$ iff $(y,{\sf
val}_{b})\in{\sf hBit}_{i}^{\mathcal{I}}$ for all with $b\in\\{{\sf t},{\sf
f}\\}$ and $i\in\\{1,\cdots,2n\\}$, and, together with property 2 of Claim
(4), even that $(x,{\sf val}_{\sf t})\in{\sf hBit}_{i}^{\mathcal{I}}$ iff
$(y,{\sf val}_{\sf f})\notin{\sf hBit}_{i}^{\mathcal{I}}$. Property 3. of
Claim (4) then entails $x=y$.

This finishes the proof of Claim (5).

We go on to extract $\pi$ from $\mathcal{I}$ and show that $\mathcal{I}$ is
sound in the sense that any two elements $x,y\in Y$ that encode the same
vertex also assign it the same color as defined by $\pi$.

######  Claim 6.

The relation $\pi:V\rightarrow\\{{\sf r},{\sf g},{\sf b}\\}$ with

$\displaystyle\begin{split}\pi(v)\coloneqq\\{c\in\\{{\sf r},{\sf g},{\sf
b}\\}\mid&\exists y\in Y\text{ such that }\vartheta(y)=(v,u)\\\ &\text{ and
}(y,c)\in{\sf hCol}^{\mathcal{I}}\\}.\end{split}$

is a function such that $(y,c_{1})\in{\sf hCol}^{\mathcal{I}}$ and
$(y,c_{2})\in{{\sf hCol}^{\prime}}^{\mathcal{I}}$ hold for all $y\in Y$ with
$\vartheta(y)=(v,u)$, $\pi(v)=c_{1}$ and $\pi(u)=c_{2}$.

Indeed, $\pi$ is a function: On one hand, Claim (3) and axioms (59) ensure the
existence of some $c,d\in\\{{\sf r},{\sf g},{\sf b}\\}$ such that
$(y,c)\in{\sf hCol}^{\mathcal{I}}$ and $(y,d)\in{\sf
hCol}^{\prime\mathcal{I}}$ for all $y\in Y$. On the other hand, $\pi(y)$ is
unique for all $y\in Y$: Assume to the contrary that there are two elements
$y,y^{\prime}\in Y$ such that $\vartheta(y)=(v,u)$ with $(y,c)\in{\sf
hCol}^{\mathcal{I}}$ and $\vartheta(y^{\prime})=(v,u^{\prime})$ with
$(y^{\prime},c^{\prime})\in{\sf hCol}^{\mathcal{I}}$ and $c^{\prime}\neq c$.
By definition of $\vartheta$, $y$ and $y^{\prime}$ assign the bits with
$1,\cdots,n$ the same, i.e., $(y,z)\in{\sf hBit}_{i}^{\mathcal{I}}$ iff
$(y^{\prime},z)\in{\sf hBit}_{i}^{\mathcal{I}}$. Furthermore, $c^{\prime}\neq
c$ yields $(c^{\prime},c)\in{\sf neq}^{\mathcal{I}}$ via axioms (50). Then,
however, there must be a homomorphism from CQ (69) to $\mathcal{I}$, which
contradicts the fact that $\mathcal{I}\not\models q$.

Now, consider some $y\in Y$ with $\vartheta(y)=(v,u)$, $\pi(v)=c_{1}$ and
$\pi(u)=c_{2}$. We first show that $(y,c_{1})\in{\sf hCol}^{\mathcal{I}}$. The
definition of $\pi$ requires the existence of some $y^{\prime}\in Y$ such that
$\vartheta(y^{\prime})=(v,u^{\prime})$ and $(y^{\prime},c_{1})\in{\sf
hCol}^{\mathcal{I}}$, while there must also be some $c\in\\{{\sf r},{\sf
g},{\sf b}\\}$ such that $(y,c)\in{\sf hCol}^{\mathcal{I}}$ via Claim (3) and
axioms (59). By $\vartheta(y)=(v,u)$ and
$\vartheta(y^{\prime})=(v,u^{\prime})$, Claim (5) implies that $(y,{\sf
val}_{b})\in{\sf hBit}_{i}^{\mathcal{I}}$ iff $(y^{\prime},{\sf
val}_{b})\in{\sf hBit}_{i}^{\mathcal{I}}$ for all $i\in\\{1,\cdots,n\\}$ and
$b\in\\{{\sf t},{\sf f}\\}$. Then, we have that $(c_{1},c)\notin{\sf
neq}^{\mathcal{I}}$ via CQs (69) and the fact that $\mathcal{I}\not\models q$.
Ergo, by Claim (3), and axioms (50) and (59), we have that $c=c_{1}$, i.e.,
$(y,c_{1})\in{\sf hCol}^{\mathcal{I}}$.

We go on to show that $(y,c_{2})\in{{\sf hCol}^{\prime}}^{\mathcal{I}}$.
Again, the definition of $\pi$ requires the existence of some $y^{\prime}\in
Y$ such that $\vartheta(y^{\prime})=(u,u^{\prime})$ and
$(y^{\prime},c_{2})\in{\sf hCol}^{\mathcal{I}}$, while there must also be some
$c\in\\{{\sf r},{\sf g},{\sf b}\\}$ such that $(y,c)\in{{\sf
hCol}^{\prime}}^{\mathcal{I}}$ via Claim (3) and axioms (59). By
$\vartheta(y)=(v,u)$ and $\vartheta(y^{\prime})=(v,u^{\prime})$, Claim (5)
implies that $(y,{\sf val}_{b})\in{\sf hBit}_{i+n}^{\mathcal{I}}$ iff
$(y^{\prime},{\sf val}_{b})\in{\sf hBit}_{i}^{\mathcal{I}}$ for all
$i\in\\{1,\cdots,n\\}$ and $b\in\\{{\sf t},{\sf f}\\}$. Then, we have that
$(c_{2},c)\notin{\sf neq}^{\mathcal{I}}$ via CQs (70) and the fact that
$\mathcal{I}\not\models q$. Ergo, by Claim (3), and axioms (50) and (59), we
have that $c=c_{1}$, i.e., $(y,c_{1})\in{{\sf hCol}^{\prime}}^{\mathcal{I}}$.

This finishes the proof of Claim (6).

As a last step before proving that $\pi$ indeed is a 3-coloring, we need to
argue that the computation of the logical gates within $\mathcal{I}$ is sound.

######  Claim 7.

For all $y\in Y$, we have that $\vartheta(y)\in E$ implies $(y,{\sf var}_{\sf
t})\in{\sf gate}_{\dot{g}}^{\mathcal{I}}$, where $\dot{g}$ is the output gate
of $C$.

As $\vartheta(y)\in E$ implies $C^{\dot{g}}(\bar{k},\bar{l})={\sf t}$, it
suffices to show that $C^{g}(\bar{k},\bar{l})=b$ implies $(y,{\sf
var}_{b})\in{\sf gate}_{g}^{\mathcal{I}}$ for all $y\in Y$ with
$\vartheta(y)=(u_{k},v_{l})$, gates $g$ in $C$ and $b\in\\{{\sf t},{\sf
f}\\}$. We do this per induction over the structure of $C^{g}$:

$g$ is an INPUT gate.

Let $C^{g}(\bar{k},\bar{l})=b$. Then, as $g$ is an INPUT gate, the $i_{g}$-th
bit in $\bar{k}\cdot\bar{l}$ must be $b$. Thus, $(y,{\sf var}_{b})\in{\sf
hBit}_{i_{g}}^{\mathcal{I}}$ by definition of $\vartheta$. Claim (3) and
axioms (61) entail $(y,{\sf var}_{b^{\prime}})\in{\sf gate}_{g}^{\mathcal{I}}$
for some $b^{\prime}\in\\{{\sf t},{\sf f}\\}$. Finally, $(y,{\sf
var}_{b})\in{\sf hBit}_{i_{g}}^{\mathcal{I}}$, axioms (52), CQs (71), and the
fact that $\mathcal{I}\not\models q$ entail $b^{\prime}=b$, i.e., $(y,{\sf
var}_{b})\in{\sf gate}_{g}^{\mathcal{I}}$.

$g$ is a NOT gate with parent $g^{\prime}$.

Let $C^{g}(\bar{k},\bar{l})=b$. As $g$ is a NOT gate with parent $g^{\prime}$,
we have that $C^{g^{\prime}}(\bar{k},\bar{l})=b^{\prime}$ for some
$b^{\prime}\in\\{{\sf t},{\sf f}\\}$ such that $b^{\prime}\neq b$. By the
induction hypothesis, we then have that $(y,{\sf var}_{b^{\prime}})\in{\sf
gate}_{g^{\prime}}^{\mathcal{I}}$. Claim (3) and axioms (61) entail $(y,{\sf
var}_{b^{\prime\prime}})\in{\sf gate}_{g}^{\mathcal{I}}$ for some
$b^{\prime\prime}\in\\{{\sf t},{\sf f}\\}$. Due to $b^{\prime}\neq b$, CQs
(72) and the fact that $\mathcal{I}\not\models q$, it must be so that
$b^{\prime\prime}=b$, i.e., $(y,{\sf var}_{b})\in{\sf
gate}_{g}^{\mathcal{I}}$.

$g$ is a AND or OR gate.

We omit the details, as these cases are very similar to the NOT case, except
that the respective semantics of the logical operators need to be applied.

We are now in the position to show that $\pi$ indeed is a 3-coloring. Assume
to the contrary that there is an edge $(v,u)\in E$ with
$\pi(v)=\pi(u)\coloneqq c$. Since $\theta$ is a bijection as of Claim (5),
there exists a unique $y\in Y$ such that $\vartheta(y)=(v,u)$. We have
$(y,\pi(v))\in{\sf hCol}^{\mathcal{I}}$ and $(y,\pi(u))\in{{\sf
hCol}^{\prime}}^{\mathcal{I}}$ by Claim (6), i.e., $(y,c)\in{\sf
hCol}^{\mathcal{I}}$ and $(y,c)\in{{\sf hCol}^{\prime}}^{\mathcal{I}}$.
Furthermore, by Claim (7), $(v,u)\in E$ entails $(y,{\sf var}_{\sf t})\in{\sf
gate}_{\dot{g}}^{\mathcal{I}}$. Together with axioms (51), there must be a
homomorphism from CQ (79) to $\Delta^{\mathcal{I}}$. However, this contradicts
the fact that $\mathcal{I}$ is a countermodel to $q$. Ergo, $\pi$ must indeed
be a 3-coloring, i.e., $G$ is 3-colorable. ∎

##  Appendix E Proofs for Section 4.2

See 10

###### Proof.

Before proving the lemma, we recall the set $E$ gathers elements
$e_{t_{1},t_{2}}$ which will serve as references for others with same types.
To lighten notation, we introduce the mapping $\mathsf{ref}:e\mapsto
e_{\mathsf{tp}_{\mathcal{A}}({e}),\mathsf{tp}_{\mathcal{I}}({e})}$ defined on
$\Delta^{\mathcal{I}}$.

“$1\Rightarrow 2$”. Assume $\mathcal{I}\models{\sf Circ_{\sf
CP}}(\mathcal{K})$. Consider $\mathcal{P}\subseteq\Delta^{\mathcal{I}}$ s.t.
${\left|{\mathcal{P}}\right|}\leq 2{\left|{\mathcal{T}}\right|}+1$. We first
verify that $\mathcal{I}_{\mathcal{P}}$ models $\mathcal{K}_{\mathcal{P}}$:

  * •

$\mathcal{I}_{\mathcal{P}}$ models $\mathcal{A}_{\mathcal{P}}$ as it inherits
interpretations of concepts on ${\sf ind}(\mathcal{A}^{\prime})$ from
$\mathcal{I}$, which is a model of $\mathcal{A}$.

  * •

Axioms in $\mathcal{T}$ with shape $\top\sqsubseteq{{A}}$,
${{A_{1}}}\sqcap{{A_{2}}}\sqsubseteq{{A}}$, ${{A}}\sqsubseteq{{\lnot B}}$ or
${{\lnot B}}\sqsubseteq{{A}}$ are satisfied since $\mathcal{I}_{\mathcal{P}}$
inherits interpretations of concept names from $\mathcal{I}$, which is a model
of $\mathcal{T}$.

  * •

Axioms in $\mathcal{T}$ with shape $A\sqsubseteq\exists r$ are witnessed with
an $r$-edge pointing to $w_{r}$.

  * •

Axioms in $\mathcal{T}$ with shape $\exists r\sqsubseteq A$ are satisfied
since every element in $\mathcal{I}_{\mathcal{P}}$ receiving some $r$-edge
already received some in $\mathcal{I}$ (and interpretations of concept names
are preserved).

  * •

Role inclusions $r\sqsubseteq s$ are satisfied directly from the definition of
$s^{\mathcal{I}_{\mathcal{P}}}$.

It remains to prove that $\mathcal{I}_{\mathcal{P}}$ also complies with ${\sf
CP}$. Assume to the contrary that there exists a model $\mathcal{J}^{\prime}$
of $\mathcal{K}_{\mathcal{P}}$ with $\mathcal{J}^{\prime}<_{\sf
CP}\mathcal{I}_{\mathcal{P}}$. Notice that, for each role $r$ s.t.
$r^{\mathcal{J}^{\prime}}\neq\emptyset$, there must be an element
$w_{r}^{\prime}\in(\exists r^{-})^{\mathcal{J}^{\prime}}$. We can chose such
an element $w_{r}^{\prime}$ for each such role $r$, and build the following
interpretation $\mathcal{J}$:

$\displaystyle\Delta^{\mathcal{J}}=\;$ $\displaystyle\Delta^{\mathcal{I}}$
$\displaystyle{{A}}^{\mathcal{J}}=\;$
$\displaystyle{{A}}^{\mathcal{J}^{\prime}}\cup\\{e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{J}^{\prime}}\mid\mathsf{ref}(e)\in
A^{\mathcal{J}^{\prime}}\\}$ $\displaystyle{{r}}^{\mathcal{J}}=\;$
$\displaystyle\\{(a,b)\mid\mathcal{K}\models r(a,b)\\}$
$\displaystyle\cup\\{(e,w_{s}^{\prime})\mid\mathsf{ref}(e)\in(\exists
s)^{\mathcal{J}^{\prime}},\mathcal{T}\models s\sqsubseteq r\\}$
$\displaystyle\cup\\{(w_{s}^{\prime},e)\mid\mathsf{ref}(e)\in(\exists
s)^{\mathcal{J}^{\prime}},\mathcal{T}\models s\sqsubseteq r^{-}\\}$

It is easily verified that $\mathcal{J}$ is a model of $\mathcal{K}$, the most
interesting cases being axioms in $\mathcal{T}$ with shape either
$A\sqsubseteq\exists r$ or $\exists r\sqsubseteq A$. The former are satisfied
using the witness $w_{r}$. The latter, when triggered on
$a\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{J}^{\prime}}$ due to a pair
$(a,b)$ s.t. $\mathcal{K}\models r(a,b)$, hold thanks to $\mathsf{ref}(a)$
having same ABox-type as $a$. We now prove $\mathcal{J}<_{\sf CP}\mathcal{I}$,
which will contradict $\mathcal{I}\models{\sf Circ_{\sf CP}}(\mathcal{K})$. It
suffices to prove that for each concept name $A$ and
$\odot\in\\{\subseteq,\supseteq\\}$, we have $A^{\mathcal{J}}\odot
A^{\mathcal{I}}$ iff $A^{\mathcal{J}^{\prime}}\odot
A^{\mathcal{I}_{\mathcal{P}}}$. Let $A$ be a concept name. We prove the claim
for $\odot=\;\subseteq$ only; for $\odot=\;\supseteq$, the arguments are
similar.

“$\Rightarrow$”. Let $A^{\mathcal{J}}\subseteq A^{\mathcal{I}}$ and $d\in
A^{\mathcal{J}^{\prime}}$. In particular, $d\in A^{\mathcal{J}}$ by definition
of $A^{\mathcal{J}}$. Thus, by hypothesis, $d\in A^{\mathcal{I}}$, and since
$d\in\Delta^{\mathcal{J}^{\prime}}=\Delta^{\mathcal{I}_{\mathcal{P}}}$ we
obtain $d\in A^{\mathcal{I}_{\mathcal{P}}}$ by definition of
$A^{\mathcal{I}_{\mathcal{P}}}$.

“$\Leftarrow$”. Let $A^{\mathcal{J}^{\prime}}\subseteq
A^{\mathcal{I}_{\mathcal{P}}}$ and $d\in A^{\mathcal{J}}$; we need to show
$d\in A^{\mathcal{I}}$. It is straightforward if
$d\in\Delta^{\mathcal{J}^{\prime}}$. Otherwise, we know that
$\mathsf{ref}(d)\in A^{\mathcal{J}^{\prime}}$ by definition of
$A^{\mathcal{J}}$. Therefore $\mathsf{ref}(d)\in
A^{\mathcal{I}_{\mathcal{P}}}$ by hypothesis, that is
$A\in\mathsf{tp}_{\mathcal{I}}({\mathsf{ref}(d)})$. Since $d$ and
$\mathsf{ref}(d)$ have same type, it yields
$A\in\mathsf{tp}_{\mathcal{I}}({d})$, that is $d\in A^{\mathcal{I}}$.

“$2\Rightarrow 1$”. Assume $\mathcal{I}_{\mathcal{P}}\models{\sf Circ_{\sf
CP}}(\mathcal{K}_{\mathcal{P}})$ for all
$\mathcal{P}\subseteq\Delta^{\mathcal{I}}$ s.t.
${\left|{\mathcal{P}}\right|}\leq 2{\left|{\mathcal{T}}\right|}+1$. By
hypothesis, we already have $\mathcal{I}\models\mathcal{K}$. By contradiction,
assume now there exists $\mathcal{J}<\mathcal{I}$. Based on $\mathcal{J}$, we
build a subset $\mathcal{P}\subseteq\Delta^{\mathcal{J}}$ containing:

  * •

for each role $r$ s.t. $r^{\mathcal{J}}\neq\emptyset$, an element
$w_{r}^{\prime}\in(\exists r^{-})^{\mathcal{J}}$;

  * •

for each $A\in\mathsf{M}$ s.t. $A^{\mathcal{J}}\not\subseteq A^{\mathcal{I}}$,
an element $e_{A}\in B^{\mathcal{J}}\setminus B^{\mathcal{I}}$ for some
$B\prec A$ (Condition 3 in the definition of $\mathcal{J}<_{\sf
CP}\mathcal{I}$ ensures existence of such $B$ and $e_{A}$);

  * •

an element $e_{\mathsf{M}}\in A^{\mathcal{J}}\setminus A^{\mathcal{I}}$ for
some $A\in\mathsf{M}$ s.t. $A^{\mathcal{J}}\subsetneq A^{\mathcal{I}}$ and for
all $B\prec A$, $B^{\mathcal{J}}=B^{\mathcal{I}}$ (Condition 4 in the
definition of $<_{\sf CP}$ ensures the existence of such $A$ and
$e_{\mathsf{M}}$).

Notice $\mathcal{P}$ has size at most $2{\left|{\mathcal{T}}\right|}+1$. We
now build $\mathcal{J}^{\prime}$ as:

$\displaystyle\Delta^{\mathcal{J}^{\prime}}=\;$
$\displaystyle\Delta^{\mathcal{I}_{\mathcal{P}}}$
$\displaystyle{{A}}^{\mathcal{J}^{\prime}}=\;$
$\displaystyle{{A}}^{\mathcal{J}}\cap\Delta^{\mathcal{J}^{\prime}}$
$\displaystyle{{r}}^{\mathcal{J}^{\prime}}=\;$
$\displaystyle\\{(e,w_{s}^{\prime})\mid e\in(\exists
s)^{\mathcal{J}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}},\mathcal{T}\models
s\sqsubseteq r\\}$ $\displaystyle\cup\\{(w_{s}^{\prime},e)\mid e\in(\exists
s)^{\mathcal{J}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}},\mathcal{T}\models
s\sqsubseteq r^{-}\\}$

It is easily verified that $\mathcal{J}^{\prime}$ is a model of
$\mathcal{K}_{\mathcal{P}}$, and we now prove $\mathcal{J}^{\prime}<_{\sf
CP}\mathcal{I}_{\mathcal{P}}$, which will contradict
$\mathcal{I}_{\mathcal{P}}\models{\sf Circ_{\sf
CP}}(\mathcal{K}_{\mathcal{P}})$. We now check that all four conditions from
the definition of $<_{\sf CP}$ are satisfied:

  1. 1.

By definition, we have
$\Delta^{\mathcal{J}^{\prime}}=\Delta^{\mathcal{I}_{\mathcal{P}}}$.

  2. 2.

Let $A\in\mathsf{F}$. Definitions of $\mathcal{I}_{\mathcal{P}}$ and
$\mathcal{J}^{\prime}$ ensure
$A^{\mathcal{I}}\cap{\Delta^{\mathcal{I}_{\mathcal{P}}}}=A^{\mathcal{I}_{\mathcal{P}}}$
and
$A^{\mathcal{J}}\cap{\Delta^{\mathcal{I}_{\mathcal{P}}}}=A^{\mathcal{J}^{\prime}}$.
From $\mathcal{J}<_{\sf CP}\mathcal{I}$, we get
$A^{\mathcal{I}}=A^{\mathcal{J}}$, which thus yields
$A^{\mathcal{I}_{\mathcal{P}}}=A^{\mathcal{J}^{\prime}}$.

  3. 3.

Let $A\in\mathsf{M}$ such that $A^{\mathcal{J}^{\prime}}\not\subseteq
A^{\mathcal{I}_{\mathcal{P}}}$. Therefore $A^{\mathcal{J}}\not\subseteq
A^{\mathcal{I}}$, and recall we kept in $\mathcal{P}$ an element $e_{A}\in
B^{\mathcal{J}}\setminus B^{\mathcal{I}}$ for some $B\prec A$ to belong to
$\mathcal{P}$. Joint with $B^{\mathcal{J}^{\prime}}\subseteq
B^{\mathcal{I}_{\mathcal{P}}}$ being trivial, $e_{A}$ additionally witnesses
that $B^{\mathcal{J}^{\prime}}\subsetneq B^{\mathcal{I}_{\mathcal{P}}}$.

  4. 4.

Recall we kept in $\mathcal{P}$ an element $e_{\mathsf{M}}\in
A^{\mathcal{J}}\setminus A^{\mathcal{I}}$ for some $A\in\mathsf{M}$ s.t.
$A^{\mathcal{J}}\subsetneq A^{\mathcal{I}}$ and for all $B\prec A$,
$B^{\mathcal{J}}=B^{\mathcal{I}}$. It gives immediately that
$A^{\mathcal{J}^{\prime}}\subsetneq A^{\mathcal{I}_{\mathcal{P}}}$ and for all
$B\prec A$, $B^{\mathcal{J}^{\prime}}=B^{\mathcal{I}_{\mathcal{P}}}$.

This proves $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{I}_{\mathcal{P}}$,
contradicting $\mathcal{I}_{\mathcal{P}}\models{\sf Circ_{\sf
CP}}(\mathcal{K}_{\mathcal{P}})$ as desired. ∎

See 8

###### Proof.

We exhibit an NP procedure to decide the complement of our problem, that is
existence of a countermodel for UCQ $q$ over $\textrm{DL-Lite}_{\sf
bool}^{\cal H}$ cKB ${\sf Circ_{\sf CP}}(\mathcal{K})$. Our procedure starts
by guessing an interpretation $\mathcal{I}$ whose domain has size at most
$|\mathcal{A}|+(2^{|\mathcal{T}|+2}+1)^{3|q|}$. This can be done in linearly
many non-deterministic steps (w.r.t. data complexity) It further checks
whether $\mathcal{I}$ is a model of $\mathcal{K}$ that does not entail $q$ and
rejects otherwise. This can essentially be done naively in
${\left|{\Delta^{\mathcal{I}}}\right|}^{{\left|{\mathcal{T}}\right|}{\left|{q}\right|}}$
deterministic steps, that is still polynomial w.r.t. data complexity. The
procedure finally checks whether $\mathcal{I}$ complies with ${\sf CP}$ by
iterating over each $\mathcal{P}$ with ${\left|{\mathcal{P}}\right|}\leq
2{\left|{\mathcal{T}}\right|}+1$ and checking whether there exists a model
$\mathcal{J}_{\mathcal{P}}$ of $\mathcal{K}$ s.t.
$\mathcal{J}_{\mathcal{P}}<\mathcal{I}_{\mathcal{P}}$. If, for a choice of
$\mathcal{P}$ and we can find such a $\mathcal{J}_{\mathcal{P}}$, then our
procedure rejects. Notice that iterating over such $\mathcal{P}$ can be done
in ${\left|{\Delta^{\mathcal{I}}}\right|}^{2{\left|{\mathcal{T}}\right|}+1}$
iterations since we require ${\left|{\mathcal{P}}\right|}\leq
2{\left|{\mathcal{T}}\right|}+1$. Computing $\mathcal{I}_{\mathcal{P}}$
follows directly from the choice of $\mathcal{P}$. Since each
$\mathcal{I}_{\mathcal{P}}$ has constant size w.r.t. data complexity,
iterating over each possible $\mathcal{J}_{\mathcal{P}}$ can be done naively
with constantly many steps. Overall, the procedure uses a linear number of
non-deterministic steps at the beginning and further performs several checks
using a polynomial number of additional deterministic steps.

It remains to prove that an accepting run exists if there is a countermodel
for $q$ over ${\sf Circ_{\sf CP}}(\mathcal{K})$. If there exists an accepting
run, then the corresponding guessed interpretation $\mathcal{I}$ is a model of
$\mathcal{K}$ that does not entail $q$, and the “$2\Rightarrow 1$” direction
from Lemma 10 ensures it also comply+ies with ${\sf CP}$. Conversely, if there
exists a countermodel, then Lemma 7 ensures existence of a countermodel
$\mathcal{I}$ whose domain has size at most
$|\mathcal{A}|+(2^{|\mathcal{T}|+2}+1)^{3|q|}$. The procedure can guess this
$\mathcal{I}$, and as $\mathcal{I}$ is indeed a model of $\mathcal{K}$ not
entailing $q$, it will not be rejected. The “$1\Rightarrow 2$” direction from
Lemma 9 further ensures $\mathcal{I}$ also passes the remaining checks
performed by the procedure. ∎

See 9

###### Proof.

We reduce the complement of the graph 3-colorability problem (3Col) to
evaluating the Boolean CQ:

$q=\exists y_{1}\,\exists y_{2}\,\exists
y~{}\mathsf{edge}(y_{1},y_{2})\land\mathsf{hasCol}(y_{1},y)\land\mathsf{hasCol}(y_{2},y)$

over the $\textrm{DL-Lite}_{\sf pos}$ TBox:

$\mathcal{T}=\\{\mathsf{Vertex}\sqsubseteq\exists\mathsf{hasCol},\exists\mathsf{hasCol}^{-}\sqsubseteq\mathsf{Color}\\},$

where $\mathsf{Color}$ is minimized while all other predicates vary. Let ${\sf
CP}$ be the resulting circumscription pattern. Given an instance
$\mathcal{G}=(\mathcal{V},\mathcal{E})$ of 3Col, we build an ABox
$\mathcal{A}$ containing the following assertions:

$\displaystyle\mathsf{Vertex}(v)$ $\displaystyle\text{ for all
}v\in\mathcal{V}$ (80) $\displaystyle\mathsf{edge}(v_{1},v_{2})$
$\displaystyle\text{ for all }\\{v_{1},v_{2}\\}\in\mathcal{E}$ (81)
$\displaystyle\mathsf{Color}(c)$ $\displaystyle\text{ for all
}c\in\\{r,g,b\\}$ (82)

We now prove the following claim:

$\mathcal{G}\notin\text{3Col}\iff{\sf Circ_{\sf CP}}(\mathcal{K})\models q$

First notice that every model $\mathcal{I}$ of ${\sf Circ_{\sf
CP}}(\mathcal{K})$ verifies $\mathsf{Color}^{\mathcal{I}}=\\{r,g,b\\}$.
Indeed, by contradiction, if $\mathcal{I}$ contains
$e\in\mathsf{Color}^{\mathcal{I}}\setminus\\{r,g,b\\}$, then we can build
$\mathcal{J}$ a model of $\mathcal{K}$ with $\mathcal{J}<_{\sf CP}\mathcal{I}$
by modifying $\mathcal{I}$ as follows:

  * •

remove $e$ from $\mathsf{Color}^{\mathcal{I}}$, that is
$\mathsf{Color}^{\mathcal{J}}=\mathsf{Color}^{\mathcal{I}}\setminus\\{e\\}$;

  * •

reroute $\mathsf{hasCol}$ as: $\mathsf{hasCol}^{\mathcal{J}}=\\{(v,r)\mid
v\in(\exists\mathsf{hasCol})^{\mathcal{I}}\\}$.

It is then straightforward that $\mathcal{J}$ satisfies the desired
properties, contradicting $\mathcal{I}$ being a model of ${\sf Circ_{\sf
CP}}(\mathcal{K})$.

“$\Rightarrow$”. Assume $\mathcal{G}\notin\text{3Col}$ and consider a model
$\mathcal{I}$ of $\mathcal{J}$. By the above remark, we have
$\mathsf{Color}^{\mathcal{I}}=\\{r,g,b\\}$ and from $\mathcal{I}$ being a
model of $\mathcal{K}$, we can find a mapping
$\tau:\mathcal{V}\rightarrow\\{r,g,b\\}$ of $\mathcal{G}$ such that for all
$v\in\mathcal{V}$, if $\tau(v)=c$ then
$(v,c)\in\mathsf{hasCol}^{\mathcal{I}}$. Since, by assumption,
$\mathcal{G}\notin\text{3Col}$, there exists an edge
$\\{v_{1},v_{2}\\}\in\mathcal{E}$ such that $\tau(v_{1})=\tau(v_{2})=c$ for
some $c\in\\{r,g,b\\}$, which ensures $y_{1}\mapsto v_{1},y_{2}\mapsto
v_{2},y\mapsto c$ is an homomorphism of $q$ in $\mathcal{I}$.

“$\Leftarrow$”. Assume $\mathcal{G}\in\text{3Col}$ and consider a 3-coloring
$\tau:\mathcal{V}\rightarrow\\{r,g,b\\}$. We build a model
$\mathcal{I}_{\tau}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$ by interpreting all
concepts and roles as in $\mathcal{A}$ except for $\mathsf{hasCol}$, which is
interpreted as:

$\mathsf{hasCol}^{\mathcal{I}_{\tau}}=\\{(v,c)\mid
v\in\mathcal{V},\tau(v)=c\\}.$

It is straightforward that $\mathcal{I}$ models ${\sf Circ_{\sf
CP}}(\mathcal{K})$ and does not embed $q$ (since $\tau$ is a 3-coloring). ∎

##  Appendix F Proofs for Section 5.1

We briefly discuss the variation of Proposition 1 mentioned in the main part
of the paper. Assume given a circumscribed $\mathcal{ALCHIO}$ KB ${\sf
Circ_{\sf CP}}(\mathcal{K})$ with $\mathcal{K}=(\mathcal{T},\mathcal{A})$, an
AQ $A_{0}(x)$ and an individual $a_{0}\in\mathsf{ind}(\mathcal{A})$. We again
replace all occurrences of a nominal $a$ with fresh concept $A_{a}$, add
$A_{a}(a),B_{a}(a)$ to $\mathcal{A}$, minimize $B_{a}$ and set $B_{a}\prec A$
for all $A\in\mathsf{M}$. However, in contrast with Proposition 1, we also add
axioms $A_{a}\sqcap\neg B_{a}\sqsubseteq\exists r.(X\sqcap A_{0})$ and
$X\sqsubseteq Y$ to $\mathcal{T}$ for some fresh concept names $X$ and $Y$ and
fresh role name $r$, and $Y(a_{0})$ to $\mathcal{A}$. Finally, we also
minimize $Y$ with higher preference than concepts from $\mathsf{M}$: We set
$Y\prec A$ for all $A\in\mathsf{M}$. Denoting ${\sf Circ}_{{\sf
CP}^{\prime}}(\mathcal{K}^{\prime})$ the resulting circumscribed
$\mathcal{ALCHI}$ KB, it can then be verified that ${\sf Circ_{\sf
CP}}(\mathcal{K})\models A_{0}(a_{0})$ iff ${\sf Circ}_{{\sf
CP}^{\prime}}(\mathcal{K}^{\prime})\models A_{0}(a_{0})$.

We now move to a proof of Theorem 11.

See 11

###### Proof.

Let ${\sf Circ}_{\sf CP}(\mathcal{K})$ be a circumscribed $\mathcal{ALC}$ KB,
with $\mathcal{K}=(\mathcal{T},\mathcal{A})$, $A_{0}$ an AQ, and $a_{0}\in{\sf
ind}(\mathcal{A})$. We construct a circumscribed ${\cal EL}$ KB ${\sf
Circ}_{\sf CP}(\mathcal{K}^{\prime})$, with
$\mathcal{K}^{\prime}=(\mathcal{T}^{\prime},\mathcal{A}^{\prime})$, such that
${\sf Circ}_{\sf CP}(\mathcal{K})\models A_{0}(a_{0})$ iff ${\sf Circ}_{\sf
CP}(\mathcal{K}^{\prime})\models A_{0}(a_{0})$.

With ${\cal ELU}_{\bot}$, we mean the extension of ${\cal EL}$ with
disjunction and $\bot$. It is well-known that every $\mathcal{ALC}$ TBox
$\mathcal{T}$ can be rewritten in polynomial time into an ${\cal ELU}_{\bot}$
TBox $\mathcal{T}^{\ast}$ that is a conservative extension of $\mathcal{T}$ in
the sense that every model of $\mathcal{T}^{\ast}$ is a model of $\mathcal{T}$
and every model of $\mathcal{T}$ can be extended to a model of
$\mathcal{T}^{\ast}$ by interpreting the fresh concept and role names in
$\mathcal{T}^{\ast}$ (?). It follows that ${\sf Circ}_{\sf
CP}(\mathcal{K})\models A_{0}(a_{0})$ iff ${\sf Circ}_{\sf
CP}(\mathcal{T}^{\ast},\mathcal{A})\models A_{0}(a_{0})$, assuming that all
the fresh concept names in $\mathcal{T}^{\ast}$ vary in ${\sf CP}$. In the
following, we recall the rewriting, which proceeds in three steps:

  1. 1.

_Remove value restrictions_ by replacing every subconcept $\forall r.C$ with
$\neg\exists r.\neg C$.

  2. 2.

_Remove negation of compound concepts_ by replacing every subconcept $\neg C$,
with $C$ compound, by $\neg X$ where $X$ is a fresh concept name, and adding
the CIs

$C\sqsubseteq X\qquad X\sqsubseteq C.$

  3. 3.

_Remove negation entirely_ by replacing every subconcept $\neg A$ with the
fresh concept name $\overline{A}$, and adding the CIs

$\top\sqsubseteq A\sqcup\overline{A}\qquad
A\sqcap\overline{A}\sqsubseteq\bot.$

We may thus assume w.l.o.g. that the TBox $\mathcal{T}$ in the given
circumscribed KB $\mathcal{K}$ is an ${\cal ELU}_{\bot}$ TBox. We may further
assume that disjunction occurs in $\mathcal{T}$ only in CIs of the form

$B\sqsubseteq B_{1}\sqcup B_{2}$

where $B,B_{1},B_{2}$ are concept names, by replacing every disjunction
$C_{1}\sqcup C_{2}$ with a fresh concept name $X$ and adding the CIs

$\begin{array}[]{r@{\;}c@{\;}lcr@{\;}c@{\;}lcr@{\;}c@{\;}l}X&\sqsubseteq&Y_{1}\sqcup
Y_{2}&&Y_{1}&\sqsubseteq&X&&Y_{2}&\sqsubseteq&X\\\\[2.84526pt]
C_{i}&\sqsubseteq&Y_{i}&&Y_{i}&\sqsubseteq&C_{i}&&\text{for
}i\in\\{1,2\\}\end{array}$

where also $Y_{1},Y_{2}$ are fresh concept names. Finally, we may assume that
$\mathcal{T}$ contains only a single CI $B\sqsubseteq B_{1}\sqcup B_{2}$ by
replacing every such CI with

$B\sqsubseteq\exists r_{B_{1},B_{2}}.D\quad\exists
r_{B_{1},B_{2}}.D_{1}\sqsubseteq B_{1}\quad\exists
r_{B_{1},B_{2}}.D_{2}\sqsubseteq B_{2}$

where $r_{B_{1},B_{2}}$ is a fresh role name and $D,D_{1},D_{2}$ are fresh
concept names, and adding the CI

$D\sqsubseteq D_{1}\sqcup D_{2}.$

We may clearly also assume that $\bot$ occurs in $\mathcal{T}$ only in the
form $C\sqsubseteq\bot$ with $C$ an ${\cal EL}$-concept. Note that the TBoxes
resulting from these transformations are conservative extensions of the
original ones. In ${\sf CP}$, all of the freshly introduced concept names
vary.

We are now ready for the actual reduction, which combines ideas from the
proofs of Theorems 2 and 4. To construct the TBox $\mathcal{T}^{\prime}$, We
start with relativized versions of the ${\cal EL}$-CIs in $\mathcal{T}$. For
an ${\cal EL}$ concept $C$, inductively define the concept $C_{X}$ as follows:

$\displaystyle A_{X}$ $\displaystyle\coloneqq X\sqcap A$
$\displaystyle(\exists r.D)_{X}$ $\displaystyle\coloneqq X\sqcap\exists
r.D_{X}$ $\displaystyle\top_{X}$ $\displaystyle\coloneqq X$
$\displaystyle(D\sqcap D^{\prime})_{X}$ $\displaystyle\coloneqq D_{X}\sqcap
D^{\prime}_{X}$

We then include in $\mathcal{T}^{\prime}$ all CIs

$\displaystyle C_{X}\sqsubseteq D_{X}$ (83)

such that $C\sqsubseteq D\in\mathcal{T}$ is neither the unique disjunctive CI
$B\sqsubseteq B_{1}\sqcup B_{2}$ nor of the form $C\sqsubseteq\bot$. To
construct the ABox $\mathcal{A}^{\prime}$, we start with the extension of
$\mathcal{A}$ by

$\displaystyle X(a)\quad\text{ for all }a\in{\sf ind}(\mathcal{A}).$ (84)

Of course, we need to compensate for removing the mentioned CIs. To simulate
the disjunctive CI $B\sqsubseteq B_{1}\sqcup B_{2}$, we extend
$\mathcal{T}^{\prime}$ with

$\displaystyle B$ $\displaystyle\sqsubseteq\exists r_{D}.(D\sqcap{\sf
Pos})\qquad\exists r_{D}.D_{1}\sqsubseteq B_{1}$ (85) $\displaystyle B$
$\displaystyle\sqsubseteq\exists r_{D}.(D\sqcap{\sf Neg})\qquad\exists
r_{D}.D_{2}\sqsubseteq B_{2}$ (86)

where $D,D_{1},D_{2},{\sf Pos}$, and ${\sf Neg}$ are fresh concept names and
$r_{D}$ is a fresh role name. We update ${\sf CP}$ so that $D$ is minimized.
We further extend $\mathcal{A}$ with the assertions

$\displaystyle D(d_{1}^{+})$ $\displaystyle D(d_{1}^{-})$ $\displaystyle
D(d_{2}^{+})$ $\displaystyle D(d_{2}^{-})$ (87) $\displaystyle
D_{1}(d_{1}^{+})$ $\displaystyle D_{1}(d_{1}^{-})$ $\displaystyle
D_{2}(d_{2}^{+})$ $\displaystyle D_{2}(d_{2}^{-})$ (88) $\displaystyle{\sf
Pos}(d_{1}^{+})$ $\displaystyle{\sf Neg}(d_{1}^{-})$ $\displaystyle{\sf
Pos}(d_{2}^{+})$ $\displaystyle{\sf Neg}(d_{2}^{-}).$ (89)

where $d^{+}_{1},d^{-}_{1},d^{+}_{2},d^{-}_{2}$ are fresh individuals. Note
that these individuals are _not_ marked with $X$, exempting them from
$\mathcal{T}$ is why the CIs from $\mathcal{T}$ are relativized in
$\mathcal{T}^{\prime}$. Note that the way we simulate disjunction is similar
to how we choose truth values in the proof of Theorem 4, and also the reason
for using a positive and a negative witness is the same. We need to make sure
that the positive and negative witnesses are distinct, which is achieved by
otherwise making the query true. To this end, we introduce a fresh role name
$u$ and fresh concept names $G,A_{0}^{\prime}$. We update ${\sf CP}$ so that
$G$ is minimized and extend $\mathcal{T}^{\prime}$ with:

$\displaystyle{\sf Pos}\sqcap{\sf Neg}$ $\displaystyle\sqsubseteq\exists
u.(G\sqcap A^{\prime}_{0})$ (90) $\displaystyle A_{0}$
$\displaystyle\sqsubseteq A^{\prime}_{0}$ (91)

We add $G(a_{0})$ to $\mathcal{A}^{\prime}$ and the new query is
$A^{\prime}_{0}$.

To compensate for removing the CIs $C\sqsubseteq\bot$, we consider another
fresh concept name $M$ and update ${\sf CP}$ so that $M$ is minimized. We
further extend $\mathcal{T}^{\prime}$ with

$\displaystyle C\sqsubseteq M\sqcap\exists u.(G\sqcap
A^{\prime}_{0})\quad\text{ for all }C\sqsubseteq\bot\in\mathcal{T}.$ (92)

So if a concept $C$ with $C\sqsubseteq\bot\in\mathcal{T}$ is satisfied, then
we force the minimized concept name $M$ to be non-empty and make the (new)
query true.

Let ${\sf CP}^{\prime}$ be the extended circumscription pattern. It remains to
establish the correctness of the reduction.
Claim. ${\sf Circ_{\sf CP}}(\mathcal{K})\models A_{0}(a_{0})$ iff ${\sf
Circ_{\sf CP}}(\mathcal{K}^{\prime})\models A^{\prime}_{0}(a_{0})$.
To prepare for the proof of the claim, we first observe that every model
$\mathcal{I}$ of $\mathcal{K}$ gives rise to a model $\mathcal{I}^{\prime}$ of
$\mathcal{K}^{\prime}$ in a natural way. More precisely, we set
$\Delta^{\mathcal{I}^{\prime}}=\Delta^{\mathcal{I}}\uplus\\{d^{+}_{1},d^{-}_{1},d^{+}_{2},d^{-}_{2}\\}$,
define the extension of all concept and role names that occur in $\mathcal{K}$
exactly as in $\mathcal{I}$, and interpret the fresh concept and role names as
follows:

$\begin{array}[]{rcl}X^{\mathcal{I}^{\prime}}&=&\Delta^{\mathcal{I}}\\\\[2.84526pt]
D^{\mathcal{I}^{\prime}}&=&\\{d^{+}_{1},d^{-}_{1},d^{+}_{2},d^{-}_{2}\\}\\\\[2.84526pt]
D_{i}^{\mathcal{I}^{\prime}}&=&\\{d^{+}_{i},d^{-}_{i}\\}\text{ for
}i\in\\{1,2\\}\\\\[2.84526pt] {\sf
Pos}^{\mathcal{I}^{\prime}}&=&\\{d^{+}_{1},d^{+}_{2}\\}\\\\[2.84526pt] {\sf
Neg}^{\mathcal{I}^{\prime}}&=&\\{d^{-}_{1},d^{-}_{2}\\}\\\\[2.84526pt]
r_{D}^{\mathcal{I}^{\prime}}&=&\\{(d,d^{+}_{1}),(d,d^{-}_{1})\mid d\in(B\sqcap
B_{1})^{\mathcal{I}}\\}\,\cup\\\\[2.84526pt]
&&\\{(d,d^{+}_{2}),(d,d^{-}_{2})\mid d\in(B\sqcap
B_{2})^{\mathcal{I}}\\}\\\\[1.42262pt] {\sf
check}^{\mathcal{I}^{\prime}}&=&\\{(a_{0},a)\mid a\in{\sf
ind}(\mathcal{A})\\\\[2.84526pt]
{A^{\prime}_{0}}^{\mathcal{I}^{\prime}}&=&A_{0}^{\mathcal{I}}\\\\[2.84526pt]
u^{\mathcal{I}^{\prime}}&=&\emptyset\\\\[2.84526pt]
M^{\mathcal{I}^{\prime}}&=&\emptyset\\\\[2.84526pt]
G^{\mathcal{I}^{\prime}}&=&\\{a_{0}\\}\\\\[2.84526pt] \end{array}$

It is easily checked that ${\mathcal{I}^{\prime}}$ is indeed a model of
$\mathcal{K}^{\prime}$. Now for the actual proof of the claim

“$\Leftarrow$”. Assume that ${\sf Circ_{\sf CP}}(\mathcal{K})\not\models
A_{0}(a_{0})$. Then there is a model $\mathcal{I}$ of $\mathcal{K}$ that is
minimal w.r.t. ${\sf CP}$ and satisfies $\mathcal{I}\not\models A_{0}(a_{0})$.
Let ${\mathcal{I}^{\prime}}$ be the corresponding model of
$\mathcal{K}^{\prime}$ defined above. We clearly have
${\mathcal{I}^{\prime}}\not\models A^{\prime}_{0}(a_{0})$. To show that ${\sf
Circ_{\sf CP}}(\mathcal{K}^{\prime})\not\models A^{\prime}_{0}(a_{0})$, it
thus remains to show that $\mathcal{I}^{\prime}$ is minimal w.r.t. ${\sf
CP}^{\prime}$.

Assume to the contrary that there is a model $\mathcal{J}^{\prime}<_{{\sf
CP}^{\prime}}\mathcal{I}^{\prime}$ of $\mathcal{K}^{\prime}$. As
$\mathcal{I}^{\prime}$ interprets $D,M,$ and $G$ minimally among all models of
$\mathcal{K}^{\prime}$, we must have
$D^{\mathcal{J}^{\prime}}=D^{\mathcal{I}^{\prime}}=\\{d^{+}_{1},d^{-}_{1},d^{+}_{2},d^{-}_{2}\\}$,
$M^{\mathcal{J}^{\prime}}=\emptyset$, and
$G^{\mathcal{J}^{\prime}}=G^{\mathcal{I}^{\prime}}=\\{a_{0}\\}$. We show that
the restriction $\mathcal{J}$ of $\mathcal{J}^{\prime}$ to domain
$X^{\mathcal{J}^{\prime}}$ is a model of $\mathcal{K}$. Moreover,
$\mathcal{J}^{\prime}<_{{\sf CP}^{\prime}}\mathcal{I}^{\prime}$,
$D^{\mathcal{J}^{\prime}}=D^{\mathcal{I}^{\prime}}$,
$M^{\mathcal{J}^{\prime}}=M^{\mathcal{I}^{\prime}}$, and
$G^{\mathcal{J}^{\prime}}=G^{\mathcal{I}^{\prime}}$ imply $\mathcal{J}<_{\sf
CP}\mathcal{I}$, which then yields a contradiction against the minimality of
$\mathcal{I}$.

Based on the facts that $\mathcal{J}^{\prime}$ is a model of
$\mathcal{A}^{\prime}$, ${\sf ind}(\mathcal{A})\subseteq
X^{\mathcal{J}^{\prime}}$ due to (84), and
$\mathcal{A}\subseteq\mathcal{A}^{\prime}$, it is clear that $\mathcal{J}$ is
a model of $\mathcal{A}$. Moreover, since $\mathcal{J}^{\prime}$ is a model of
$\mathcal{T}^{\prime}$, by construction of $\mathcal{J}$ it is easy to see
that $\mathcal{J}$ satisfies all CIs in $\mathcal{T}$ with the possible
exceptions of the disjunctive CI $B\sqsubseteq B_{1}\sqcup B_{2}$ and the CIs
of the form $C\sqsubseteq\bot$. The former, however, is satisfied due to CIs
(85) and (86) and since
$D^{\mathcal{J}^{\prime}}=\\{d^{+}_{1},d^{-}_{1},d^{+}_{2},d^{-}_{2}\\}$. And
the latter is satisfied due to the CIs (92) and since
$M^{\mathcal{J}^{\prime}}=\emptyset$.

“$\Rightarrow$”. Assume that ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})\not\models A^{\prime}_{0}(a_{0})$. Then there is a
model $\mathcal{I}^{\prime}$ of $\mathcal{K}^{\prime}$ that is minimal w.r.t.
${\sf CP}^{\prime}$ and satisfies $\mathcal{I}^{\prime}\not\models
A^{\prime}_{0}(a_{0})$. We first argue that
$G^{\mathcal{I}^{\prime}}=\\{a_{0}\\}$ as, otherwise, we can find a model
$\mathcal{J}^{\prime}<_{{\sf CP}^{\prime}}\mathcal{I}^{\prime}$ of
$\mathcal{K}^{\prime}$, contradicting the minimality of
$\mathcal{I}^{\prime}$. We have $G^{\mathcal{I}^{\prime}}\subseteq\\{a_{0}\\}$
since $\mathcal{I}^{\prime}$ is a model of $\mathcal{A}^{\prime}$. Assume to
the contrary of what we want to show that the converse fails. Then we
construct $\mathcal{J}^{\prime}$ by modifying $\mathcal{I}^{\prime}$ as
follows:

  * •

set $G^{\mathcal{J}^{\prime}}=\\{a_{0}\\}$;

  * •

add $a_{0}$ to ${A^{\prime}_{0}}^{\mathcal{J}^{\prime}}$;

  * •

reroute $u$ as $u^{\mathcal{J}^{\prime}}=\\{(e,a_{0})\mid e\in(\exists
u)^{\mathcal{I}^{\prime}}\\}$.

It is easy to see that, indeed, $\mathcal{J}^{\prime}$ is still a model of
$\mathcal{K}^{\prime}$ and $\mathcal{J}^{\prime}<_{{\sf
CP}^{\prime}}\mathcal{I}^{\prime}$.

Since $\mathcal{I}^{\prime}$ satisfies CIs (85) and (86), for every $e\in
B^{\mathcal{I}^{\prime}}$ we can choose two elements $e^{+}\in(D\sqcap{\sf
Pos})^{\mathcal{I}^{\prime}}$ and $e^{-}\in(D\sqcap{\sf
Neg})^{\mathcal{I}^{\prime}}$ such that $(e,e^{+}),(e,e^{-})\in
r_{D}^{\mathcal{I}^{\prime}}$. If $e^{+}=e^{-}$ for some $e$, then by (90) and
$G^{\mathcal{I}^{\prime}}=\\{a_{0}\\}$, we have $a_{0}\in
A_{0}^{\mathcal{I}^{\prime}}$, which is impossible since
$\mathcal{I}^{\prime}\not\models A^{\prime}_{0}(a_{0})$. Thus $e^{+}\neq
e^{-}$ for all $e$.

We next argue that the following conditions are satisfied:

  1. 1.

for all $e\in B^{\mathcal{I}^{\prime}}$:
$\\{e^{+},e^{-}\\}\cap\\{d^{+}_{1},d^{-}_{1},d^{+}_{2},d^{-}_{2}\\}\neq\emptyset$;

  2. 2.

$M^{\mathcal{I}^{\prime}}=\emptyset$.

If, in fact, any of the above conditions are violated, then we can again find
a model $\mathcal{J}^{\prime}<_{{\sf CP}^{\prime}}\mathcal{I}^{\prime}$ of
$\mathcal{K}^{\prime}$, contradicting the minimality of
$\mathcal{I}^{\prime}$. We start with Condition 1.

Assume to the contrary that for some $e\in B^{\mathcal{I}^{\prime}}$,
$e^{+},e^{-}\notin\\{d^{+}_{1},d^{-}_{1},d^{+}_{2},d^{-}_{2}\\}$. Then we
construct $\mathcal{J}^{\prime}$ by modifying $\mathcal{J}$ as follows:

  * •

remove $e^{-}$ from $D^{\mathcal{J}^{\prime}}$;

  * •

add $e^{+}$ to ${\sf Neg}^{\mathcal{J}^{\prime}}$;

  * •

add $a_{0}$ to ${A^{\prime}_{0}}^{\mathcal{J}^{\prime}}$;

  * •

add $(e^{+},a_{0})$ to $u^{\mathcal{J}^{\prime}}$.

It is easy to see that, indeed, $\mathcal{J}^{\prime}$ is still a model of
$\mathcal{K}^{\prime}$ and $\mathcal{J}^{\prime}<_{{\sf
CP}^{\prime}}\mathcal{I}^{\prime}$.

In the case of Condition 2, we can construct the model $\mathcal{J}^{\prime}$
simply as $\mathcal{J}$ modified by setting
$M^{\mathcal{J}^{\prime}}=\emptyset$. The resulting $\mathcal{J}^{\prime}$ is
a model of $\mathcal{K}^{\prime}$. The CIs (92) are the only potentially
problematic items. But since $\mathcal{I}^{\prime}\not\models
A^{\prime}_{0}(a_{0})$ and $G^{\mathcal{I}^{\prime}}=\\{a_{0}\\}$, we can
infer from (92) that $C^{\mathcal{I}^{\prime}}=\emptyset$ for all
$C\sqsubseteq\bot\in\mathcal{T}$, and thus the same holds for
$\mathcal{J}^{\prime}$. Consequently, the CIs (92) are never triggered in
$\mathcal{J}^{\prime}$ and it is safe to set
$M^{\mathcal{J}^{\prime}}=\emptyset$.

Let $\mathcal{I}$ be the restriction of $\mathcal{I}^{\prime}$ to
$X^{\mathcal{I}^{\prime}}$. It can be verified that $\mathcal{I}^{\prime}$ is
a model of $\mathcal{A}$ and that it satisfies all CIs in $\mathcal{T}$ with
the possible exceptions of the disjunctive CI $B\sqsubseteq B_{1}\sqcup B_{2}$
and the CIs of the form $C\sqsubseteq\bot$. The former, however, is satisfied
by Condition 1 and due to CIs (85) and (86). And the latter is satisfied by
Condition 2 and due to CI (92).

Since $\mathcal{I}^{\prime}\not\models A^{\prime}_{0}(a_{0})$ and by (91), we
have $\mathcal{I}\not\models A_{0}(a_{0})$. To show that
$\mathcal{K}\not\models A_{0}(a_{0})$, it thus remains to show that
$\mathcal{I}$ is minimal w.r.t. $<_{\sf CP}$. Assume to the contrary that
there is a model $\mathcal{J}<_{\sf CP}\mathcal{I}$ of $\mathcal{K}$ and let
$\mathcal{J}^{\prime}$ be the corresponding model of $\mathcal{K}^{\prime}$
constructed at the beginning of the correctness proof. Since
$\mathcal{J}^{\prime}$ interprets the minimized concept names $D$, $M$, and
$G$ in a minimal way among the models of $\mathcal{K}^{\prime}$, it follows
from $\mathcal{J}<_{\sf CP}\mathcal{I}$ that $\mathcal{J}^{\prime}<_{{\sf
CP}^{\prime}}\mathcal{I}^{\prime}$, in contradiction to $\mathcal{I}^{\prime}$
being minimal. ∎

##  Appendix G Proofs for Section 5.2

We now move to a proof of Theorem 13, which strongly combines $\textrm{DL-
Lite}_{\sf bool}$ expressiveness with fixed concept names. Interestingly,
fixed concept names are actually not needed. Indeed, given a circumscribed
$\textrm{DL-Lite}_{\sf bool}$ KB ${\sf Circ_{\sf CP}}$ ($\mathcal{K}$), each
$A\in\mathsf{F}$ can be replaced by the two minimized predicates $A$ and
$\overline{A}$, where $\overline{A}$ is a fresh concept name set to be the
complement of $A$ via the $\textrm{DL-Lite}_{\sf bool}$ axioms
$\overline{A}\sqsubseteq\lnot A$ and $\lnot A\sqsubseteq\overline{A}$ that can
be added in the TBox. Concept names $A$ and $\overline{A}$ are then given
higher preference than any other concept name from the original set of
minimized concept names $\mathsf{M}$. It is then straightforward to verify
that the resulting circumscribed $\textrm{DL-Lite}_{\sf bool}$ KB ${\sf
Circ}_{{\sf CP}^{\prime}}(\mathcal{K}^{\prime})$ has the same models as ${\sf
Circ_{\sf CP}}(\mathcal{K})$ (up to the interpretation of $\overline{A}$,
which always equals the interpretation of $\lnot A$).

See 13

###### Proof.

The proof proceeds by reduction from the complement of the NExp-complete
Succinct-3COL problem. An instance of Succinct-3COL consists of a Boolean
circuit $\mathcal{C}$ with $2n$ input gates. The graph
$\mathcal{G}_{\mathcal{C}}$ encoded by $\mathcal{C}$ has $2^{n}$ vertices,
identified by binary encodings on $n$ bits. Two vertices $u$ and $v$, with
respective binary encodings $u_{1}\dots u_{n}$ and $v_{1}\dots v_{n}$, are
adjacent in $\mathcal{G}_{\mathcal{C}}$ iff $\mathcal{C}$ returns True when
given as input $u_{1}\dots u_{n}$ on its first $n$ gates and $v_{1}\dots
v_{n}$ on the second half. The problem of deciding if
$\mathcal{G}_{\mathcal{C}}$ is 3-colorable has been proven to be NExp-complete
in (?).

Let $\mathcal{C}$ be a Boolean circuit with $2n$ input gates. We build a
$\textrm{DL-Lite}_{\sf bool}$ cKB ${\sf Circ_{\sf CP}}(\mathcal{K})$ with
$\mathcal{K}=(\mathcal{T},\mathcal{A})$ s.t. the AQ $\mathsf{Goal}(x)$ admits
the individual $a$ as a certain answer iff $\mathcal{C}$ does not belong to
Succinct-3COL. Let us already clarify that ${\sf CP}$ uses three minimized
concept names, namely $\mathsf{Center}$, $\mathsf{AllPairs}$ and
$\mathsf{GoodCol}$, with the following preference relation $\prec$:

$\displaystyle\mathsf{Center}\prec\mathsf{AllPairs}\prec\mathsf{GoodCol}$ (93)

It also uses fixed concept names: each $\mathsf{Bit}_{i}$ for $1\leq i\leq 2n$
and the six concept names $\mathsf{R}_{1}$, $\mathsf{G}_{1}$,
$\mathsf{B}_{1}$, $\mathsf{R}_{2}$, $\mathsf{G}_{2}$ and $\mathsf{B}_{2}$,
which will be useful to represent binary encodings and color assignments
respectively. All other predicates vary.

Models of $\mathcal{K}$ contain a central element $a$, that we enforce via the
ABox $\mathcal{A}=\\{\mathsf{Center}(a)\\}$ and which will be unique by virtue
of the preference relation. This central element will further be used to
detect undesired behaviors of the models via the AQ. In a model, each element
represents a pair $(v_{1},v_{2})$ of vertices by its combination of fixed
concepts $\mathsf{Bit}_{i}$ with $1\leq i\leq 2n$ that corresponds to the
binary encodings of $v_{1}$ and $v_{2}$. To detect models that do not
represent all possible pairs, we require each element representing a pair
$(v_{1},v_{2})$ to “send” at the center a binary sequence of $2n$ bits that
must be different from the encoding of $(v_{1},v_{2})$. This is achieved by
the following axioms in $\mathcal{T}$:

$\displaystyle\top\sqsubseteq\;$ $\displaystyle\exists
r_{i}\sqcup\exists\overline{r_{i}}\quad\text{ for each }1\leq i\leq 2n$ (94)
$\displaystyle\exists r_{i}^{-}\sqsubseteq\;$
$\displaystyle\mathsf{Center}\qquad\text{ for each }1\leq i\leq 2n$ (95)
$\displaystyle\exists\overline{r_{i}}^{-}\sqsubseteq\;$
$\displaystyle\mathsf{Center}\qquad\text{ for each }1\leq i\leq 2n$ (96)
$\displaystyle\top\sqsubseteq\;$
$\displaystyle\mathop{\mathop{\mbox{\bigmathxx\char 116\relax}}}\limits_{0\leq
i\leq 2n}(\exists
r_{i}\sqcap\lnot\mathsf{Bit}_{i})\sqcup(\exists\overline{r_{i}}\sqcap\mathsf{Bit}_{i})$
(97)

We now require the number of sent sequences to be unique, if possible, via the
minimized concept name $\mathsf{AllPairs}$, triggered by the following axioms
in $\mathcal{T}$:

$\displaystyle\exists r_{i}^{-}\sqcap\exists\overline{r_{i}}^{-}\sqsubseteq\;$
$\displaystyle\mathsf{AllPairs}\quad\text{ for each }1\leq i\leq 2n$ (98)

Therefore, if (at least) a pair is not represented in a model, then _all_
elements can send the binary encoding of a same missing pair to avoid
instantiating $\mathsf{AllPairs}$. If, on the other hand, each pair is
represented (at least once), then the number of sent sequences cannot be
unique, and $\mathsf{AllPairs}$ must be satisfied on the central element $a$.
To detect this with the AQ, we add the following axiom to $\mathcal{T}$:

$\displaystyle\lnot\mathsf{AllPairs}\sqsubseteq\;$
$\displaystyle\mathsf{Goal}$ (99)

Now that we can detect whether all pairs are represented, we move to the
encoding of colors. The respective color of $v_{1}$ and $v_{2}$ is chosen
locally via the following axioms in $\mathcal{T}$:

$\displaystyle\top\sqsubseteq\;$
$\displaystyle\mathsf{R}_{1}\sqcup\mathsf{G}_{1}\sqcup\mathsf{B}_{1}$ (100)
$\displaystyle\top\sqsubseteq\;$
$\displaystyle\mathsf{R}_{2}\sqcup\mathsf{G}_{2}\sqcup\mathsf{B}_{2}$ (101)

Recall concept names $\mathsf{R}_{1},\mathsf{G}_{1},\mathsf{B}_{1}$ and
$\mathsf{R}_{2},\mathsf{G}_{2},\mathsf{B}_{2}$ are fixed. We additionally
enforce that if an element represents a pair $(v_{1},v_{2})$ corresponding to
an edge $\\{v_{1},v_{2}\\}$ in $\mathcal{G}_{\mathcal{C}}$, then it must
assign different colors to $v_{1}$ and $v_{2}$. This is achieved by computing
the output of $\mathcal{C}$ on input $v_{1}$ and $v_{2}$ via a fresh concept
$G$ for each gate $G$ of $\mathcal{C}$ and adding the following axioms in
$\mathcal{T}$:

$\displaystyle G\equiv\;$ $\displaystyle\mathsf{Bit}_{i}\quad\qquad\text{ if
}G\text{ is the }i^{\text{th}}\text{ input gate of }\mathcal{C}$ (102)
$\displaystyle G\equiv\;$ $\displaystyle G_{1}\sqcap G_{2}\quad\text{ if
}G\text{ is a $\land$-gate with inputs }G_{1},G_{2}$ (103) $\displaystyle
G\equiv\;$ $\displaystyle G_{1}\sqcup G_{2}\quad\text{ if }G\text{ is a
$\lor$-gate with inputs }G_{1},G_{2}$ (104) $\displaystyle G\equiv\;$
$\displaystyle\lnot G^{\prime}\quad\qquad\text{if }G\text{ is a $\lnot$-gate
with input }G^{\prime}$ (105)

Assuming the output gate of $\mathcal{C}$ is $G_{o}$, it now suffices to add
the following axioms in $\mathcal{T}$:

$\displaystyle G_{o}\sqcap\mathsf{R}_{1}\sqcap\mathsf{R}_{2}\sqsubseteq\;$
$\displaystyle\bot$ (106) $\displaystyle
G_{o}\sqcap\mathsf{G}_{1}\sqcap\mathsf{G}_{2}\sqsubseteq\;$
$\displaystyle\bot$ (107) $\displaystyle
G_{o}\sqcap\mathsf{B}_{1}\sqcap\mathsf{B}_{2}\sqsubseteq\;$
$\displaystyle\bot$ (108)

While the above allows ensuring that each element $e$ representing an edge
$\\{v_{1},v_{2}\\}$ assigns different colors to $v_{1}$ and $v_{2}$, there
might still be inconsistent colorings in the sense that $v_{1}$ might have
been assigned another color by some other element $e^{\prime}$ representing an
edge $\\{v_{1},v_{3}\\}$. To detect such inconsistent colorings, the central
element “scans” all colors assigned to a tested vertex, whose encoding
corresponds to a binary sequence of $n$ bits represented by dedicated concepts
$\mathsf{T}_{i}$. To do so, the interpretation of each $\mathsf{T}_{i}$ on the
center element is first copied by all elements via the following axioms in
$\mathcal{T}$, defined for each $1\leq i\leq n$:

$\displaystyle\top\sqsubseteq\;$ $\displaystyle\exists
t_{i}\sqcup\exists\overline{t_{i}}$ (109) $\displaystyle\exists
t_{i}^{-}\sqsubseteq\;$ $\displaystyle\mathsf{Center}\sqcap\mathsf{T}_{i}$
$\displaystyle\exists\overline{t_{i}}^{-}\sqsubseteq\;$
$\displaystyle\mathsf{Center}\sqcap\lnot\mathsf{T}_{i}$ (110)
$\displaystyle\exists t_{i}\sqsubseteq\;$ $\displaystyle\mathsf{T}_{i}$
$\displaystyle\exists\overline{t_{i}}\sqsubseteq\;$
$\displaystyle\lnot\mathsf{T}_{i}$ (111)

Each element representing a pair $(v_{1},v_{2})$ then compares whether the
encoding of either $v_{1}$ or $v_{2}$ matches the sequence $\mathsf{T}_{i}$,
via the following axioms:

$\displaystyle\bigsqcap_{1\leq i\leq
n}\left((\mathsf{Bit}_{i}\sqcap\mathsf{T}_{i})\sqcup(\lnot\mathsf{Bit}_{i}\sqcap\lnot\mathsf{T}_{i})\right)\equiv\;$
$\displaystyle\mathsf{Test}_{1}$ (112) $\displaystyle\bigsqcap_{1\leq i\leq
n}\left((\mathsf{Bit}_{n+i}\sqcap\mathsf{T}_{i})\sqcup(\lnot\mathsf{Bit}_{n+i}\sqcap\lnot\mathsf{T}_{i})\right)\equiv\;$
$\displaystyle\mathsf{Test}_{2}$ (113)

It then sends the corresponding assigned color back to the central element via
the following axioms in $\mathcal{T}$, defined for each
$C\in\\{\mathsf{R},\mathsf{G},\mathsf{B}\\}$:

$\displaystyle\mathsf{Test}_{1}\sqcap C_{1}\equiv\;$ $\displaystyle\exists
s_{C}$ (114) $\displaystyle\mathsf{Test}_{2}\sqcap C_{2}\equiv\;$
$\displaystyle\exists s_{C}$ (115) $\displaystyle\exists
s_{C}^{-}\sqsubseteq\,$ $\displaystyle\mathsf{Center}$ (116)

The center now detects whether it receives two different colors for the tested
vertex:

$\displaystyle\mathop{\mathop{\mbox{\bigmathxx\char
116\relax}}}\limits_{\begin{subarray}{c}C,C^{\prime}\in\\{\mathsf{R},\mathsf{G},\mathsf{B}\\}\\\
C\neq C^{\prime}\end{subarray}}(\exists s_{C}^{-}\sqcap\exists
s_{C^{\prime}}^{-})\equiv\;$ $\displaystyle\lnot\mathsf{GoodCol}$ (117)

where $\mathsf{GoodCol}$ is a minimized concept name, which forces the center
element to detect an inconsistent coloring if it exists. This is further
translated in terms of the AQ with:

$\displaystyle\lnot\mathsf{GoodCol}\sqsubseteq\;$ $\displaystyle\mathsf{Goal}$
(118)

We are now done with the construction of ${\sf Circ_{\sf CP}}(\mathcal{K})$.
It remains to prove that:

${\sf Circ_{\sf
CP}}(\mathcal{K})\models\mathsf{Goal}(a)\iff\mathcal{C}\notin\text{Succinct}\text{-}\text{3COL}.$

“$\Rightarrow$”. Assume $\mathcal{C}\in\text{Succinct}\text{-}\text{3COL}$ and
let
$\rho:\\{0,\dots,2^{n}-1\\}\rightarrow\\{\mathsf{R},\mathsf{G},\mathsf{B}\\}$
be a (legal) 3-coloring of the encoded graph $\mathcal{G}_{\mathcal{C}}$. We
build a model $\mathcal{I}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$ based on
$\rho$, whose domain $\Delta^{\mathcal{I}}$ contains $a$ and one fresh element
$e_{v_{1},v_{2}}$ per
$(v_{1},v_{2})\in\\{0,\dots,2^{n}-1\\}\times\\{0,\dots,2^{n}-1\\}$. Model
$\mathcal{I}$ further interprets concept and role names as follows:

$\displaystyle{\mathsf{Center}}^{\mathcal{I}}$
$\displaystyle=\mathsf{GoodCol}^{\mathcal{I}}=\mathsf{AllPairs}^{\mathcal{I}}=\\{a\\}$
$\displaystyle\mathsf{Bit}_{i}^{\mathcal{I}}$
$\displaystyle=\\{e_{v_{1},v_{2}}\mid i^{\text{th}}\text{ bit in
}(v_{1},v_{2})\text{ encoding is }1\\}$ $\displaystyle C_{i}^{\mathcal{I}}$
$\displaystyle=\\{e_{v_{1},v_{2}}\mid\rho(v_{i})=C\\}$ $\displaystyle G$
$\displaystyle=\\{e_{v_{1},v_{2}}\mid G\in\mathcal{C}\text{ evaluates to
}1\text{ on input }(v_{1},v_{2})\\}$ $\displaystyle\mathsf{Test}_{i}$
$\displaystyle=\\{e_{v_{1},v_{2}}\mid v_{i}=0\\}$
$\displaystyle\mathsf{Goal}^{\mathcal{I}}$
$\displaystyle=\mathsf{T}_{i}^{\mathcal{I}}=\emptyset$ $\displaystyle
r_{i}^{\mathcal{I}}$ $\displaystyle=\\{(e_{v_{1},v_{2}},a)\mid
i^{\text{th}}\text{ bit in }(v_{1},v_{2})\text{ encoding is }0\\}$
$\displaystyle\overline{r_{i}}^{\mathcal{I}}$
$\displaystyle=\\{(e_{v_{1},v_{2}},a)\mid i^{\text{th}}\text{ bit in
}(v_{1},v_{2})\text{ encoding is }1\\}$ $\displaystyle t_{i}^{\mathcal{I}}$
$\displaystyle=\emptyset$ $\displaystyle\overline{t_{i}}^{\mathcal{I}}$
$\displaystyle=\\{(e_{v_{1},v_{2}},a)\mid 0\leq v_{1},v_{2}\leq 2^{n}-1\\}$
$\displaystyle\begin{split}s_{C}&=\\{(e_{v_{1},v_{2}},a)\mid\rho(0)=C\\\
&\phantom{=\\{(e_{v_{1},v_{2}},a)\mid}\text{ and either }v_{1}=0\text{ or
}v_{2}=0\\}\end{split}$

Notice that we have arbitrarily chosen each element representing a pair to
send back to the center it’s own encoding in which all bits have been flipped
(see interpretations of roles $r_{i}$ and $\overline{r_{i}}$), and the tested
vertex to be $0$ (interpretations of each $\mathsf{T}_{i}$ being empty and
$t_{i}$, $\overline{t_{i}}$ and $\mathsf{T}_{i}$ being set accordingly). With
the two above remarks, it is easily verified $\mathcal{I}$ models
$\mathcal{K}$, and, by definition $a\notin\mathsf{Goal}^{\mathcal{I}}$. It
remains to verify $\mathcal{I}$ complies with ${\sf CP}$. By contradiction,
assume there exists $\mathcal{J}<_{\sf CP}\mathcal{I}$. Notice that from the
fixed predicates, $\mathcal{J}$ still encodes one instance of each possible
pair and the very same coloring $\rho$. From $\mathcal{J}$ being a model of
$\mathcal{A}$ , we have $a\in\mathsf{Center}^{\mathcal{J}}$. From
$\mathsf{Center}^{\mathcal{I}}=\\{a\\}$ and $\mathsf{Center}$ being the most
preferred minimized predicate, it follows that
$\mathsf{Center}^{\mathcal{J}}=\\{a\\}$ as otherwise we would have
$\mathcal{I}<_{\sf CP}\mathcal{J}$. Therefore, since each possible pair is
represented at least once, the $r_{i}$ and $\overline{r_{i}}$ mechanism
ensures $a\in\mathsf{AllPairs}^{\mathcal{J}}$. Together with
$\mathsf{AllPairs}^{\mathcal{I}}=\\{a\\}$ and $\mathsf{AllPairs}$ being second
most preferred minimized predicates, we obtain
$\mathsf{AllPairs}^{\mathcal{J}}=\\{a\\}$ (as otherwise, again, we would have
$\mathcal{I}<_{\sf CP}\mathcal{J}$). Finally, since the coloring encoded in
$\mathcal{J}$ must be exactly $\rho$, whatever the interpretations of concepts
$\mathsf{T}_{i}$, the concept $\exists s_{C}^{-}\sqcap\exists
s_{C^{\prime}}^{-}$ will always be empty for all
$C,C^{\prime}\in\\{\mathsf{R},\mathsf{G},\mathsf{B}\\}$ s.t. $C\neq
C^{\prime}$. Therefore, $a\in\mathsf{GoodCol}^{\mathcal{J}}$. Now, from
$\mathsf{GoodCol}$ being also minimized and
$\mathsf{GoodCol}^{\mathcal{I}}=\\{a\\}$, we obtain
$\mathsf{GoodCol}^{\mathcal{J}}=\\{a\\}$. Overall $\mathcal{J}$ interprets the
minimized predicates as $\mathcal{I}$ does, hence the desired contradiction of
$\mathcal{J}<_{\sf CP}\mathcal{I}$.

“$\Leftarrow$”. Assume $\mathcal{C}\notin\text{Succinct}\text{-}\text{3COL}$.
Consider a model $\mathcal{I}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$. First
notice that $\mathsf{Center}^{\mathcal{I}}=\\{a\\}$. Indeed, $\mathcal{I}$
models $\mathcal{A}$ hence $a\in\mathsf{Center}^{\mathcal{I}}$, and, if there
were $b\in\mathsf{Center}^{\mathcal{I}}$ with $b\neq a$, then we could find a
model $\mathcal{J}$ of $\mathcal{K}$ with $\mathcal{J}<_{\sf CP}\mathcal{I}$
by:

  1. 1.

take $\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}}$ and preserve all
interpretations of fixed concept names;

  2. 2.

setting $\mathsf{Center}^{\mathcal{J}}=\\{a\\}$;

  3. 3.

replace every $(e,e^{\prime})\in r_{i}^{\mathcal{I}}$ by $(e,a)\in
r_{i}^{\mathcal{J}}$ and same for $\overline{r_{i}}$;

  4. 4.

define accordingly $\mathsf{AllPairs}^{\mathcal{J}}$;

  5. 5.

set for all $e\in\Delta^{\mathcal{J}}$: $e\in\mathsf{T}_{i}^{\mathcal{J}}$ iff
$a\in\mathsf{T}_{i}^{\mathcal{I}}$;

  6. 6.

set $t_{i}^{\mathcal{J}}=\\{(e,a)\mid e\in\mathsf{T}_{i}^{\mathcal{J}}\\}$ and
$\overline{t_{i}}^{\mathcal{J}}=\\{(e,a)\mid
e\notin\mathsf{T}_{i}^{\mathcal{J}}\\}$;

  7. 7.

define accordingly interpretations of concepts evaluating the circuit and
$\mathsf{Test}_{1}^{\mathcal{J}}$, $\mathsf{Test}_{2}^{\mathcal{J}}$;

  8. 8.

set $s_{C}^{\mathcal{J}}=\\{(e,a)\mid e\in((\mathsf{Test}_{1}\sqcap
C_{1})\sqcup(\mathsf{Test}_{2}\sqcap C_{2}))^{\mathcal{J}}\\}$;

  9. 9.

define accordingly $\mathsf{GoodCol}^{\mathcal{J}}$ and
$\mathsf{Goal}^{\mathcal{J}}$.

In particular, notice Step 1 removes $b$ from the interpretation of
$\mathsf{Center}$.

We now want to prove that if a pair $(v_{1},v_{2})$ is not represented in
$\mathcal{I}$, that is:

$\bigcap_{i\in\text{Ones}(v_{1},v_{2})}\mathsf{Bit}_{i}^{\mathcal{J}}\cap\bigcap_{i\in\text{Zeros}(v_{1},v_{2})}(\lnot\mathsf{Bit}_{i})^{\mathcal{J}}=\emptyset,$

where $\text{Ones}(v_{1},v_{2})$ is the set of $0\leq i\leq 2n-1$ s.t. the
$i^{\text{th}}$ bit in the binary encoding of $(v_{1},v_{2})$ is $1$ and
$\text{Zeros}(v_{1},v_{2})$ is its complement, then the query must be
satisfied. Indeed, if such a $(v_{1},v_{2})$ exists, then we must have
$\mathsf{AllPairs}^{\mathcal{J}}=\emptyset$, thus
$a\in\mathsf{Goal}^{\mathcal{J}}$, as otherwise we can obtain a model
$\mathcal{J}$ of $\mathcal{K}$ s.t. $\mathcal{J}<_{\sf CP}\mathcal{I}$ by:

  1. 1.

take $\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}}$ and preserve all
interpretations of fixed concept names and $\mathsf{Center}$;

  2. 2.

set $r_{i}^{\mathcal{J}}=\Delta^{\mathcal{I}}\times\\{a\\}$ if
$i\in\text{Ones}(v_{1},v_{2})$ and $r_{i}^{\mathcal{J}}=\emptyset$ otherwise;
set $\overline{r_{i}}^{\mathcal{J}}=\Delta^{\mathcal{I}}\times\\{a\\}$ if
$i\in\text{Zeros}(v_{1},v_{2})$ and $\overline{r_{i}}^{\mathcal{J}}=\emptyset$
otherwise;

  3. 3.

follow steps 3 to 8 from the previous construction of $\mathcal{J}$.

In particular, Step 2 of the above complies with Equation 97 as
$(v_{1},v_{2})$ is not represented in $\mathcal{I}$. It further implies that
$\mathsf{AllPairs}^{\mathcal{J}}=\emptyset$, which ensures the desired
contradiction $\mathcal{J}<_{\sf CP}\mathcal{I}$.

We are thus left with the case in which each possible pair $(v_{1},v_{2})$ is
represented at least once in $\mathcal{I}$. From Equations 100 and 101, we
know each element representing a pair assigns colors to its $v_{1}$ and
$v_{2}$. From Equations 102 to 108, these colors cannot be the same if there
is an edge $\\{v_{1},v_{2}\\}$ in the graph $\mathcal{G}_{\mathcal{C}}$. Thus,
since we assume $\mathcal{C}\notin\text{Succinct}\text{-}\text{3COL}$, the
overall choices of colors cannot be consistent: there must exist a vertex
$v_{0}$ which is assigned a color $C_{1}$ by an element $e_{1}$ representing a
pair $p_{1}$ and a different color $C_{2}$ by an element $e_{2}$ representing
a pair $p_{2}$. Let us assume $p_{1}$ has shape $(v_{0},v_{1})$ and $p_{2}$
has shape $(v_{0},v_{2})$ (other cases works similarly). We can now prove that
$\mathsf{GoodCol}^{\mathcal{I}}=\emptyset$, thus $a\in\mathsf{Goal}$, as
otherwise we could find a model $\mathcal{J}$ of $\mathcal{K}$ with
$\mathcal{J}<_{\sf CP}\mathcal{I}$ by:

  1. 1.

take $\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}}$ and preserve all
interpretations of fixed concept names, of $\mathsf{Center}$ and
$\mathsf{AllPairs}$, and of roles $r_{i}$ and $\overline{r_{i}}$;

  2. 2.

set for all $e\in\Delta^{\mathcal{J}}$: $e\in\mathsf{T}_{i}^{\mathcal{J}}$ iff
$i\in\text{Ones}(v_{0})$;

  3. 3.

set $t_{i}^{\mathcal{J}}=\\{(e,a)\mid e\in\mathsf{T}_{i}^{\mathcal{J}}\\}$ and
$\overline{t_{i}}^{\mathcal{J}}=\\{(e,a)\mid
e\notin\mathsf{T}_{i}^{\mathcal{J}}\\}$;

  4. 4.

define accordingly interpretations of concepts evaluating the circuit and
$\mathsf{Test}_{1}^{\mathcal{J}}$, $\mathsf{Test}_{2}^{\mathcal{J}}$;

  5. 5.

set $s_{C}^{\mathcal{J}}=\\{(e,a)\mid e\in((\mathsf{Test}_{1}\sqcap
C_{1})\sqcup(\mathsf{Test}_{2}\sqcap C_{2}))^{\mathcal{J}}\\}$;

  6. 6.

define accordingly $\mathsf{GoodCol}^{\mathcal{J}}$ and
$\mathsf{Goal}^{\mathcal{J}}$.

In particular, Equation 112 and Step 4 in the above ensure
$e_{1},e_{2}\in\mathsf{Test}_{1}^{\mathcal{J}}$. Therefore Step 5 above yields
$(e_{1},a)\in s_{C_{1}}^{\mathcal{J}}$ and $(e_{2},a)\in
s_{C_{2}}^{\mathcal{J}}$, which triggers Equation 117 in Step 6 and ensures
$\mathsf{GoodCol}^{\mathcal{J}}=\emptyset$. This yields the desired
contradiction $\mathcal{J}<_{\sf CP}\mathcal{I}$. Thus,
$\mathsf{GoodCol}^{\mathcal{I}}=\emptyset$, in particular Equation 118 yields
$a\in\mathsf{Goal}^{\mathcal{I}}$.

∎

We work towards a proof of Theorem 14. Assume given a model $\mathcal{I}$ of a
$\textrm{DL-Lite}_{\sf horn}^{\cal H}$ cKB ${\sf Circ_{\sf CP}}(\mathcal{K})$.
We “forget” about some parts of $\mathcal{I}$, only retaining which roles may
be needed due to a combination of fixed predicates in the forgotten part. To
this end, we define the fixed-type $\mathsf{ftp}_{\mathcal{I}}({e})$ of an
element $e\in\Delta^{\mathcal{I}}$ as the set of DL-Lite concepts $C$ such
that $\mathcal{T}\models(\bigsqcap_{e\in F^{\mathcal{I}},\
F\in\mathsf{F}}F)\sqsubseteq C$. Given a role $r\in\mathsf{N_{R}}^{\pm}$, we
say that $r$ is _forced_ in $\mathcal{I}$ if there exists an element
$f_{r}\in\Delta^{\mathcal{I}}$ such that $\exists
r\in\mathsf{ftp}_{\mathcal{I}}({f_{r}})$. For each forced role in
$\mathcal{I}$, we assume chosen such an element $f_{r}$. Similarly, for each
role $r\in\mathsf{N_{R}}^{\pm}$, we assume chosen an element $w_{r}\in(\exists
r^{-})^{\mathcal{I}}$ if $(\exists r^{-})^{\mathcal{I}}\neq\emptyset$. We now
construct an interpretation ${\mathcal{I}_{0}}$ whose domain
$\Delta^{\mathcal{I}_{0}}$ consists in ${\sf ind}(\mathcal{A})$, all chosen
$f_{r}$ and all chosen $w_{r}$. The interpretation $\mathcal{I}_{0}$ is now
defined as:

$\displaystyle{{A}}^{\mathcal{I}_{0}}=\;$
$\displaystyle{{A}}^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{0}}$
$\displaystyle{{r}}^{\mathcal{I}_{0}}=\;$
$\displaystyle{{r}}^{\mathcal{I}}\cap({\sf ind}(\mathcal{A})\times{\sf
ind}(\mathcal{A}))$ $\displaystyle\cup\\{(e,w_{s})\mid e\in(\exists
s)^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{0}},\mathcal{T}\models s\sqsubseteq
r\\}$ $\displaystyle\cup\\{(w_{s},e)\mid e\in(\exists
s)^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{0}},\mathcal{T}\models s\sqsubseteq
r^{-}\\}$

######  Remark 5.

Notice $\mathcal{I}_{0}$ is a special case of the models
$\mathcal{I}_{\mathcal{P}}$ considered in Section 4.1, and that
${\left|{\mathcal{I}_{0}}\right|}\leq{\left|{\mathcal{A}}\right|}+2{\left|{\mathcal{T}}\right|}$.

The key result is now the following:

######  Lemma 25.

Let $q$ be an AQ. If $\mathcal{I}$ is a countermodel for $q$ over ${\sf
Circ_{\sf CP}}(\mathcal{K})$, then so is $\mathcal{I}_{0}$.

###### Proof.

Assume $\mathcal{I}$ is a countermodel for $q$ over ${\sf Circ_{\sf
CP}}(\mathcal{K})$. Setting $\mathcal{P}=\\{f_{r}\mid r\text{ is forced in
}\mathcal{I}\\}$, we have $\mathcal{I}_{\mathcal{P}}=\mathcal{I}_{0}$ (see
Section 4.1) and thus Lemma 22 ensures $\mathcal{I}_{0}\models\mathcal{K}$.
Since concept interpretations in $\mathcal{I}_{0}$ are inherited from
$\mathcal{I}$, it is clear $\mathcal{I}_{0}$ does not entail $q$. It remains
to prove $\mathcal{I}_{0}$ also complies with ${\sf CP}$. By contradiction
assume there exists $\mathcal{J}_{0}$ a model of $\mathcal{K}$ with
$\mathcal{J}_{0}<_{\sf CP}\mathcal{I}_{0}$. Notice that, for each forced role
$r$ in $\mathcal{I}$, there must exists an element $w_{r}^{\prime}\in(\exists
r^{-})^{\mathcal{J}_{0}}$ as we kept element
$f_{r}\in\Delta^{\mathcal{I}_{0}}$ and $r$ is a consequence of the fixed
predicates on $f_{r}$ that must have been preserved in $\mathcal{J}_{0}$ (see
Condition 2 from the definition of $<_{\sf CP}$). We assume chosen such an
element $w_{r}^{\prime}$ per forced role and build an interpretation
$\mathcal{J}$:

$\displaystyle\Delta^{\mathcal{J}}=\;$ $\displaystyle\Delta^{\mathcal{I}}$
$\displaystyle{{A}}^{\mathcal{J}}=\;$
$\displaystyle{{A}}^{\mathcal{J}_{0}}\cup\\{e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{J}_{0}}\mid
A\in\mathsf{ftp}_{\mathcal{I}}({e})\\}$ $\displaystyle{{r}}^{\mathcal{J}}=\;$
$\displaystyle{{r}}^{\mathcal{J}_{0}}\cup\left\\{(e,w_{s}^{\prime})\;\middle|\begin{array}[]{l}e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{J}_{0}}\\\
\exists s\in\mathsf{ftp}_{\mathcal{I}}({e}),\mathcal{T}\models s\sqsubseteq
r\end{array}\right\\}$
$\displaystyle\phantom{{{r}}^{\mathcal{J}_{0}}}\cup\left\\{(w_{s}^{\prime},e)\;\middle|\begin{array}[]{l}e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{J}_{0}}\\\
\exists s\in\mathsf{ftp}_{\mathcal{I}}({e}),\mathcal{T}\models s\sqsubseteq
r^{-}\end{array}\right\\}$

It is easily verified that $\mathcal{J}$ is a model of $\mathcal{K}$, and we
now prove $\mathcal{J}<_{\sf CP}\mathcal{I}$, which will contradict
$\mathcal{I}\models{\sf Circ_{\sf CP}}(\mathcal{K})$. We first notice a useful
property: for all concept name $A$, we have
$A^{\mathcal{J}}\cap(\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{0}})\subseteq
A^{\mathcal{I}}\cap(\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{0}})$
($\star$). Indeed, if $e\in
A^{\mathcal{J}}\cap(\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{0}})$,
then $A\in\mathsf{ftp}_{\mathcal{I}}({e})$, and therefore $e\in
A^{\mathcal{I}}$. The converse does not hold in general. We now check that all
four conditions from the definition of $<_{\sf CP}$ are satisfied:

  1. 1.

By definition, we have $\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}}$.

  2. 2.

Let $A\in\mathsf{F}$. Definitions of $\mathcal{I}_{0}$ and $\mathcal{J}$
ensure $A^{\mathcal{I}}\cap{\Delta^{\mathcal{I}_{0}}}=A^{\mathcal{I}_{0}}$ and
$A^{\mathcal{J}}\cap{\Delta^{\mathcal{I}_{0}}}=A^{\mathcal{J}_{0}}$. From
$\mathcal{J}_{0}<_{\sf CP}\mathcal{I}_{0}$, we get
$A^{\mathcal{I}_{0}}=A^{\mathcal{J}_{0}}$, which yields
$A^{\mathcal{I}}\cap{\Delta^{\mathcal{I}_{0}}}=A^{\mathcal{J}}\cap{\Delta^{\mathcal{I}_{0}}}$.
For an element $e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{0}}$, we
remark: $e\in A^{\mathcal{I}}$ iff $A\in\mathsf{ftp}_{\mathcal{I}}({e})$ iff
$e\in A^{\mathcal{J}}$. Altogether, we obtain
$A^{\mathcal{I}}=A^{\mathcal{J}}$.

  3. 3.

Let $A\in\mathsf{M}$ such that $A^{\mathcal{J}}\not\subseteq A^{\mathcal{I}}$.
Let thus $e\in A^{\mathcal{J}}\setminus A^{\mathcal{I}}$. Notice $e$ must
belong to $\Delta^{\mathcal{I}_{0}}$, as otherwise $\star$ yields $e\in
A^{\mathcal{I}}$. It follows that $e\in A^{\mathcal{J}_{0}}\not\subseteq
A^{\mathcal{I}_{0}}$. Since $\mathcal{J}_{0}<_{\sf CP}\mathcal{I}_{0}$, there
exists $B\prec A$ s.t. $B^{\mathcal{J}_{0}}\subsetneq B^{\mathcal{I}_{0}}$. By
$\star$, this extends into $B^{\mathcal{J}}\subsetneq B^{\mathcal{I}}$ and we
found $B$ as desired.

  4. 4.

From $\mathcal{J}_{0}<_{\sf CP}\mathcal{I}_{0}$, there exists $A\in\mathsf{M}$
s.t. $A^{\mathcal{J}_{0}}\subsetneq A^{\mathcal{I}_{0}}$ and for all $B\prec
A$, $B^{\mathcal{J}_{0}}=B^{\mathcal{I}_{0}}$. Joint with $\star$, it follows
that $A^{\mathcal{J}}\subsetneq A^{\mathcal{I}}$ and for all $B\prec A$,
$B^{\mathcal{J}}\subseteq B^{\mathcal{I}}$. If ever there exists such a
$B\prec A$, such that additionally $B^{\mathcal{J}}\subsetneq
B^{\mathcal{I}}$, then we select a minimal such $B$ w.r.t. $\prec$, which
provides the desired minimized concept. Otherwise, $A$ fits.

It $\mathcal{J}<_{\sf CP}\mathcal{I}$, contradicting $\mathcal{I}\models{\sf
Circ_{\sf CP}}(\mathcal{K})$ as desired. ∎

See 14

###### Proof.

Guess a candidate interpretation $\mathcal{I}$ with size
${\left|{\mathcal{A}}\right|}+2{\left|{\mathcal{T}}\right|}$. Check whether it
is a model of $\mathcal{K}$ and if the AQ of interest is _not_ satisfied in
$\mathcal{I}$. Using a NP oracle, check whether $\mathcal{I}$ is a model of
${\sf Circ_{\sf CP}}(\mathcal{K})$. If all the above tests succeed, then
accept; otherwise, reject. From Lemma 25, it is immediate that there exists an
accepting run if there exists a countermodel for the AQ over ${\sf Circ_{\sf
CP}}(\mathcal{K})$. Conversely, if a run accepts, then the guessed model
$\mathcal{I}$ is a countermodel. ∎

See 11

###### Proof.

“$\Rightarrow$”. Assume ${\sf Circ_{\sf CP}}(\mathcal{K})\models A_{0}(a_{0})$
and let $\mathcal{I}^{\prime}$ be a model of ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})$.

We extend $\mathcal{I}^{\prime}$ into an interpretation $\mathcal{I}$ whose
domain is $\Delta^{\mathcal{I}}=\Delta^{\mathcal{I}^{\prime}}\uplus({\sf
ind}(\mathcal{A})\setminus{\sf ind}(\mathcal{A}^{\prime}))$. To define a
suitable interpretation of concepts on an individual $a$ from $\Delta={\sf
ind}(\mathcal{A})\setminus{\sf ind}(\mathcal{A}^{\prime})$, we consider its
ABox-type $t=\mathsf{tp}_{\mathcal{A}}({a})$. Notice
$m_{t}=4^{\left|{\mathcal{T}}\right|}$ as otherwise we would have $a\in{\sf
ind}(\mathcal{A}^{\prime})$. Consider now the types in $\mathcal{I}$ of
elements $a_{t,1},\dots a_{t,4^{\left|{\mathcal{T}}\right|}}$. Since there are
$4^{\left|{\mathcal{T}}\right|}$ such elements for only
$2^{{\left|{\mathcal{T}}\right|}}$ possible types, there exists a type
$t^{\prime}$ realized in $\mathcal{I}$ at least
$2^{\left|{\mathcal{T}}\right|}$ times. We now chose an element
$\mathsf{ref}(t)\in\Delta^{\mathcal{I}^{\prime}}$ s.t.
$\mathsf{tp}_{\mathcal{A}}({\mathsf{ref}(t)})=t$ and
$\mathsf{tp}_{\mathcal{I}^{\prime}}({\mathsf{ref}(t)})=t^{\prime}$. Such an
element $\mathsf{ref}(t)$ serves as a reference to interpret concepts and
roles on individuals $a\in\Delta$ with ABox type $t$, as the following
construction shows:

$\begin{array}[]{r@{\;}c@{\;}l}A^{\mathcal{I}}&=&A^{\mathcal{I}^{\prime}}\;\cup\;\\{a\mid
a\in\Delta,\mathsf{ref}(\mathsf{tp}_{\mathcal{A}}({a}))\in
A^{\mathcal{I}^{\prime}}\\}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
p^{\mathcal{I}}&=&p^{\mathcal{I}^{\prime}}\;\cup\;\\{(a,b)\mid\mathcal{K}\models
p(a,b)\\}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\ &&\cup\;\\{(a,e)\mid
a\in\Delta,(\mathsf{ref}(\mathsf{tp}_{\mathcal{A}}({a}),e)\in
p^{\mathcal{I}^{\prime}}\\}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
&&\cup\;\\{(e,a)\mid
a\in\Delta,(e,\mathsf{ref}(\mathsf{tp}_{\mathcal{A}}({a}))\in
p^{\mathcal{I}^{\prime}}\\}.\end{array}$

It is easily verified that $\mathcal{I}$ is a model of $\mathcal{K}$,
particularly that it satisfies all role assertions from $\mathcal{A}$. We now
prove $\mathcal{I}\models{\sf Circ_{\sf CP}}(\mathcal{K})$, which, by
hypothesis, gives $\mathcal{I}\models A_{0}(a_{0})$, and thus
$\mathcal{I}^{\prime}\models A_{0}(a_{0})$ by definition of
$A_{0}^{\mathcal{I}}$. Assume by contradiction one can find a model
$\mathcal{J}$ of $\mathcal{K}$ s.t. $\mathcal{J}<_{\sf CP}\mathcal{I}$. We
construct $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{I}^{\prime}$ which will
contradict $\mathcal{I}^{\prime}$ being a model of ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})$. Intuitively, we proceed as in Lemma 2 and
simulate $\mathcal{J}$ in $\mathcal{J}^{\prime}$. For each ABox type $t$ s.t.
there exists $a\in\Delta$ with $\mathsf{tp}_{\mathcal{A}}({a})=t$, we set:

$\displaystyle D_{t}=$
$\displaystyle\;\\{d\in\Delta^{\mathcal{I}^{\prime}}\mid\mathsf{tp}_{\mathcal{A}}({d})=t,\mathsf{tp}_{\mathcal{I}^{\prime}}({d})=\mathsf{tp}_{\mathcal{I}^{\prime}}({\mathsf{ref}(t)})\\}\vskip
3.0pt plus 1.0pt minus 1.0pt$ $\displaystyle S_{t}=$
$\displaystyle\;\\{\mathsf{tp}_{\mathcal{J}}({d})\mid\mathsf{tp}_{\mathcal{A}}({d})=t,\mathsf{tp}_{\mathcal{I}^{\prime}}({d})=\mathsf{tp}_{\mathcal{I}^{\prime}}({\mathsf{ref}(t)})\\}$

From the definition of $\mathsf{ref}(t)$, we have ${\left|{D_{t}}\right|}\geq
2^{\left|{\mathcal{T}}\right|}$, while, clearly, ${\left|{S_{t}}\right|}\leq
2^{\left|{\mathcal{T}}\right|}$. Since $S_{t}\neq\emptyset$ (it contains e.g.
$\mathsf{tp}_{\mathcal{J}}({\mathsf{ref}(t)})$), we can find a surjective
function $\pi_{t}:D_{t}\rightarrow S_{t}$. We consider $\pi$ the union of all
such $\pi_{t}$, that is with $t$ s.t. there exists $a\in\Delta$ with
$\mathsf{tp}_{\mathcal{A}}({a})=t$. We further extend the domain of definition
of $\pi$ to $\Delta^{\mathcal{I}^{\prime}}$ by setting
$\pi(d)=\mathsf{tp}_{\mathcal{J}}({d})$ for the remaining elements of
$\Delta^{\mathcal{I}^{\prime}}$. We now define the interpretation
$\mathcal{J}^{\prime}$ as:

$\begin{array}[]{r@{\;}c@{\;}l}\Delta^{\mathcal{J}^{\prime}}&=&\Delta^{\mathcal{I}^{\prime}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
A^{\mathcal{J}^{\prime}}&=&\\{d\in\Delta^{\mathcal{I}^{\prime}}\mid
A\in\pi(d)\\}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
{{r}}^{\mathcal{J}^{\prime}}&=&\\{(d,e)\in\Delta^{\mathcal{I}^{\prime}}\times\Delta^{\mathcal{I}^{\prime}}\mid\pi(d)\rightsquigarrow_{{r}}\pi(e)\\}.\end{array}$

It can now be verified that $\mathcal{J}^{\prime}$ is a model of
$\mathcal{K}^{\prime}$ such that $\mathcal{J}^{\prime}<_{\sf
CP}\mathcal{I}^{\prime}$.

“$\Leftarrow$”. Assume ${\sf Circ_{\sf CP}}(\mathcal{K}^{\prime})\models
A_{0}(a_{0})$ and let $\mathcal{I}$ be a model of ${\sf Circ_{\sf
CP}}(\mathcal{K})$. Here again, we denote $\Delta={\sf
ind}(\mathcal{A})\setminus{\sf ind}(\mathcal{A}^{\prime})$. By definition of
$W$, all elements from $\Delta$ have an ABox type $t$ that is already realized
at least $4^{\left|{\mathcal{T}}\right|}$ times in $W$. Therefore, we can
define a permutation $\sigma$ on $\Delta^{\mathcal{I}}$ such that for all
$d\in\Delta^{\mathcal{I}}$, the following conditions are respected:

  1. 1.

$\sigma(a_{0})=a_{0}$;

  2. 2.

$\mathsf{tp}_{\mathcal{A}}({\sigma(d)})=\mathsf{tp}_{\mathcal{A}}({d})$;

  3. 3.

If $d\in\Delta$, then there exists an element $\mathsf{ref}(d)\in W$ with
$\mathsf{tp}_{\mathcal{A}}({\mathsf{ref}(d)})=\mathsf{tp}_{\mathcal{A}}({d})$
and
$\mathsf{tp}_{\mathcal{I}}({\mathsf{ref}(d)})=\mathsf{tp}_{\mathcal{I}}({d})$.

We can then define an interpretation $\mathcal{I}_{\sigma}$ as follows:

$\begin{array}[]{r@{\;}c@{\;}l}\Delta^{\mathcal{I}_{\sigma}}&=&\Delta^{\mathcal{I}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
A^{\mathcal{I}_{\sigma}}&=&\sigma(A^{\mathcal{I}})\vskip 3.0pt plus 1.0pt
minus 1.0pt\\\ {{r}}^{\mathcal{I}_{\sigma}}&=&\\{(d,e)\mid\mathcal{K}\models
r(d,e)\\}\;\cup\;(\sigma\times\sigma)(r^{\mathcal{I}}).\end{array}$

It is straightforward that $\mathcal{I}_{\sigma}$ models $\mathcal{K}$
(notably relying on Condition 2), that preserves interpretation of concepts on
the individual $a_{0}$ of interest (from Condition 1). Additionally,
$\mathcal{I}_{\sigma}$ models ${\sf Circ_{\sf CP}}(\mathcal{K})$ as otherwise
a model $\mathcal{J}$ of $\mathcal{K}$ with $\mathcal{J}<_{\sf
CP}\mathcal{I}_{\sigma}$ immediately yields a model
$\mathcal{J}_{\sigma^{-1}}$ of $\mathcal{K}$ with
$\mathcal{J}_{\sigma^{-1}}<_{\sf CP}\mathcal{I}$, contradicting $\mathcal{I}$
being a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$.

We extend the mapping $\mathsf{ref}$ from Condition 3 to the identity for
elements from $\Delta^{\mathcal{I}}\setminus\Delta$, and define an
interpretation $\mathcal{I}^{\prime}$ as follows:

$\begin{array}[]{r@{\;}c@{\;}l}\Delta^{\mathcal{I}^{\prime}}&=&\Delta^{\mathcal{I}}\setminus\Delta\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
A^{\mathcal{I}^{\prime}}&=&A^{\mathcal{I}_{\sigma}}\cap\Delta^{\mathcal{I}^{\prime}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
{{r}}^{\mathcal{I}^{\prime}}&=&(\mathsf{ref}\times\mathsf{ref})(r^{\mathcal{I}_{\sigma}}\cap(\Delta^{\mathcal{I}^{\prime}}\times\Delta^{\mathcal{I}^{\prime}})).\end{array}$

It can be verified that $\mathcal{I}^{\prime}$ is a model of
$\mathcal{K}^{\prime}$. We now prove it is also a model of ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})$, which, by hypothesis, gives
$\mathcal{I}^{\prime}\models A_{0}(a_{0})$, and thus $\mathcal{I}\models
A_{0}(a_{0})$ as unfolding definitions gives $a_{0}\in A_{0}^{\mathcal{I}}$
iff $a_{0}\in A_{0}^{\mathcal{I}_{\sigma}}$ iff $a_{0}\in
A_{0}^{\mathcal{I}^{\prime}}$ (notably via Condition 1 on $\sigma$). Assume by
contradiction one can find a model $\mathcal{J}^{\prime}$ of
$\mathcal{K}^{\prime}$ with $\mathcal{J}^{\prime}<_{\sf
CP}\mathcal{I}^{\prime}$. We now construct $\mathcal{J}<_{\sf CP}\mathcal{I}$
which will contradict $\mathcal{I}$ being a model of ${\sf Circ_{\sf
CP}}(\mathcal{K})$. Relying on the mapping $\mathsf{ref}$, we set:

$\begin{array}[]{r@{\;}c@{\;}l}\Delta^{\mathcal{J}}&=&\Delta^{\mathcal{I}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
A^{\mathcal{J}}&=&\mathsf{ref}^{-1}(A^{\mathcal{J}^{\prime}})\vskip 3.0pt plus
1.0pt minus 1.0pt\\\ {{r}}^{\mathcal{J}}&=&\\{(d,e)\mid\mathcal{K}\models
r(d,e)\\}\;\cup\;(\mathsf{ref}^{-1}\times\mathsf{ref}^{-1})(r^{\mathcal{J}^{\prime}}).\end{array}$

It is easily checked that $\mathcal{J}$ models $\mathcal{K}$. From Condition 3
on $\sigma$, it then follows $\mathcal{J}<_{\sf CP}\mathcal{I}$, ie the
desired contradiction. ∎

##  Appendix H Proofs for Section 5.3

See 16

###### Proof.

We give a polynomial time reduction from $\forall\exists{\sf 3SAT}$, c.f. the
proof of Theorem 4. Let a $\forall\exists$-3CNF sentence
$\forall\bar{x}\exists\bar{y}\,\varphi$ be given where $\bar{x}=x_{1}\cdots
x_{m}$, $\bar{y}=y_{1}\cdots y_{n}$, and
$\varphi=\bigwedge^{\ell}_{i=1}\bigvee_{j=1}^{3}L_{ij}$ with $L_{ij}=v$ or
$L_{ij}=\lnot{v}$ for some $v\in\\{x_{1},\dots x_{m},y_{1},\dots,y_{n}\\}$. We
construct a circumscribed $\textrm{DL-Lite}_{\sf core}^{\cal H}$ KB ${\sf
Circ_{\sf CP}}(\mathcal{K})$ and an atomic query $q$ such that ${\sf Circ_{\sf
CP}}(\mathcal{K})\models q$ iff $\forall\bar{x}\exists\bar{y}\,\varphi$ is
true.

The circumscription pattern ${\sf CP}$ involves four minimized concept names
with the preference

${\mathsf{VVal}}\prec{\mathsf{XVal}}\prec{\mathsf{CVal}}\prec{\mathsf{FVal}},$

and no fixed concept names. We now describe the construction of the KB
$\mathcal{K}=(\mathcal{T},\mathcal{A})$, not strictly separating $\mathcal{T}$
from $\mathcal{A}$. We first introduce an ABox individual for each variable,
marking the existential variables with the concept name ${\mathsf{XVar}}$ and
the universal ones with ${\mathsf{YVar}}$:

$\displaystyle{\mathsf{XVar}}({x})$ $\displaystyle\quad\text{for all
}x\in\bar{x}$ (119) $\displaystyle{\mathsf{YVar}}({y})$
$\displaystyle\quad\text{for all }y\in\bar{y}.$ (120)

To choose truth values for variables, we use the minimized concept name
${\mathsf{VVal}}$. We introduce two instances of ${\mathsf{VVal}}$ for each
variable, one representing true and the other false:

$\displaystyle{\mathsf{VVal}}(t_{v})$ $\displaystyle\quad\text{for all
}v\in\bar{x}\cup\bar{y}$ (121) $\displaystyle{\mathsf{VVal}}(f_{v})$
$\displaystyle\quad\text{for all }v\in\bar{x}\cup\bar{y}.$ (122)

Each variable must choose an instance of ${\mathsf{VVal}}$ via the role names
${\mathsf{eval}}_{{\mathsf{X}}}$ an ${\mathsf{eval}}_{{\mathsf{Y}}}$,
depending on whether it is existential or universal:

$\displaystyle{\mathsf{XVar}}$
$\displaystyle\sqsubseteq\,\exists{\mathsf{eval}}_{{\mathsf{X}}}$ (123)
$\displaystyle{\mathsf{YVar}}$
$\displaystyle\sqsubseteq\,\exists{\mathsf{eval}}_{{\mathsf{Y}}}$ (124)
$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{X}}}}^{-}$
$\displaystyle\sqsubseteq\,{\mathsf{VVal}}$ (125)
$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{Y}}}}^{-}$
$\displaystyle\sqsubseteq\,{\mathsf{VVal}}.$ (126)

There is no guarantee yet, however, that a variable $v$ chooses one of the
instances $t_{v}$ and $f_{v}$ of ${\mathsf{VVal}}$ reserved for it. To ensure
this, we first install the following role inclusions:

$\displaystyle{\mathsf{eval}}_{{\mathsf{X}}}$
$\displaystyle\sqsubseteq\,{\mathsf{eval}}$ (127)
$\displaystyle{\mathsf{eval}}_{{\mathsf{Y}}}$
$\displaystyle\sqsubseteq\,{\mathsf{eval}}$ (128)
$\displaystyle{\mathsf{eval}}$
$\displaystyle\sqsubseteq\,\lnot\overline{{\mathsf{eval}}}.$ (129)

The negative role inclusion allows us to flexibly control the targets for the
existential restrictions in CIs (123) and (124), as follows:

$\displaystyle\overline{{\mathsf{eval}}}(v,t_{v^{\prime}})$
$\displaystyle\quad\text{for all }v,v^{\prime}\in\bar{x}\cup\bar{y}\text{ with
}v\neq v^{\prime}$ (130)
$\displaystyle\overline{{\mathsf{eval}}}(v,f_{v^{\prime}})$
$\displaystyle\quad\text{for all }v,v^{\prime}\in\bar{x}\cup\bar{y}\text{ with
}v\neq v^{\prime}.$ (131)

To force the truth values of the variables in $\bar{x}$ to be identical in all
models that are smaller w.r.t. ‘$<_{\sf CP}$,’ we mark those truth values with
the minimized concept name ${\mathsf{XVal}}$:

$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{X}}}}^{-}$
$\displaystyle\sqsubseteq\,{\mathsf{XVal}}.$ (132)

We next introduce an individual for each clause:

$\displaystyle{\mathsf{Clause}}(c_{i})$ $\displaystyle\quad\text{for }1\leq
i\leq\ell.$ (133)

We also assign a truth value to every clause via the role name
${\mathsf{eval}}_{{\mathsf{C}}}$, another subrole of ${\mathsf{eval}}$. Every
element with an incoming ${\mathsf{eval}}_{{\mathsf{C}}}$-edge must make the
concept name ${\mathsf{CVal}}$ true, which is minimized, but with lower
priority than ${\mathsf{VVal}}$ and ${\mathsf{XVal}}$. This reflects the fact
that the truth values of variables determine the truth values of clauses. We
put:

$\displaystyle{\mathsf{Clause}}$
$\displaystyle\sqsubseteq\,\exists{\mathsf{eval}}_{{\mathsf{C}}}$ (134)
$\displaystyle{\mathsf{eval}}_{{\mathsf{C}}}$
$\displaystyle\sqsubseteq\,{\mathsf{eval}}$ (135)
$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{C}}}}^{-}$
$\displaystyle\sqsubseteq\,{\mathsf{CVal}}$ (136)

The truth values of clauses are represented by the same individuals as the
truth values of variables:

$\displaystyle{\mathsf{CVal}}(t_{v})$ $\displaystyle\quad\text{for all
}v\in\bar{x}\cup\bar{y}$ (137) $\displaystyle{\mathsf{CVal}}(f_{v})$
$\displaystyle\quad\text{for all }v\in\bar{x}\cup\bar{y}$ (138)

We again use the role $\overline{{\mathsf{eval}}}$ to control which instance
of ${\mathsf{Clause}}$ can be used as truth values for which clause. This is
based on the literals that occur in the clause. If a variable $v$ occurs
positively in the $i^{th}$ clause, then $c_{i}$ has access to $f_{v}$, while
if $v$ occurs negatively, then $c_{i}$ has access to $t_{v}$. And those are
the only instances of ${\mathsf{VVal}}$ to which $c_{i}$ has access: for
$1\leq i\leq\ell$ and all $v\in\bar{x}\cup\bar{y}$, put

$\displaystyle\overline{{\mathsf{eval}}}(c_{i},t_{v})$
$\displaystyle\quad\text{if }\lnot v\notin\\{L_{i,1},L_{i,2},L_{i,3}\\}$ (139)
$\displaystyle\overline{{\mathsf{eval}}}(c_{i},f_{v})$
$\displaystyle\quad\text{if }v\notin\\{L_{i,1},L_{i,2},L_{i,3}\\}.$ (140)

Note that clause individual $c_{i}$ has access via
${\mathsf{eval}}_{{\mathsf{C}}}$ to $t_{v}$ if making $v$ _false_ leads to
satisfaction of the $i^{th}$ clause, and likewise for $f_{v}$ and making $v$
_true_. Moreover, $v$ being made true is represented by an
${\mathsf{eval}}_{{\mathsf{X}}}$\- or ${\mathsf{eval}}_{{\mathsf{Y}}}$-edge
from $v$ to $t_{v}$ and likewise for $v$ being made false and $f_{v}$. Also
recall that $t_{v}$ and $f_{v}$ cannot have such incoming edges from
elsewhere. Consequently, the $i^{th}$ clause evaluates to true if we can find
a target for the ${\mathsf{eval}}_{{\mathsf{C}}}$-edge that does _not_ have an
incoming ${\mathsf{eval}}_{{\mathsf{X}}}$\- or
${\mathsf{eval}}_{{\mathsf{Y}}}$-edge:

$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{X}}}}^{-}$
$\displaystyle\sqsubseteq\,\lnot\exists{{\mathsf{eval}}_{{\mathsf{C}}}}^{-}$
(141) $\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{Y}}}}^{-}$
$\displaystyle\sqsubseteq\,\lnot\exists{{\mathsf{eval}}_{{\mathsf{C}}}}^{-}.$
(142)

In the case that a clause evaluates to false, it cannot reuse one of the
admitted instances of ${\mathsf{CVal}}$. We introduce an extra instance $f$ of
${\mathsf{CVal}}$ that can be used instead:

$\displaystyle{\mathsf{CVal}}(f).$ (143)

To ensure that $f$ is indeed used as an
${\mathsf{eval}}_{{\mathsf{C}}}$-target only if at least one clause is
falsified, we use the fourth minimized concept name ${\mathsf{FVal}}$. Note
that it is minimized with the least priority. We make sure that $f$ must have
an outgoing ${\mathsf{eval}}_{{\mathsf{F}}}$-edge leading to an instance of
${\mathsf{FVal}}$, that $f$ itself is an instance of ${\mathsf{FVal}}$, and
that having an incoming ${\mathsf{eval}}_{{\mathsf{F}}}$-edge precludes having
an incoming ${\mathsf{eval}}_{{\mathsf{C}}}$-edge. If all clauses evaluate to
true, then there is no need to use $f$ as a target for
${\mathsf{eval}}_{{\mathsf{C}}}$ and $f$ can use itself as the
${\mathsf{eval}}_{{\mathsf{F}}}$-target. But if a clause evaluates to false,
then we must use $f$ as a last resort ${\mathsf{eval}}_{{\mathsf{C}}}$-target
and cannot use it as an ${\mathsf{eval}}_{{\mathsf{F}}}$-target. Since
${\mathsf{FVal}}$ is minimized with least priority, the latter will simply
lead to a fresh instance of ${\mathsf{eval}}_{{\mathsf{F}}}$ to be created. In
summary, all clauses evaluate to true if and only of $f$ has an incoming
${\mathsf{eval}}_{{\mathsf{F}}}$-edge. We put:

$\displaystyle{\mathsf{Formula}}(f)$ $\displaystyle\qquad{\mathsf{FVal}}(f)$
(144) $\displaystyle{\mathsf{Formula}}$
$\displaystyle\sqsubseteq\,\exists{\mathsf{eval}}_{{\mathsf{F}}}$ (145)
$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{F}}}}^{-}$
$\displaystyle\sqsubseteq\,{\mathsf{FVal}}$ (146)
$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{C}}}}^{-}$
$\displaystyle\sqsubseteq\,\lnot\exists{{\mathsf{eval}}_{{\mathsf{F}}}}^{-}.$
(147)

By what was said above, to finish the reduction, it suffices to add

$\displaystyle\exists{{\mathsf{eval}}_{{\mathsf{F}}}}^{-}$
$\displaystyle\sqsubseteq\,{\mathsf{Goal}}.$ (148)

to choose as the query $q={\mathsf{Goal}}(x)$, and to ask whether $f$ is an
answer.

To prove correctness, we thus have to show the following.
Claim. ${\sf Circ_{\sf CP}}(\mathcal{K})\models q(f)$ iff
$\forall\bar{x}\exists\bar{y}\,\varphi$ is true.
To prepare for the proof of the claim, we first observe that every valuation
$V$ for $\bar{x}\cup\bar{y}$ gives rise to a corresponding model
$\mathcal{I}_{V}$ of $\mathcal{K}$. We use domain

$\Delta^{\mathcal{I}_{V}}={\sf ind}(\mathcal{A})$

and set

$A^{\mathcal{I}_{V}}=\\{a\mid A(a)\in\mathcal{A}\\}$

for all concept names

$A\in\\{{\mathsf{XVar}},{\mathsf{YVar}},{\mathsf{VVal}},{\mathsf{CVal}},{\mathsf{Clause}},{\mathsf{Formula}}\\}.$

We interpret ${\mathsf{eval}}_{{\mathsf{X}}}$ and
${\mathsf{eval}}_{{\mathsf{Y}}}$ according to $V$, that is

$\begin{array}[]{rcl}{\mathsf{eval}}_{{\mathsf{X}}}^{\mathcal{I}_{V}}&=&\\{(x,t_{v})\mid
x\in\bar{x}\text{ and }V(x)=1\\}\,\cup\\\\[2.84526pt] &&\\{(x,f_{v})\mid
x\in\bar{x}\text{ and }V(x)=0\\}\end{array}$

and analogously for ${\mathsf{eval}}_{{\mathsf{Y}}}$. Next we put

${\mathsf{XVal}}^{\mathcal{I}_{V}}=\\{e\mid(e,d)\in{\mathsf{eval}}_{{\mathsf{X}}}^{\mathcal{I}_{V}}\\}.$

If $V$ makes the $i^{th}$ clause true, then there is a literal in it that is
true. Choose such a literal $L$ and set $w_{i}=t_{v}$ if $L=\neg v$ an
$w_{i}=f_{v}$ if $L=v$. If $V$ makes the $i^{th}$ clause false, then set
$w_{i}=f$. We proceed with the definition of $\mathcal{I}_{V}$:

$\begin{array}[]{rcl}{\mathsf{eval}}_{{\mathsf{C}}}^{\mathcal{I}_{V}}&=&\\{(c_{i},w_{i})\mid
1\leq i\leq\ell\\}\\\\[2.84526pt]
{\mathsf{eval}}^{\mathcal{I}_{V}}&=&{\mathsf{eval}}_{{\mathsf{X}}}^{\mathcal{I}_{V}}\cup{\mathsf{eval}}_{{\mathsf{Y}}}^{\mathcal{I}_{V}}\cup{\mathsf{eval}}_{{\mathsf{C}}}^{\mathcal{I}_{V}}\\\\[2.84526pt]
\overline{{\mathsf{eval}}}^{\mathcal{I}_{V}}&=&\\{(a,b)\mid\overline{{\mathsf{eval}}}(a,b)\in\mathcal{A}\\}\\\\[2.84526pt]
{\mathsf{FVal}}^{\mathcal{I}_{V}}&=&\\{f,c_{1}\\}\\\\[2.84526pt]
{\mathsf{eval}}_{{\mathsf{F}}}^{\mathcal{I}_{V}}&=&\\{(f,c_{1}0)\\}\\\\[2.84526pt]
{\mathsf{Goal}}^{\mathcal{I}_{V}}&=&\\{c_{1}\\}.\end{array}$

The choice of $c_{1}$ is somewhat arbitrary in the last three statements, any
other individual without an incoming ${\mathsf{eval}}_{{\mathsf{C}}}$-edge
would also do. It is straightforward to verify that $\mathcal{I}_{V}$ is a
model of $\mathcal{K}$ with $\mathcal{I}_{V}\not\models q(f)$.

We can define a variation $\mathcal{I}^{\prime}_{V}$ of $\mathcal{I}_{V}$ that
is still a model of $\mathcal{K}$ provided that all clauses are satisfied by
$V$ (which guarantees that $f$ has no incoming
${\mathsf{eval}}_{{\mathsf{C}}}$-edge), and that satisfies
$\mathcal{I}^{\prime}_{V}\models q(f)$. To achieve this, we replace the last
three lines from the definition of $\mathcal{I}_{V}$ with

$\begin{array}[]{rcl}{\mathsf{FVal}}^{\mathcal{I}_{V}}&=&\\{f\\}\\\\[2.84526pt]
{\mathsf{eval}}_{{\mathsf{F}}}^{\mathcal{I}_{V}}&=&\\{(f,f)\\}\\\\[2.84526pt]
{\mathsf{Goal}}^{\mathcal{I}_{V}}&=&\\{f\\}.\end{array}$

Now for the actual proof of the claim

“$\Rightarrow$”. Assume that $\forall\bar{x}\exists\bar{y}\,\varphi$ is false,
and thus $\exists\bar{x}\forall\bar{y}\,\lnot\varphi$ is true and there is a
valuation $V_{\bar{x}}:\bar{x}\rightarrow\\{0,1\\}$ such that
$\forall\bar{y}\,\lnot\varphi^{\prime}$ holds where $\varphi^{\prime}$ is
obtained from $\varphi$ by replacing every variable $x\in\bar{x}$ with the
truth constant $V_{\bar{x}}(x)$. Consider any extension $V$ of $V_{\bar{x}}$
to the variables in $\bar{y}$ and the interpretation $\mathcal{I}_{V}$. Since
$\mathcal{I}_{V}$ is a model of $\mathcal{K}$ with $\mathcal{I}_{V}\not\models
q(f)$, to show that ${\sf Circ_{\sf CP}}(\mathcal{K})\not\models q(f)$ it
remains to prove that there is no model $\mathcal{J}<_{\sf CP}\mathcal{I}$ of
$\mathcal{K}$.

Assume to the contrary that there is such a $\mathcal{J}$. We first observe
that $A^{\mathcal{J}}=A^{\mathcal{I}_{V}}$ for all
$A\in\\{{\mathsf{VVal}},{\mathsf{XVal}},{\mathsf{CVal}}\\}$. This holds for
${\mathsf{VVal}}$ since
${\mathsf{VVal}}^{\mathcal{J}}\subsetneq{\mathsf{VVal}}^{\mathcal{I}_{V}}$
means that $\mathcal{J}$ does not satisfy $\mathcal{A}$, and likewise for
${\mathsf{CVal}}$. It also holds for ${\mathsf{XVal}}$ since every model of
$\mathcal{K}$ must make ${\mathsf{XVal}}$ true at at least one of $t_{x}$ and
$f_{x}$ for all $x\in\bar{x}$. This is because of CIs (123), (125), (127), and
(132), the role disjointness (129), the assertions (130) and (131), and the
fact that minimization of ${\mathsf{VVal}}$ is preferred over minimization of
${\mathsf{XVal}}$. But no subset of ${\mathsf{XVal}}^{\mathcal{I}_{V}}$
satisfies this condition, so we must have
${\mathsf{XVal}}^{\mathcal{I}_{V}}\subseteq{\mathsf{XVal}}^{\mathcal{J}}$,
consequently
${\mathsf{XVal}}^{\mathcal{J}}={\mathsf{XVal}}^{\mathcal{I}_{V}}$.

The above and $\mathcal{J}<_{\sf CP}\mathcal{I}$ means that
${\mathsf{FVal}}^{\mathcal{J}}\subsetneq{\mathsf{FVal}}^{\mathcal{I}_{V}}$.
Since $\mathcal{J}$ is a model of $\mathcal{K}$, this implies
${\mathsf{FVal}}^{\mathcal{J}}=\\{f\\}$.

Since ${\mathsf{XVal}}^{\mathcal{J}}={\mathsf{XVal}}^{\mathcal{I}_{V}}$ and
$\mathcal{J}$ is a model of $\mathcal{K}$, $V(x)=1$ implies
$(x,t_{x})\in{\mathsf{eval}}^{\mathcal{J}}$ and $V(x)=0$ implies
$(x,f_{x})\in{\mathsf{eval}}^{\mathcal{J}}$. Moreover, since
${\mathsf{VVal}}^{\mathcal{J}}={\mathsf{VVal}}^{\mathcal{I}_{V}}$ and
$\mathcal{J}$ is a model of $\mathcal{K}$, for every $y\in\bar{y}$ we have
$(y,t_{y})\in{\mathsf{eval}}^{\mathcal{J}}$ or
$(y,f_{y})\in{\mathsf{eval}}^{\mathcal{J}}$. We thus find an extension
$V^{\prime}$ of $V_{\bar{x}}$ to $\bar{x}\cup\bar{y}$ that is _compatible
with_ $\mathcal{J}$ in the sense that for all $v\in\bar{x}\cup\bar{y}$,

  * •

$V^{\prime}(v)=1$ implies $(v,t_{v})\in{\mathsf{eval}}^{\mathcal{J}}$ and

  * •

$V^{\prime}(v)=0$ implies $(v,f_{v})\in{\mathsf{eval}}^{\mathcal{J}}$.

Choose some such $V^{\prime}$. Since $\forall\bar{y}\,\lnot\varphi^{\prime}$
holds, at least one of the clauses must be made false by $V^{\prime}$. As
explained alongside the construction of $\mathcal{K}$, that clause can only
have an ${\mathsf{eval}}_{{\mathsf{C}}}$-edge to $f$. By (147), the outgoing
${\mathsf{eval}}_{{\mathsf{F}}}$-edge from $f$ cannot end at $f$. But
${\mathsf{FVal}}^{\mathcal{J}}=\\{f\\}$ and thus (134) implies that $f$ is the
only point where that edge may end. We have arrived at a contradiction.

“$\Leftarrow$”. Assume that
$\forall\bar{x}\exists\bar{y}\,\varphi(\bar{x},\bar{y})$ is true and let
$\mathcal{I}$ be a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$. We have to
show that $\mathcal{I}\models q(f)$. To this end, we first observe that

${\mathsf{VVal}}^{\mathcal{I}}=\\{a\mid{\mathsf{VVal}}(a)\in\mathcal{A}\\}.$
($*$)

If this is not the case, in fact, then we find a model $\mathcal{J}<_{\sf
CP}\mathcal{I}$ of $\mathcal{K}$, contradicting the minimality of
$\mathcal{J}$. This model $\mathcal{J}$ is essentially $\mathcal{I}_{V}$,
except that we might have to extend the domain with additional elements that
do not occur in the extension of any concept or role name to make sure that
the domains of $\mathcal{I}$ and $\mathcal{I}_{V}$ are identical.

It follows from ($*$) and the fact that $\mathcal{I}$ is a model of
$\mathcal{K}$ that for every $x\in\bar{x}$, we have
$(x,t_{x})\in{\mathsf{eval}}^{\mathcal{J}}$ or
$(x,f_{x})\in{\mathsf{eval}}^{\mathcal{J}}$. Consequently, we find a valuation
$V_{\bar{x}}$ for $\bar{x}$ that is compatible with $\mathcal{I}$ as defined
in the “$\Rightarrow$” direction of the proof. Since
$\forall\bar{x}\exists\bar{y}\,\varphi(\bar{x},\bar{y})$ is true, we can
extend $V_{\bar{x}}$ to a valuation $V$ for $\bar{x}\cup\bar{y}$ that
satisfies $\varphi$. Consider the model $\mathcal{I}^{\prime}_{V}$, extended
to domain $\Delta^{\mathcal{I}}$. By construction of
$\mathcal{I}^{\prime}_{V}$ and ($*$), we have
${\mathsf{VVal}}^{\mathcal{I}}={\mathsf{VVal}}^{\mathcal{I}^{\prime}_{V}}$.
Using the facts that $\mathcal{I}$ is a minimal model of $\mathcal{K}$ and the
construction of $\mathcal{I}^{\prime}_{V}$, it can now be observed that
${\mathsf{XVal}}^{\mathcal{I}}={\mathsf{XVal}}^{\mathcal{I}^{\prime}_{V}}$.
Moreover, by construction, $\mathcal{I}^{\prime}_{V}$ interprets
${\mathsf{CVal}}$ and ${\mathsf{FVal}}$ in the minimal possible way among all
models of $\mathcal{K}$. Since $\mathcal{I}$ is a minimal model, this implies
${\mathsf{CVal}}^{\mathcal{I}}={\mathsf{CVal}}^{\mathcal{I}^{\prime}_{V}}$ and
${\mathsf{FVal}}^{\mathcal{I}}={\mathsf{FVal}}^{\mathcal{I}^{\prime}_{V}}$. In
particular, ${\mathsf{FVal}}^{\mathcal{I}}=\\{f\\}$. But this implies
$(f,f)\in{\mathsf{eval}}_{{\mathsf{F}}}^{\mathcal{I}}$ as all objects with an
incoming ${\mathsf{eval}}_{{\mathsf{F}}}$-edge must satisfy ${\mathsf{FVal}}$.
It follows that $f\in{\mathsf{Goal}}^{\mathcal{I}}$ and thus
$\mathcal{I}\models q(f)$, as desired. ∎