ind}(\mathcal{A})$; otherwise, it should be ‘dormant’. The individual names in
${\sf ind}(\mathcal{A})$, in contrast, should always be active. To achieve
this, we include in $\mathcal{A}^{\prime}$ the following assertions where $X$
is a fresh concept name indicating activeness and $u$ is a fresh role name:

$\displaystyle X(a)$ $\displaystyle\quad\text{for all }a\in{\sf
ind}(\mathcal{A}),$ (6) $\displaystyle u(x,a)$ $\displaystyle\quad\text{for
all }a\in{\sf Ind}(\mathcal{A})\text{ and }x\in{\sf var}(q)$ (7)

We then define the CQ $q^{\prime}$ to be

$q^{\prime}=q\wedge\bigwedge_{x\in{\sf var}(q)}X(x),$

and add to $\mathcal{T}^{\prime}$:

$\displaystyle\exists u.L\sqsubseteq X.$ (8)

Elements generated by existential quantifiers on the right-hand side of CIs in
$\mathcal{T}$ should of course also be active. Moreover, dormant elements
should not trigger CIs from $\mathcal{T}$ as this might generate ‘unjustified’
existential (thus active) elements. We deal with these issues by including in
$\mathcal{T}^{\prime}$ the following relativized version of $\mathcal{T}$
(recall $\mathcal{T}$ is in normal form):

$\displaystyle X\sqsubseteq A$ $\displaystyle\quad\text{for all
}\top\sqsubseteq A\in\mathcal{T}$ (9) $\displaystyle X\sqcap
A\sqsubseteq\exists r.(X\sqcap B)$ $\displaystyle\quad\text{for all
}A\sqsubseteq\exists r.B\in\mathcal{T}$ (10) $\displaystyle X\sqcap\exists
r.(X\sqcap B)\sqsubseteq A$ $\displaystyle\quad\text{for all }\exists
r.B\sqsubseteq A\in\mathcal{T}$ (11) $\displaystyle X\sqcap A_{1}\sqcap
A_{2}\sqsubseteq A$ $\displaystyle\quad\text{for all }A_{1}\sqcap
A_{2}\sqsubseteq A\in\mathcal{T}$ (12)

Note that, when activating the copy of $q$ in $\mathcal{A}^{\prime}$ by making
$X$ true at all its individual names, then the CIs (9)–(12) apply also there
and may make concept names $A$ with $A\in\Sigma$ true at elements $x\in{\sf
var}(q)$. Because of (1), this may lead to models in which the copy of $q$ is
activated to be incomparable to models in which it is not activated regarding
$<_{\sf CP}$. This can be remedied by adding to $\mathcal{A}^{\prime}$:

$\displaystyle M(x)$ $\displaystyle\quad\text{ for all }x\in{\sf var}(q).$
(13)

The second case of non-asserted instances $d$ of closed concept names is that
$d$ is not from ${\sf ind}(\mathcal{A})\cup{\sf var}(q)$. The idea is that
models with such instances $d$ should be non-minimal. We achieve this by
including in $\mathcal{A}^{\prime}$ a fresh individual $t$ that must satisfy
$M$, but not necessarily anything else. Since any existential instance $d$ of
a closed concept name must also satisfy $M$, we can find a model that is
preferred w.r.t. $<_{\sf CP}$ by using $t$ as a surrogate for $d$, that is,
making true at $t$ exactly the concept names true at $d$, rerouting all
incoming and outgoing role edges from $d$ to $t$, and then removing $d$ from
the extension of all concept and role names. We thus include in
$\mathcal{A}^{\prime}$:

$\displaystyle M(t).$ (14)

The third and last case of non-asserted instances $d$ of closed concept names
is that $d$ is $t$ or an individual in the copy of $q$ in
$\mathcal{A}^{\prime}$. Since these individuals satisfy $M$, we may make true
at them a closed concept name without producing a non-minimal model. To fix
this problem, it suffices to prevent the individuals in ${\sf
var}(q)\cup\\{t\\}$ to be used as witnesses for existential restrictions in
$\mathcal{T}$, as this is the only possible reason for creating non-asserted
instances of closed concept names of the described form. It is, however, easy
to identify such witnesses as they must be active and satisfy the concept name
$X$. We thus add

$\displaystyle\overline{}X(a)$ $\displaystyle\quad\text{for all }a\in{\sf
var}(q)\cup\\{t\\}$ (15) $\displaystyle u(x,a)$ $\displaystyle\quad\text{for
all }a\in{\sf var}(q)\cup\\{t\\}\text{ and }x\in{\sf var}(q)$ (16)
$\displaystyle X\sqcap\overline{}X\sqsubseteq L.$ (17)

where $\overline{X}$ is a fresh concept name. This finishes the construction
of $\mathcal{T}^{\prime}$ and $\mathcal{A}^{\prime}$.
Claim. $\mathcal{K}_{\Sigma}\models q$ iff ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})\models q^{\prime}$.

“$\Leftarrow$”. Let $\mathcal{K}_{\Sigma}\not\models q$. Then, there is a
model $\mathcal{I}$ of $\mathcal{K}_{\Sigma}$ such that
$\mathcal{I}\not\models q$. W.l.o.g. assume that
$\Delta^{\mathcal{I}}\cap({\sf var}(q)\cup\\{t\\})=\emptyset$. We construct an
interpretation $\mathcal{J}$ as follows:

$\displaystyle\Delta^{\mathcal{J}}$
$\displaystyle\coloneqq\Delta^{\mathcal{I}}\cup{\sf var}(q)\cup\\{t\\}$
$\displaystyle A^{\mathcal{J}}$ $\displaystyle\coloneqq
A^{\mathcal{I}}\cup\\{x\mid A(x)\in\mathcal{A}^{\prime}\\}$ $\displaystyle
r^{\mathcal{J}}$ $\displaystyle\coloneqq r^{\mathcal{I}}\cup\\{(x,y)\mid
r(x,y)\in\mathcal{A}^{\prime}\\}$ $\displaystyle X^{\mathcal{J}}$
$\displaystyle\coloneqq\Delta^{\mathcal{I}}$ $\displaystyle M^{\mathcal{J}}$
$\displaystyle\coloneqq\bigcup_{A\in\Sigma}A^{\mathcal{J}}\cup{\sf
var}(q)\cup\\{t\\}$

for all concept names $A\notin\\{X,M\\}$ and role names $r$. From
$\mathcal{I}\models\mathcal{K}$ and the construction of $X^{\mathcal{J}}$, it
easily follows that $\mathcal{J}\models\mathcal{K}^{\prime}$. To show
$\mathcal{J}\models{\sf Circ_{\sf CP}}(\mathcal{K}^{\prime})$, we are left to
prove that $\mathcal{J}$ is minimal.

Assume to the contrary that there is a model $\mathcal{J}^{\prime}$ of
$\mathcal{K}^{\prime}$ with $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{J}$. As
$M$ is the only minimized concept name, there must be some $a\in
M^{\mathcal{J}}$ with $a\notin M^{\mathcal{J}^{\prime}}$. We must have
$a\notin{\sf var}(q)\cup\\{t\\}$ since $M(x)\in\mathcal{A}^{\prime}$ for
$x\in{\sf var}(q)\cup\\{t\\}$ and $\mathcal{J}^{\prime}$ is a model of
$\mathcal{K}^{\prime}$. But then, the definition of $M^{\mathcal{J}}$ implies
$a\in A^{\mathcal{J}}$ with $A\in\Sigma$. By definition of $A^{\mathcal{J}}$,
in turn, $a\in A^{\mathcal{I}}$ or $A(a)\in\mathcal{A}^{\prime}$. In the
former case, it follows from the fact that $\mathcal{I}$ respects $\Sigma$
that $A(a)\in\mathcal{A}\subseteq\mathcal{A}^{\prime}$, and thus
$A(a)\in\mathcal{A}^{\prime}$ in both cases. Now, CI (1) and $a\notin
M^{\mathcal{J}^{\prime}}$ imply that $\mathcal{J}^{\prime}$ is not a model of
$\mathcal{K}^{\prime}$, a contradiction.

We are left to show that $\mathcal{J}\not\models q^{\prime}$. Assume to the
contrary that there is a homomorphism $h$ from $\mathcal{D}_{q^{\prime}}$ to
$\mathcal{J}$. We derive a contradiction to $\mathcal{I}\not\models q$ by
showing that $h$ is also a homomorphism from $\mathcal{D}_{q}$ to
$\mathcal{I}$. First, note that $h$ is a function from ${\sf var}(q)$ to
$\Delta^{\mathcal{I}}$ since ${\sf var}(q^{\prime})={\sf var}(q)$ and for each
$x\in{\sf var}(q^{\prime})$, we have $X(x)\in q^{\prime}$ and thus $h(x)\in
X^{\mathcal{J}}=\Delta^{\mathcal{I}}$. Finally, observe that $\mathcal{I}$ is
identical to the restriction of $\mathcal{J}$ to $\Delta^{\mathcal{I}}$ and
the concept and role names that occur in $\mathcal{K}^{\prime}$ and
$q^{\prime}$.

“$\Rightarrow$”. Assume that ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})\not\models q^{\prime}$. Then there is a model
$\mathcal{I}$ of ${\sf Circ_{\sf CP}}(\mathcal{K}^{\prime})$ with
$\mathcal{I}\not\models q^{\prime}$. We show that w.l.o.g, we may assume that
$\mathcal{I}$ satisfies several additional conditions that shall prove to be
convenient in what follows.

######  Claim 2.

There is a model $\mathcal{I}$ of ${\sf Circ_{\sf CP}}(\mathcal{K}^{\prime})$
with $\mathcal{I}\not\models q^{\prime}$ that satisfies the following
properties.

  1. (a)

$a\in A^{\mathcal{I}}$ implies $A(a)\in\mathcal{A}^{\prime}$ for all $a\in{\sf
var}(q)\cup\\{t\\}$,

  2. (b)

$(d,e)\in r^{\mathcal{I}}$ implies $r(d,e)\in\mathcal{A}^{\prime}$ for all
$d,e\in\Delta^{\mathcal{I}}$ with $\\{d,e\\}\cap(\\{{\sf
var}(q)\\}\cup\\{t\\})\neq\emptyset$, and

  3. (c)

$(d,e)\in u^{\mathcal{I}}$ implies $u(d,e)\in\mathcal{A}^{\prime}$ for all
$d,e\in\Delta^{\mathcal{I}}$.

We may construct the desired $\mathcal{I}$ from any model
$\mathcal{I}^{\prime}$ of ${\sf Circ_{\sf CP}}(\mathcal{K}^{\prime})$ with
$\mathcal{I}^{\prime}\not\models q^{\prime}$, as follows:

$\displaystyle\Delta^{\mathcal{I}}$
$\displaystyle\coloneqq\Delta^{\mathcal{I}^{\prime}}$ $\displaystyle
A^{\mathcal{I}}$ $\displaystyle\coloneqq
A^{\mathcal{I}^{\prime}}\setminus\\{a\in{\sf var}(q)\cup\\{t\\}\mid
A(a)\notin\mathcal{A}^{\prime}\\}$ $\displaystyle u^{\mathcal{I}}$
$\displaystyle\coloneqq\\{(x,y)\mid u(x,y)\in\mathcal{A}^{\prime}\\}$
$\displaystyle\begin{split}r^{\mathcal{I}}&\coloneqq
r^{\mathcal{I}^{\prime}}\setminus\\{(x,y)\mid
r(x,y)\notin\mathcal{A}^{\prime}\text{ and }\\\ &\phantom{\coloneqq
r^{\mathcal{I}^{\prime}}\setminus\\{(x,y)\mid\;\,}\\{x,y\\}\cap({\sf
var}(q)\cup\\{t\\})\neq\emptyset\\}\end{split}$

for all concept names $A$ and role names $r\neq u$. Obviously,
$\mathcal{I}\not\models q^{\prime}$, $\mathcal{I}\models\mathcal{A}^{\prime}$
and Points (a) to (b) hold by construction. To show that
$\mathcal{I}\models\mathcal{T}^{\prime}$, note the following:

  * •

$\mathcal{I}$ obviously satisfies the CIs (1) by construction and the fact
that $\mathcal{I}^{\prime}$ is a model of $\mathcal{K}^{\prime}$.

  * •

$\mathcal{I}$ satisfies CIs (3), (8) and (17) as $L^{\mathcal{I}^{\prime}}$
must be empty—otherwise Assertions (7) and CIs (8) activate the copy of $q$ in
$\mathcal{A}^{\prime}$ and thus there is a trivial homomorphism from
$q^{\prime}$ to $\mathcal{I}^{\prime}$, contradicting
$\mathcal{I}^{\prime}\not\models q^{\prime}$.

  * •

For the CIs (9)–(12), observe that $X^{\mathcal{I}^{\prime}}\cap({\sf
var}(q)\cup\\{t\\})=\emptyset$ following the same argument and using
Assertions (15) and CI (17). Hence

$X^{\mathcal{I}^{\prime}}\cap A^{\mathcal{I}^{\prime}}=X^{\mathcal{I}}\cap
A^{\mathcal{I}}$

and

$(X^{\mathcal{I}^{\prime}}\times X^{\mathcal{I}^{\prime}})\cap
r^{\mathcal{I}^{\prime}}=(X^{\mathcal{I}}\times X^{\mathcal{I}})\cap
r^{\mathcal{I}}$

for all concept names $A$ and role names $r\neq u$. Consequently, it is easy
to see that for all CIs $\alpha\in\mathcal{T}^{\prime}$ we have
$\mathcal{I}\models\alpha$ as $\mathcal{I}^{\prime}\models\alpha$.

  * •

We are left to show that $\mathcal{I}$ is minimal; however, this is easy to
see as $\mathcal{I}^{\prime}$ is minimal and $\mathcal{I}\leq_{\sf
CP}\mathcal{I}^{\prime}$.

This finishes the proof of Claim 2.

We aim to show that the interpretation $\mathcal{J}$, obtained as the
restriction of $\mathcal{I}$ to domain ${X^{\mathcal{I}}}$, is a model of
$\mathcal{K}_{\Sigma}$ with $\mathcal{J}\not\models q$. We assume that the
properties from Claim 2 are satisfied, and Property (a) yields
$\Delta^{\mathcal{J}}\cap({\sf var}(q)\cup\\{t\\})=\emptyset$. Assertion (6)
yields ${\sf ind}(\mathcal{A})\subseteq\Delta^{\mathcal{J}}$ and since
$\mathcal{A}\subseteq\mathcal{A}^{\prime}$ and $\mathcal{I}$ is a model of
$\mathcal{A}^{\prime}$, $\mathcal{J}$ must be a model of $\mathcal{A}$. Since
$\mathcal{J}$ is the restriction of $\mathcal{I}$ to $X^{\mathcal{I}}$ and
$\mathcal{I}$ satisfies CIs (9)–(12), $\mathcal{J}$ must satisfy $\mathcal{T}$
as well.

To see that $\mathcal{J}\not\models q$, assume to the contrary that there is a
homomorphism $h$ from $q$ to $\mathcal{J}$. As $\mathcal{J}$ is the
restriction of $\mathcal{I}$ to $X^{\mathcal{I}}$ and $q^{\prime}$ is the
extension of $q$ that adds atoms $X(x)$ for all variables $x$, $h$ must also
be a homomorphism from $q^{\prime}$ to $\mathcal{I}$. This contradicts
$\mathcal{I}\not\models q^{\prime}$.

We are left to argue that $\mathcal{J}$ respects $\Sigma$. Assume to the
contrary that there is some $A\in\Sigma$ and $d_{0}\in A^{\mathcal{J}}$ with
$A(d_{0})\notin\mathcal{A}$. We have $d_{0}\in X^{\mathcal{I}}$ by
construction of $\mathcal{J}$. First assume that $d_{0}\in{\sf
ind}(\mathcal{A})$. Then (2), (3), (7), and (8) activate the copy of $q$ in
$\mathcal{A}^{\prime}$, giving a homomorphism from $q$ to $\mathcal{I}$,
contradicting $\mathcal{I}\not\models q^{\prime}$.

The more laborious case is $d_{0}\notin{\sf ind}(\mathcal{A})$. As we show in
the following, we may then construct a model $\mathcal{I}^{\prime}<_{\sf
CP}\mathcal{I}$ of $\mathcal{K}^{\prime}$, contradicting the minimality of
$\mathcal{I}$.

Intuitively, in the construction of $\mathcal{I}^{\prime}$ we replace $d_{0}$
with $t$ by making true at $t$ all concept names that are true at $d_{0}$,
making false all concept names at $d_{0}$, and “redirecting” all incoming and
outgoing edges of $d_{0}$ to $t$. This forces us to make $X$ true at $t$, and
by (8) and (15) to (17) we must activate the copy of $q$ in
$\mathcal{A}^{\prime}$. But then the CIs (9)–(12) apply to that copy. To
satisfy them, we make all concept and role names true in the copy of $q$. In
detail:

$\displaystyle\Delta^{\mathcal{I}^{\prime}}$
$\displaystyle\coloneqq\Delta^{\mathcal{I}}$ $\displaystyle
A^{\mathcal{I}^{\prime}}$
$\displaystyle\coloneqq(A^{\mathcal{I}}\setminus\\{d_{0}\\})\cup\\{t\mid
d_{0}\in A^{\mathcal{I}}\\}\cup{\sf var}(q)$ $\displaystyle
L^{\mathcal{I}^{\prime}}$ $\displaystyle\coloneqq\Delta^{\mathcal{I}}$
$\displaystyle\begin{split}r^{\mathcal{I}^{\prime}}&\coloneqq(r^{\mathcal{I}}\setminus\\{(d,e)\mid
d_{0}\in\\{d,e\\}\\})\\\ &\phantom{\coloneqq}\cup\\{(e,t)\mid(e,d_{0})\in
r^{\mathcal{I}}\text{ and }e\neq d_{0}\\}\\\
&\phantom{\coloneqq}\cup\\{(t,e)\mid(d_{0},e)\in r^{\mathcal{I}}\text{ and
}e\neq d_{0}\\}\\\ &\phantom{\coloneqq}\cup\\{(t,t)\mid(d_{0},d_{0})\in
r^{\mathcal{I}}\\}\\\ &\phantom{\coloneqq}\cup({\sf var}(q)\times{\sf
var}(q))\end{split}$

for all concept names $A\neq L$ and role names $r$.

Because $\mathcal{I}$ satisfies Assertions (13) and (14) and
$d_{0}\in\Delta^{\mathcal{J}}$ cannot be from ${\sf var}(q)\cup\\{t\\}$, we
have $M^{\mathcal{I}^{\prime}}=M^{\mathcal{I}}\setminus\\{d_{0}\\}$ by
construction of $\mathcal{I}^{\prime}$. Thus $\mathcal{I}^{\prime}<_{\sf
CP}\mathcal{I}$, as desired. It remains to prove that $\mathcal{I}^{\prime}$
is a model of $\mathcal{K}^{\prime}$. We have
$\mathcal{I}^{\prime}\models\mathcal{A}^{\prime}$ because
$\mathcal{I}\models\mathcal{A}^{\prime}$ and the restrictions of $\mathcal{I}$
and of $\mathcal{I}^{\prime}$ to ${\sf ind}(\mathcal{A}^{\prime})$ are
identical.

To see that $\mathcal{I}^{\prime}$ satisfies the CIs (1), let $x\in
A^{\mathcal{I}^{\prime}}$ with $A\in\Sigma$. If $x\in{\sf var}(q)\cup\\{t\\}$,
then $x\in M^{\mathcal{I}}$ due to Assertions (13) and (14), and thus $x\in
M^{\mathcal{I}^{\prime}}$ by construction of $\mathcal{I}^{\prime}$.
Otherwise, we have $x\in A^{\mathcal{I}}$ by construction of
$A^{\mathcal{I}^{\prime}}$, yielding $x\in M^{\mathcal{I}}$ via Assertions
(1). We must have $x\neq d_{0}$ and thus $x\in M^{\mathcal{I}^{\prime}}$ by
construction of $\mathcal{I}^{\prime}$. $\mathcal{I}^{\prime}$ obviously
satisfies CIs (3) and (17) by $L^{\mathcal{I}^{\prime}}=\Delta^{\mathcal{I}}$.

For CIs (9), consider some $X\sqsubseteq A\in\mathcal{T}^{\prime}$ and let
$x\in X^{\mathcal{I}^{\prime}}$. We know that $x\neq d_{0}$ as $d_{0}\notin
X^{\mathcal{I}^{\prime}}$ by construction. If $x\in{\sf var}(q)$, $x\in
A^{\mathcal{I}^{\prime}}$ is entailed by construction. If $x=t$, note that
Point (a) of Claim (2) and the construction of $\mathcal{I}^{\prime}$ imply

$\displaystyle t\in A^{\mathcal{I}^{\prime}}\text{ iff }d_{0}\in
A^{\mathcal{I}}$ (†)

for all concept names $A\neq L$. Thus, $d_{0}\in X^{\mathcal{I}}$. Together
with the fact that $\mathcal{I}$ as a model of $\mathcal{K}^{\prime}$ must
satisfy $X\sqsubseteq A$, we have that $d_{0}\in A^{\mathcal{I}}$. Ergo, $t\in
A^{\mathcal{I}^{\prime}}$ follows via († ‣ B). Similarly, if
$x\in\Delta^{\mathcal{I}}\setminus({\sf var}(q)\cup\\{d_{0},t\\})$, then $x\in
X^{\mathcal{I}}$ holds by construction, and as $\mathcal{I}$ satisfies
$X\sqsubseteq A$, we have $x\in A^{\mathcal{I}}$. This yields $x\in
A^{\mathcal{I}^{\prime}}$ by construction.

For CIs (10), consider some $X\sqcap A\sqsubseteq\exists r.(X\sqcap
B)\in\mathcal{T}^{\prime}$ and let $x\in(X\sqcap A)^{\mathcal{I}^{\prime}}$.
Again, $x\neq d_{0}$. If $x\in{\sf var}(q)$, $x\in(\exists r.(X\sqcap
B))^{\mathcal{I}^{\prime}}$ follows directly as $(x,x)\in
r^{\mathcal{I}^{\prime}}$ and $x\in(X\sqcap B)^{\mathcal{I}^{\prime}}$ hold by
construction. If $x=t$, Property († ‣ B) implies $d_{0}\in(X\sqcap
A)^{\mathcal{I}}$. Together with the fact that $\mathcal{I}$ as a model of
$\mathcal{K}^{\prime}$ must satisfy $X\sqcap A\sqsubseteq\exists r.(X\sqcap
B)$, there must be some $y\in\Delta^{\mathcal{I}}$ such that $(d_{0},y)\in
r^{\mathcal{I}}$ and $y\in(X\sqcap B)^{\mathcal{I}}$. Observe that Point (b)
of Claim (2) and the construction of $\mathcal{I}^{\prime}$ imply

$\displaystyle\big{(}t,f(y)\big{)}\in r^{\mathcal{I}^{\prime}}\text{ iff }$
$\displaystyle(d_{0},y)\in r^{\mathcal{I}}\text{, where}$ $\displaystyle
f(y)\coloneqq$ $\displaystyle\begin{cases}t&\text{if }y=d_{0}\\\
y&\text{otherwise}\end{cases}$

for all role names $r$. We thus have $(t,f(y))\in r^{\mathcal{I}^{\prime}}$.
If $y=d_{0}$, Property († ‣ B) furthermore implies $f(y)\in(X\sqcap
B)^{\mathcal{I}^{\prime}}$. Otherwise, $f(y)\in(X\sqcap
B)^{\mathcal{I}^{\prime}}$ is entailed by construction. In either case, we
have $x\in(\exists r.(X\sqcap B))^{\mathcal{I}^{\prime}}$. Finally, if
$x\in\Delta^{\mathcal{I}}\setminus({\sf var}(q)\cup\\{t,d_{0}\\})$, then
$x\in(X\sqcap A)^{\mathcal{I}}$ follows via construction. As $\mathcal{I}$ is
a model of $\mathcal{K}^{\prime}$, $\mathcal{I}$ must satisfy $X\sqcap
A\sqsubseteq\exists r.(X\sqcap B)$, i.e., there must be some $y\in(X\sqcap
B)^{\mathcal{I}}$ such that $(x,y)\in r^{\mathcal{I}}$. If $y\neq d_{0}$,
$y\in(X\sqcap B)^{\mathcal{I}^{\prime}}$ and $(x,y)\in
r^{\mathcal{I}^{\prime}}$ follow by construction of $\mathcal{I}^{\prime}$.
Otherwise, we have $t\in(X\sqcap B)^{\mathcal{I}^{\prime}}$ and $(x,t)\in
r^{\mathcal{I}^{\prime}}$ by construction. In either case, $x\in(\exists
r.(X\sqcap B))^{\mathcal{I}^{\prime}}$ holds.

We omit the details for the cases of CIs (11) and (12) as they are very
similar to those for CIs (10) and (9), respectively.

For CIs (8), let $x\in(\exists u.L)^{\mathcal{I}^{\prime}}$. Point (c) of
Claim (2) and the construction of $\mathcal{A}^{\prime}$ entail that $x\in{\sf
var}(q)$. By construction of $\mathcal{I}^{\prime}$, we get $x\in
X^{\mathcal{I}^{\prime}}$ as desired.

∎

##  Appendix C Proofs for Section 3.3

In the main part of the paper, we have defined neighborhoods only for the
unraveling $\mathcal{I}^{\prime}$ of the interpretation $\mathcal{I}$. In the
proofs, we also consider neighborhods in the quotient
$\mathcal{J}=\mathcal{I}^{\prime}/{\sim_{{{\left|{q}\right|}+1}}}$. We thus
start with a more general definition of neighborhoods.

Let $\mathcal{I}$ be an interpretation and
$\Delta\subseteq\Delta^{\mathcal{I}}$. For $n\geq 0$ and
$d\in\Delta^{\mathcal{I}}\setminus\Delta$, we use
$\mathcal{N}_{n}^{{\mathcal{I}},\Delta}(d)$ to denote the _$n$ -neighborhood
of $d$ in $\mathcal{I}$ up to_ $\Delta$, that is, the set of all elements
$e\in\Delta^{\mathcal{I}}\setminus\Delta$ such that the undirected graph
$G_{\mathcal{I}}$ associated with $\mathcal{I}$ contains a path
$d_{0},\dots,d_{k}$ with $0\leq k\leq n$, $d_{0}=d$,
$d_{0},\dots,d_{k-1}\notin\Delta$, and $d_{k}=e$.

So the neighborhoods $\mathcal{N}_{n}(d)$ defined in the main body of the
paper are now called
$\mathcal{N}_{n}^{{\mathcal{I}^{\prime}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(d)$.

See 7

We prove that
$\mathcal{J}=\mathcal{I}^{\prime}/{\sim_{{{\left|{q}\right|}+1}}}$ is indeed a
model of ${\sf Circ_{\sf CP}}(\mathcal{K})$ with $\mathcal{J}\not\models
q(\bar{a})$. The key to proving the latter is to exhibit suitable local
homomorphisms from $\mathcal{J}$ back to $\mathcal{I}^{\prime}$. The existence
of a homomorphism $h$ from a CQ $p(\bar{x})$ in $q$ to $\mathcal{J}$ with
$h(\bar{x})=a$ would then contradict the fact that $\mathcal{I}^{\prime}$ is a
countermodel of $q$. Indeed, such a homomorphism $h$ would map each connected
component $C$ of $p$ into a ${\left|{q}\right|}$-neighborhood
$\mathcal{N}_{{\left|{q}\right|}}^{\mathcal{J},{\overline{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}({\overline{c}})$,
for some $c\in\Delta^{\mathcal{I}^{\prime}}$ and where
${\overline{\Delta_{\mathsf{base}}^{\mathcal{I}}}}$ stands for the set
$\\{{\overline{e}}\mid e\in{\Delta_{\mathsf{base}}^{\mathcal{I}}}\\}$. By
exhibiting a homomorphism
$\rho_{c}:\mathcal{N}_{{\left|{q}\right|}}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})\rightarrow\mathcal{N}_{{\left|{q}\right|}}^{\mathcal{I}^{\prime},{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}({c})$
such that
$\rho_{c}^{-1}({\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}})\subseteq{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$,
we can find a homomorphism from $C$ to $\mathcal{I}^{\prime}$. Taking the
union of homomorphisms for all of $p$’s connected components gives a
homomorphism from the full $p$ to $\mathcal{I}^{\prime}$.

Except for the use of Lemma 2, concerned with circumscription, we roughly
follow (?), with slight simplifications as we are not considering negative
role inclusions. For all $n\geq 0$, all $c\in\Delta^{\mathcal{I}^{\prime}}$,
and all
$d\in\mathcal{N}_{n}^{\mathcal{I}^{\prime},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$,
we denote $w_{n,c}^{d}$ the (unique) word such that $d={p_{n,c}w_{n,c}^{d}}$.
Let us first formulate two remarks concerning the constructed interpretation
$\mathcal{J}$.

######  Remark 2.

Combining Conditions 1 and 2.(a) from the definition of $\sim_{n}$, gives: if
$d_{1}\sim_{n}d_{2}$, then
$\mathsf{tp}_{\mathcal{I}^{\prime}}({d_{1}})=\mathsf{tp}_{\mathcal{I}^{\prime}}({d_{2}})$.

######  Remark 3.

If $d_{1}\sim_{n}d_{2}$, then $d_{1}\sim_{m}d_{2}$ for any $m\leq n$.

We now define homomorphisms $\rho_{c}$, mentioned in the proof sketch,
inductively on $n$ increasing from $0$ to ${\left|{q}\right|}$. Starting from
the element
${\overline{c}}\in\mathcal{N}_{0}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$,
we can naturally carry it back as
$\rho_{c}({\overline{c}})=c\in\mathcal{N}_{0}^{\mathcal{I}^{\prime},{\Delta_{\mathsf{base}}^{\mathcal{I}}}}({c})$.
Assume now that we have defined $\rho_{c}({\overline{d}})$ for some
${\overline{d}}\in\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$
and that we are moving further to an element
${\overline{e}}\in\mathcal{N}_{n+1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$
along an edge $({\overline{d}},{\overline{e}})$ in $\mathcal{J}$. In the case
of ${\overline{e}}\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$,
the following lemma produces an element $e^{\prime}$ which is to
$\rho_{c}({\overline{d}})$ (that is $d^{\prime}$ in the below statement), what
${\overline{e}}$ is to ${\overline{d}}$. We will thus set
$\rho_{c}({\overline{e}})$ to $e^{\prime}$. The case disjunction that arises
reflects $e^{\prime}$ being either a successor of $d^{\prime}$ in the
corresponding tree-shaped structure of the unraveling $\mathcal{I}^{\prime}$
(which is identified in the quotient $\mathcal{J}$ as
${\left|{e}\right|}\equiv{\left|{d}\right|}+1\mod 2{\left|{q}\right|}+3$), or
the converse (identified as ${\left|{d}\right|}\equiv{\left|{e}\right|}+1\mod
2{\left|{q}\right|}+3$).

######  Lemma 18.

Given two elements
${\overline{d}},{\overline{e}}\in\Delta^{\mathcal{J}}\setminus{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$,
if there exists a role ${{p}}$ such that
$({\overline{d}},{\overline{e}})\in{{p}}^{\mathcal{J}}$, then there exists a
unique element $rB\in\Omega$ such that one of the two following conditions is
satisfied:

  * r+.

${\left|{e}\right|}\equiv{\left|{d}\right|}+1\mod 2{\left|{q}\right|}+3$,
$w_{{{\left|{q}\right|}+1},e}^{e}=w_{{\left|{q}\right|},d}^{d}rB$ and
$\mathcal{T}\models{r}\sqsubseteq{p}$. Furthermore, for all
$d^{\prime}\sim_{n}d$, the element $e^{\prime}=d^{\prime}rB$ belongs to
$\Delta^{\mathcal{I}^{\prime}}$ and satisfies $e^{\prime}\sim_{n-1}e$.

  * r-.

${\left|{d}\right|}\equiv{\left|{e}\right|}+1\mod 2{\left|{q}\right|}+3$,
$w_{{{\left|{q}\right|}+1},d}^{d}=w_{{\left|{q}\right|},e}^{e}rB$ and
$\mathcal{T}\models{r^{-}}\sqsubseteq{p}$. Furthermore, for all
$d^{\prime}\sim_{n}d$, we have $e^{\prime}$ such that
$d^{\prime}=e^{\prime}rB$ and the prefix $e^{\prime}$ satisfies
$e^{\prime}\sim_{n-1}e$.

###### Proof.

Notice the two conditions are mutually exclusive:
${\left|{e}\right|}\equiv{\left|{d}\right|}+1\mod 2{\left|{q}\right|}+3$ and
${\left|{d}\right|}\equiv{\left|{e}\right|}+1\mod 2{\left|{q}\right|}+3$ would
imply $0\equiv 2\mod 2{\left|{q}\right|}+3$, which is impossible as
$2{\left|{q}\right|}+3>2$. Furthermore, in each case ${{r}}{{B}}$ is defined
as the last letter of the word $w_{{{\left|{q}\right|}+1},e}^{e}$ (resp
$w_{{{\left|{q}\right|}+1},d}^{d}$), which is unique and does not depends on
the choice of $e$ (resp $d$) nor on ${{p}}$. This proves the uniqueness.

We now focus on the existence and the additional property. From the definition
of ${{p}}^{\mathcal{J}}$, there exist
$({d_{0}},{e_{0}})\in{{p}}^{\mathcal{I}^{\prime}}$ such that
${\overline{d_{0}}}={\overline{d}}$ and ${\overline{e_{0}}}={\overline{e}}$.
Recall
${\overline{d}},{\overline{e}}\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$,
hence $d_{0},e_{0}\notin{\Delta_{\mathsf{base}}^{\mathcal{I}}}$. Therefore the
definition of ${{p}}^{\mathcal{I}^{\prime}}$, yields two cases:

  * •

We have $e_{0}=d_{0}{{r}}{{B}}$ with $\mathcal{T}\models{r}\sqsubseteq{p}$. It
follows that ${\left|{e_{0}}\right|}={\left|{d_{0}}\right|}+1\mod
2{\left|{q}\right|}+3$ and
$w_{{{\left|{q}\right|}+1},e_{0}}^{e_{0}}=w_{{{\left|{q}\right|}+1}-1,d_{0}}^{d_{0}}{{r}}{{B}}$,
immediately yielding the same properties for $d$ and $e$ as
$({\overline{d_{0}}},{\overline{e_{0}}})=({\overline{d}},{\overline{e}})$.

Consider now $d^{\prime}$ and $1\leq n\leq{{\left|{q}\right|}+1}$ s.t. now
$d^{\prime}\sim_{n}d$. Transitivity gives $d^{\prime}\sim_{n}d_{0}$, and we
have in particular $w_{n,d^{\prime}}^{d^{\prime}}=w_{n,d_{0}}^{d_{0}}$. Recall
that $e_{0}=d_{0}{{r}}{{B}}$, hence Condition 2 from the definition of
$d^{\prime}\sim_{n}d_{0}$ ensures $d^{\prime}{{r}}{{B}}$ belongs to
$\Delta^{\mathcal{I}^{\prime}}$. Notice it is now sufficient to prove
$d^{\prime}{{r}}{{B}}\sim_{n-1}e_{0}$: that is because
${\overline{e}}={\overline{e_{0}}}$, hence transitivity will conclude the
proof. It should be clear that
$w_{n-1,d^{\prime}{{r}}{{B}}}^{d^{\prime}{{r}}{{B}}}=w_{n-1,e_{0}}^{e_{0}}$
and ${\left|{d^{\prime}{{r}}{{B}}}\right|}\equiv{\left|{e_{0}}\right|}\mod
2{\left|{q}\right|}+3$, hence Conditions 1 and 3 from the definition of
$\sim_{n-1}$ are satisfied. To verify Condition 2, it suffices to remark that
$e_{0}=d_{0}{{r}}{{B}}$ ensures that the characterization via paths of the
$n$-neighborhood of $d_{0}$ fully determines the characterization of the
$(n-1)$ neighborhood of $e_{0}$. But since the former coincides with the
characterization of the $n$-neighborhood of $d^{\prime}$ (using Condition 2
from the definition of ${\overline{d_{0}}}={\overline{d^{\prime}}}$), that
fully decides the characterization of the $(n-1)$-neighborhood of
$e^{\prime}$, we are done.

  * •

We have $d_{0}=e_{0}{{r}}{{B}}$ with
$\mathcal{T}\models{r^{-}}\sqsubseteq{p}$. It follows that
${\left|{d_{0}}\right|}\equiv{\left|{e_{0}}\right|}+1\mod
2{\left|{q}\right|}+3$ and
$w_{{{\left|{q}\right|}+1},d_{0}}^{d_{0}}=w_{{{\left|{q}\right|}+1}-1,e_{0}}^{e_{0}}{{r}}{{B}}$,
immediately yielding the same properties for $d$ and $e$ as
$({\overline{d_{0}}},{\overline{e_{0}}})=({\overline{d}},{\overline{e}})$.

Let now $1\leq n\leq{{\left|{q}\right|}+1}+1$ be an integer and
$d^{\prime}\sim_{n}d$. Transitivity gives $d^{\prime}\sim_{n}d_{0}$, and we
have in particular
$w_{1,d^{\prime}}^{d^{\prime}}=w_{1,d_{0}}^{d_{0}}={{r}}{{B}}$ (it is here
important to have $n\geq 1$!). That is $d^{\prime}$ ends by ${{r}}{{B}}$, and
therefore we can indeed have prefix $e^{\prime}$ such that
$d^{\prime}=e^{\prime}{{r}}{{B}}$. ∎

Notice the “strength” of the equivalence relation $\sim_{n}$ between
${\overline{e}}$ and $\rho_{c}({\overline{e}})$ decreases as we move further
in the neighbourhood of ${\overline{c}}$. However, since we start from
$\rho_{c}({\overline{c}}):=c\sim_{{{\left|{q}\right|}+1}}c$ and explore a
${\left|{q}\right|}$-neighbourhood, the index remains at least $1$. This is
essential as $\sim_{1}$ notably encodes relations to elements of
${\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$ as required by Condition
2.(b) from the definition of $\sim_{1}$.

It remains to abstract from the particular choice of ${\overline{d}}$, which
is likely not to be the only element of
$\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$
connected to ${\overline{e}}$. Taking a closer look at Lemma 18, we observe
that $\rho_{c}({\overline{e}})$, that is $e^{\prime}$, is obtained either by
adding a letter to $\rho_{c}({\overline{d}})$, that is $d^{\prime}$, or by
removing the last letter of $\rho_{c}({\overline{d}})$, and that these letters
coincide with those in the suffixes of elements ${d}$ and ${e}$. Therefore,
when moving from ${\overline{c}}$ to ${\overline{e}}$, each added letter
appears already in the suffix $w_{{\left|{q}\right|}+1,e}^{e}$ of ${e}$ and,
similarly, each removed letter appeared in the suffix
$w_{{\left|{q}\right|}+1,c}^{c}$ of $c$. This is however not completely true
as some steps along the way from ${\overline{c}}$ to ${\overline{e}}$ may
cancel each other, _e.g._ a letter is introduced at one step and removed on
the next one.

The challenge is therefore to decide the numbers $l^{+}$ of _actual_ additions
and $l^{-}$ of _actual_ removals to build $\rho_{c}({\overline{e}})$ directly
from $c$ and ${\overline{e}}$ (which determines
$w_{{\left|{q}\right|}+1,e}^{e}$). We then drop the $l^{-}$ last letters from
$c$, which intuitively corresponds to keeping its prefix $p_{l^{-},c}$, and
keep the $l^{+}$ last letters from $w_{{\left|{q}\right|}+1,e}^{e}$, which
intuitively corresponds to $w_{l^{+},e}^{e}$, and concatenate those two words.
To this end, the next definition captures the relative difference of letters
between ${\overline{c}}$ and ${\overline{e}}$, encoded in ${\left|{c}\right|}$
and ${\left|{e}\right|}\mod 2{\left|{q}\right|}+3$.

######  Definition 5.

Let ${\overline{c}}\in\Delta^{\mathcal{J}}$ and $n\leq{\left|{q}\right|}$. The
_relative depth_ of
${\overline{e}}\in\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$
from ${\overline{c}}$ is the integer
$\delta_{{\overline{c}}}({\overline{e}})\in[-n,n]$ such that
${\left|{e}\right|}\equiv{\left|{c}\right|}+\delta_{{\overline{c}}}({\overline{e}})\mod
2{\left|{q}\right|}+3$.

######  Remark 4.

By induction on $n\leq{\left|{q}\right|}$, it is straightforward to see that
$\delta_{{\overline{c}}}({\overline{e}})$ is well defined. Uniqueness is
ensured by $\delta_{{\overline{c}}}({\overline{e}})\leq
n\leq{\left|{q}\right|}$. A consequence of Lemma 18 is that for the smallest
$n\leq{\left|{q}\right|}$ such that
${\overline{e}}\in\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$
we have $\delta_{{\overline{c}}}({\overline{e}})=n\mod 2$.

We can now identify how many additions and removals canceled each other.
Indeed, if it takes exactly $n$ steps to reach ${\overline{e}}$ from
${\overline{c}}$, with relative difference of
$\delta:=\delta_{{\overline{c}}}({\overline{e}})$, then
$n-{\left|{\delta}\right|}$ is the number of steps that canceled each other,
hence: $\frac{n-{\left|{\delta}\right|}}{2}$ canceled additions and
$\frac{n-{\left|{\delta}\right|}}{2}$ canceled removals. Therefore, the number
$l^{+}$ of _actual_ additions is $\frac{n-{\left|{\delta}\right|}}{2}+\delta$
if $\delta\geq 0$, or $\frac{n-{\left|{\delta}\right|}}{2}$ if $\delta\leq 0$,
that is in both cases $\frac{n+\delta}{2}$. Similarly we obtain
$\frac{n-\delta}{2}$ for the number $l^{-}$ of _actual_ removals. Notice
Remark 4 ensures both $l^{+}$ and $l^{-}$ are integers.

The next theorem formalizes the above intuitions. Notably, in the non-trivial
cases, $\rho_{n,c}({\overline{e}})$ is obtained by removing the
$\frac{n-\delta}{2}$ last letters of ${c}$ and keeping the
$\frac{n+\delta}{2}$ last letters from the suffix of ${e}$, which results in
the word
$p_{\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},c}w_{\frac{n+\delta_{{\overline{c}}}({\overline{e}})}{2},e}^{e}$.
It is then a technicality to verify these syntactical operations on words
produces an element in the domain of $\mathcal{I}^{\prime}$ and that the
defined $\rho_{n,c}$ is a homomorphism as desired.

######  Lemma 19.

For all $c\in\Delta^{\mathcal{I}^{\prime}}$ and all $n\leq{\left|{q}\right|}$,
the following mapping $\rho_{n,c}({\overline{e}})$:

$\begin{array}[]{r@{\;}c@{\;}l}\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})&\rightarrow&\mathcal{N}_{n}^{\mathcal{I}^{\prime},{\Delta_{\mathsf{base}}^{\mathcal{I}}}}(c)\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
{\overline{e}}&\mapsto&\left\\{\begin{array}[]{ll}\rho_{n-1,c}({\overline{e}})\qquad\text{if
}{\overline{e}}\in\mathcal{N}_{n-1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})\vskip
3.0pt plus 1.0pt minus 1.0pt\\\ e\qquad\qquad\qquad\text{if
}{\overline{e}}\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
p_{\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},c}w_{\frac{n+\delta_{{\overline{c}}}({\overline{e}})}{2},e}^{e}\quad\text{otherwise}\end{array}\right.\end{array}$

is a homomorphism satisfying
$\rho_{n,c}({\overline{{e}}})\sim_{{{\left|{q}\right|}+1}-n}{e}$ and
$\rho_{n,c}^{-1}({\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}})\subseteq{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$.

###### Proof.

Let $c\in\Delta^{\mathcal{I}^{\prime}}$. We proceed by induction on
$n\leq{\left|{q}\right|}$ and prove along a technical statement. Property
$\rho_{n,c}({\overline{e}})\sim_{{{\left|{q}\right|}+1}-n}{e}$ already ensures
$w_{{{\left|{q}\right|}+1}-n,\rho_{n,c}({\overline{e}})}^{\rho_{n,c}({\overline{e}})}=w_{{{\left|{q}\right|}+1}-n,e}^{e}$;
we reinforce this latter fact as follows. If
$e\in\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})\setminus\mathcal{N}_{n-1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$,
then:

$w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},\rho_{n,c}({\overline{e}})}^{\rho_{n,c}({\overline{e}})}=w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},e}^{e}$
($*$)

It is indeed a stronger statement since
$-n\leq\delta_{{\overline{c}}}({\overline{e}})\leq n$ leads to
$0\leq\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2}\leq n$, hence
${{\left|{q}\right|}+1}-n\leq{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2}$.
Property $*$ ‣ C therefore provides a more precise information about the
suffix of $\rho_{n,c}{e}$.

Base case: $n=0$. Let
${\overline{e}}\in\mathcal{N}_{0}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$,
hence ${\overline{e}}={\overline{c}}$. If
${\overline{c}}\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$, then
$\rho_{0,c}{e}=e=c$. Otherwise we have
$\delta_{{\overline{c}}}({\overline{e}})=0$, hence
$\rho_{0,c}{e}=p_{0,c}w_{0,c}^{c}=c$. In both cases $\rho_{0,c}{e}=c$, and it
is straightforward that all the desired properties hold. In particular,
agreeing that
$\mathcal{N}_{-1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$
can reasonably be set to $\emptyset$, our technical statement holds.

Induction case. Assume the statement holds for $0\leq n-1<{\left|{q}\right|}$.
Let
${\overline{e}}\in\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$.
If
${\overline{e}}\in\mathcal{N}_{n-1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$,
then the induction hypothesis applies directly on ${\overline{e}}$ and
provides (stronger versions of) the desired properties. Otherwise, we have by
definition of neighbourhoods an element
${\overline{d}}\in\mathcal{N}_{n-1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$,
not belonging to ${\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$ nor to
$\mathcal{N}_{n-2}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$,
and a role ${{p}}\in\mathsf{N_{R}}^{\pm}$ such that
$({\overline{d}},{\overline{e}})\in{{p}}^{\mathcal{J}}$. We apply the
induction hypothesis on ${\overline{d}}$, which gives
$\rho_{n-1,c}({\overline{d}})=p_{\frac{n-1-\delta_{{\overline{c}}}({\overline{d}})}{2},d}w_{\frac{n-1+\delta_{{\overline{c}}}({\overline{d}})}{2},d}^{d}$
since
${\overline{d}}\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$. We
further distinguish between
${\overline{e}}\in{\Delta_{\mathsf{base}}^{\mathcal{I}}}$ and
${\overline{e}}\notin{\Delta_{\mathsf{base}}^{\mathcal{I}}}$, the latter
subcase yielding two subcases by applying Lemma 18 and distinguishing between
Cases r+and r-. We have therefore three cases to treat.

${\overline{e}}\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$. We
have $\rho_{n,c}({\overline{e}})=e$ and the only non-trivial property to prove
is that
$e\in\mathcal{N}_{n}^{\mathcal{I}^{\prime},{\Delta_{\mathsf{base}}^{\mathcal{I}}}}(c)$.
Recall the induction hypothesis ensures in particular
$\rho_{n-1,c}({\overline{d}})\sim_{1}d$. Condition 2.(b) from the definition
of $\sim_{1}$ ensures
$(\rho_{n-1,c}({\overline{d}}),e)\in{{p}}^{\mathcal{I}^{\prime}}$, which
provides the desired property.

r+. Case r+ensures ${\left|{e}\right|}={\left|{d}\right|}+1\mod
2{\left|{q}\right|}+3$, hence
$\delta_{{\overline{c}}}({\overline{e}})=\delta_{{\overline{c}}}({\overline{d}})+1$,
and
$w_{{{\left|{q}\right|}+1},e}^{e}=w_{{{\left|{q}\right|}+1}-1,d}^{d}{{r}}{{B}}$.
Therefore, our element $\rho_{n,c}({\overline{e}})$ of interest simplifies as:

$\begin{array}[]{r@{\;}c@{\;}l}\rho_{n,c}({\overline{e}})&=&p_{\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},c}w_{\frac{n+\delta_{{\overline{c}}}({\overline{e}})}{2},e}^{e}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=&p_{\frac{n-(\delta_{{\overline{c}}}({\overline{d}})+1)}{2},c}w_{\frac{n+(\delta_{{\overline{c}}}({\overline{d}})+1)}{2},e}^{e}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=&p_{\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2},c}w_{\frac{(n-1)+\delta_{{\overline{c}}}({\overline{d}})}{2}+1,e}^{e}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=&p_{\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2},c}w_{\frac{(n-1)+\delta_{{\overline{c}}}({\overline{d}})}{2},d}^{d}{{r}}{{B}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=&\rho_{n-1,c}({\overline{d}}){{r}}{{B}},\end{array}$

which is well-defined and satisfies
$\rho_{n,c}({\overline{e}})\sim_{{{\left|{q}\right|}+1}-n}e$ from Lemma 18.
Recalling that the induction hypothesis gives
$\rho_{n-1,c}({\overline{d}})\in\mathcal{N}_{n-1}^{\mathcal{I}^{\prime},{\Delta_{\mathsf{base}}^{\mathcal{I}}}}(c)$,
it follows that
$\rho_{n,c}({\overline{e}})\in\mathcal{N}_{n}^{\mathcal{I}^{\prime},{\Delta_{\mathsf{base}}^{\mathcal{I}}}}(c)$.
Furthermore, notice that ${\overline{e}}$ and ${\overline{d}}$ satisfy all
conditions of our additional statement. Since in Case r+we have
$\mathcal{T}\models{r}\sqsubseteq{p}$, reusing
$\rho_{n,c}({\overline{e}})=\rho_{n-1,c}({\overline{d}}){{r}}{{B}}$
immediately yields
$(\rho_{n-1,c}({\overline{d}}),\rho_{n,c}({\overline{e}}))\in{{p}}^{\mathcal{I}^{\prime}}$.

Checking that Property $*$ ‣ C holds is now a technicality, and recall that
since
$d\in\mathcal{N}_{n-1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})\setminus\mathcal{N}_{n-2}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$,
we can apply it to $d$ by induction hypothesis. We hence have:

$\begin{array}[]{r@{\hspace*{-50pt}}l}w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},\rho_{n,c}({\overline{e}})}^{\rho_{n,c}({\overline{e}})}\vskip
3.0pt plus 1.0pt minus 1.\\\
&=w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2}-1,\rho_{n-1,c}({\overline{d}})}^{\rho_{n-1,c}({\overline{d}})}{{r}}{{B}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{(n-1)+1-(\delta_{{\overline{c}}}({\overline{d}})+1)}{2}-1,\rho_{n-1,c}({\overline{d}})}^{\rho_{n-1,c}({\overline{d}})}{{r}}{{B}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2}-1,\rho_{n-1,c}({\overline{d}})}^{\rho_{n-1,c}({\overline{d}})}{{r}}{{B}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2}-1,d}^{d}{{r}}{{B}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},e}^{e}.\end{array}$

r-. Case r-ensures ${\left|{e}\right|}={\left|{d}\right|}-1\mod
2{\left|{q}\right|}+3$, hence
$\delta_{{\overline{c}}}({\overline{e}})=\delta_{{\overline{c}}}({\overline{d}})-1$,
and
$w_{{{\left|{q}\right|}+1},d}^{d}=w_{{{\left|{q}\right|}+1}-1,e}^{e}{{r}}{{B}}$.
By induction hypothesis, element
$\rho_{n-1,c}({\overline{d}})=p_{\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2},d}w_{\frac{(n-1)+\delta_{{\overline{c}}}({\overline{d}})}{2},d}^{d}$
is well-defined. Notice Property $*$ ‣ C on $d$ (which, again can be applied
as
$d\in\mathcal{N}_{n-1}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})\setminus\mathcal{N}_{n-2}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$)
gives more precise information on the suffix of $\rho_{n-1,c}({\overline{d}})$
than the definition of $\rho_{n-1,c}({\overline{d}})$, because
$n\leq{{\left|{q}\right|}+1}$ leads to
$\frac{(n-1)+\delta_{{\overline{c}}}({\overline{d}})}{2}+1\leq{{\left|{q}\right|}+1}-\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2}$.
Therefore,
$w_{\frac{(n-1)+\delta_{{\overline{c}}}({\overline{d}})}{2}+1,d}^{d}$ is
itself a suffix of
$w_{{{\left|{q}\right|}+1}-\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2},d}^{d}$,
which equals
$w_{{{\left|{q}\right|}+1}-\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2},\rho_{n-1,c}({\overline{d}})}^{\rho_{n-1,c}({\overline{d}})}$.
Hence we obtain:

$\begin{array}[]{r@{\;}c@{\;}l}\rho_{n-1,c}({\overline{d}})&=&p_{\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2}+1,d}w_{\frac{(n-1)+\delta_{{\overline{c}}}({\overline{d}})}{2}+1,d}^{d}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=&p_{\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},d}w_{\frac{n+\delta_{{\overline{c}}}({\overline{e}})}{2}+1,d}^{d}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=&p_{\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},d}w_{\frac{n+\delta_{{\overline{c}}}({\overline{e}})}{2},e}^{e}{{r}}{{B}}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=&\rho_{n,c}({\overline{e}}){{r}}{{B}}\end{array}$

Lemma 18 now ensures
$\rho_{n,c}({\overline{e}})\sim_{{{\left|{q}\right|}+1}-n}e$. Recalling that
the induction hypothesis gives
$\rho_{n-1,c}({\overline{d}})\in\mathcal{N}_{n-1}^{\mathcal{I}^{\prime},{\Delta_{\mathsf{base}}^{\mathcal{I}}}}(c)$,
it follows that
$\rho_{n,c}({\overline{e}})\in\mathcal{N}_{n}^{\mathcal{I}^{\prime},{\Delta_{\mathsf{base}}^{\mathcal{I}}}}(c)$.
Furthermore, notice that ${\overline{e}}$ and ${\overline{d}}$ satisfy all
conditions of our additional statement. Since in Case r-we have
$\mathcal{T}\models{r^{-}}\sqsubseteq{p}$, reusing
$\rho_{n-1,c}({\overline{d}})=\rho_{n,c}({\overline{e}}){{r}}{{B}}$
immediately yields
$(\rho_{n-1,c}({\overline{d}}),\rho_{n,c}({\overline{e}}))\in{{p}}^{\mathcal{I}^{\prime}}$.

Again, we check Property $*$ ‣ C holds:

$\begin{array}[]{r@{\hspace*{-50pt}}l}w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},\rho_{n,c}({\overline{e}})}^{\rho_{n,c}({\overline{e}})}{{r}}{{B}}\vskip
3.0pt plus 1.0pt minus 1.\\\
&=w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2}+1,\rho_{n-1,c}({\overline{d}})}^{\rho_{n-1,c}({\overline{d}})}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{(n-1)+1-(\delta_{{\overline{c}}}({\overline{d}})-1)}{2}+1,\rho_{n-1,c}({\overline{d}})}^{\rho_{n-1,c}({\overline{d}})}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2},\rho_{n-1,c}({\overline{d}})}^{\rho_{n-1,c}({\overline{d}})}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{(n-1)-\delta_{{\overline{c}}}({\overline{d}})}{2},d}^{d}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\
&=w_{{{\left|{q}\right|}+1}-\frac{n-\delta_{{\overline{c}}}({\overline{e}})}{2},e}^{e}{{r}}{{B}}\end{array}$

We now verify that $\rho_{n,c}$ is a homomorphism.

  * •

Let
${\overline{u}}\in{{A}}^{\mathcal{J}}\cap\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$.
By definition of ${{A}}^{\mathcal{J}}$, we have
$e\in{{A}}^{\mathcal{I}^{\prime}}$. Since $n\leq{\left|{q}\right|}$ we have
$\rho_{n,c}({\overline{u}})\sim_{1}e$, hence applying Remark 2 we obtain
$\rho_{n,c}({\overline{u}})\in{{A}}^{\mathcal{I}^{\prime}}$.

  * •

Let
$({\overline{u}},{\overline{v}})\in{{r}}^{\mathcal{J}}\cap(\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})\times\mathcal{N}_{n}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}}))$.
If ${\overline{u}}\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$ or
${\overline{v}}\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$, then
Condition 2.(b) from the definition of $\sim_{1}$ applies on
$\rho_{n,c}({\overline{u}})$ or on $\rho_{n,c}({\overline{v}})$ (recall
$\rho_{n,c}({\overline{u}})\sim_{1}u$ and
$\rho_{n,c}({\overline{v}})\sim_{1}v$) and gives
$(\rho_{n,c}({\overline{u}}),\rho_{n,c}({\overline{v}}))\in{{r}}^{\mathcal{J}}$.
Otherwise
${\overline{u}}\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$ and
${\overline{v}}\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$. Let
$n_{1},n_{2}$ be the minimum integers such that
${\overline{u}}\in\mathcal{N}_{n_{1}}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$
and
${\overline{v}}\in\mathcal{N}_{n_{2}}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}({\overline{c}})$.
Since $({\overline{u}},{\overline{v}})\in{{r}}^{\mathcal{J}}$, we have
$n_{1}-n_{2}\in\\{-1,0,1\\}$. Definitions of
$\delta_{{\overline{c}}}({\overline{u}})$ and
$\delta_{{\overline{c}}}({\overline{v}})$ lead to
${\left|{u}\right|}-{\left|{v}\right|}\equiv\delta_{{\overline{c}}}({\overline{u}})-\delta_{{\overline{c}}}({\overline{v}})\mod
2{\left|{q}\right|}+3$. Lemma 18 gives
${\left|{u}\right|}\equiv{\left|{v}\right|}\pm 1\mod 2{\left|{q}\right|}+3$.
Recall
$\delta_{{\overline{c}}}({\overline{u}}),\delta_{{\overline{d}}}({\overline{v}})\in[-{\left|{q}\right|},{\left|{q}\right|}]$,
hence
$-2{\left|{q}\right|}-1\leq\delta_{{\overline{c}}}({\overline{u}})-\delta_{{\overline{c}}}({\overline{u}})\mp
1\leq 2{\left|{q}\right|}+1$. Since
$\delta_{{\overline{c}}}({\overline{u}})-\delta_{{\overline{d}}}({\overline{v}})\mp
1\equiv 0\mod 2{\left|{q}\right|}+3$ and
$2{\left|{q}\right|}+1<2{\left|{q}\right|}+3$, we must have
$\delta_{{\overline{c}}}({\overline{u}})-\delta_{{\overline{c}}}({\overline{v}})=\pm
1$. Joint to Remark 4, it excludes the case $n_{1}-n_{2}=0$. We are hence left
with $n_{1}=n_{2}\pm 1$. Applying our additional property with
$k:=\max(n_{1},n_{2})$ gives
$(\rho_{n,c}({\overline{u}}),\rho_{n,c}({\overline{v}}))\in{{r}}^{\mathcal{I}^{\prime}}$.

Finally,
$\rho_{n,c}^{-1}({{\Delta_{\mathsf{base}}^{\mathcal{I}}}})\subseteq{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$
is a straightforward consequence of $\rho_{n,c}({\overline{u}})\sim_{1}{u}$
(and again, recall elements from ${\Delta_{\mathsf{base}}^{\mathcal{I}}}$ are
alone in their equivalent class!). ∎

Let us now complete the proof of Lemma 7 with Lemma 19 in hand.

###### Proof of Lemma 7.

We first prove that $\mathcal{J}$ is a model of $\mathcal{K}$ by considering
each possible shape of assertions and axioms:

  * •

${{A}}(a)$. Since $\mathcal{I}^{\prime}$ is a model, we have
$a\in{{A}}^{\mathcal{I}^{\prime}}$. Therefore, the definition of
${{A}}^{\mathcal{J}}$ gives ${\overline{a}}=a\in{{A}}^{\mathcal{J}}$.

  * •

${{p}}(a,b)$. Since $\mathcal{I}^{\prime}$ is a model, we have
$(a,b)\in{{p}}^{\mathcal{I}^{\prime}}$. Therefore, the definition of
${{p}}^{\mathcal{J}}$ gives
$({\overline{a}},{\overline{b}})=(a,b)\in{{p}}^{\mathcal{J}}$.

  * •

${\top}\sqsubseteq{A}$. Let $u\in\top^{\mathcal{J}}=\Delta^{\mathcal{J}}$. By
definition of $\Delta^{\mathcal{J}}$, there exists
$u_{0}\in\Delta^{\mathcal{I}^{\prime}}$ such that ${\overline{u_{0}}}=u$.
Since $u_{0}\in\top^{\mathcal{I}^{\prime}}$ and $\mathcal{I}^{\prime}$ is a
model, it ensures $u_{0}\in{{A}}^{\mathcal{I}^{\prime}}$. Therefore the
definition of ${{A}}^{\mathcal{J}}$ gives
$u={\overline{u_{0}}}\in{{A}}^{\mathcal{J}}$.

  * •

${A_{1}\sqcap A_{2}}\sqsubseteq{A}$. Let
$u\in({{A}}_{1}\sqcap{{A}}_{2})^{\mathcal{J}}$. By definition of
${{A}}_{1}^{\mathcal{J}}$ and ${{A}}_{2}^{\mathcal{J}}$, there exists
$u_{1}\in{{A}}_{1}^{\mathcal{I}^{\prime}}$ and
$u_{2}\in{{A}}_{2}^{\mathcal{I}^{\prime}}$ with
${\overline{u_{1}}}={\overline{u_{2}}}=u$. Remark 2 ensures $u_{1}$ and
$u_{2}$ satisfy the same concepts, that is in particular
$u_{1}\in({{A}}_{1}\sqcap{{A}}_{2})^{\mathcal{I}^{\prime}}$. Since
$\mathcal{I}^{\prime}$ is a model, it ensures
$u_{1}\in{{A}}^{\mathcal{I}^{\prime}}$, yielding by definition of
${{A}}^{\mathcal{J}}$ that $u={\overline{u_{1}}}\in{{A}}^{\mathcal{J}}$.

  * •

${A_{1}}\sqsubseteq{\exists{{r}}.{A_{2}}}$. Let $u\in{{A}}_{1}^{\mathcal{J}}$.
By definition of ${{A_{1}}}^{\mathcal{J}}$ there exists
$u_{0}\in{{A_{1}}}^{\mathcal{I}^{\prime}}$ with ${\overline{u_{0}}}=u$. Since
$\mathcal{I}^{\prime}$ is a model, it ensures there exists
$v_{0}\in{{A_{2}}}^{\mathcal{I}^{\prime}}$ with
$(u_{0},v_{0})\in{{r}}^{\mathcal{I}^{\prime}}$. By definition of
${{A_{2}}}^{\mathcal{J}}$ and ${{r}}^{\mathcal{J}}$, the element
$v:={\overline{v_{0}}}$ satisfies both $v\in{{A_{2}}}^{\mathcal{J}}$ and
$(u,v)\in{{r}}^{\mathcal{J}}$, that is
$u\in(\exists{{r}}.{A_{2}})^{\mathcal{J}}$.

  * •

${\exists{{r}}.{A_{1}}}\sqsubseteq{A_{2}}$. Let
$u\in(\exists{{r}}.{A_{1}})^{\mathcal{J}}$, that is, there exists
$v\in{{A}}_{1}^{\mathcal{J}}$ with $(u,v)\in{{r}}^{\mathcal{J}}$. By
definition of ${{A}}_{1}^{\mathcal{J}}$ and ${{r}}^{\mathcal{J}}$, there exist
$(u_{0},v_{0})\in{{r}}^{\mathcal{I}^{\prime}}$ and
$v_{1}\in{{A}}_{1}^{\mathcal{I}^{\prime}}$ such that ${\overline{u_{0}}}=u$
and ${\overline{v_{0}}}={\overline{v_{1}}}=v$. Remark 2 ensures $v_{0}$ and
$v_{1}$ satisfy the same concepts, in particular
$u_{0}\in(\exists{{r}}.{A_{1}})^{\mathcal{I}^{\prime}}$. Since
$\mathcal{I}^{\prime}$ is a model, this ensures
$u_{0}\in{{A}}_{2}^{\mathcal{I}^{\prime}}$, yielding by definition of
${{A}}_{2}^{\mathcal{J}}$ that
$u={\overline{u_{0}}}\in{{A}}_{2}^{\mathcal{J}}$.

  * •

${{A}}\sqsubseteq{{\lnot B}}$. By contradiction, assume
$u\in{{A}}^{\mathcal{J}}\cap{{B}}^{\mathcal{J}}$. By definition there exists
$v\in{{A}}^{{\mathcal{I}}^{\prime}}$ and $w\in{{B}}^{{\mathcal{I}}^{\prime}}$
with ${\overline{v}}={\overline{w}}=u$. Remark 2 ensures $v$ and $w$ satisfy
the same concepts, contradicting ${\mathcal{I}}^{\prime}$ being a model.

  * •

${{\lnot B}}\sqsubseteq{{A}}$. Let $u\in{{\lnot B}}^{\mathcal{J}}$. By
definition of $\Delta^{\mathcal{J}}$, there exists
$v\in{\mathcal{I}}^{\prime}$ such that ${\overline{v}}=u$. Since
$u\notin{{B}}^{\mathcal{J}}$, we have
${v}\notin{{B}}^{{\mathcal{I}}^{\prime}}$. Hence ${\mathcal{I}}^{\prime}$
being a model gives ${v}\in{{A}}^{{\mathcal{I}}^{\prime}}$, yielding by
definition $u={\overline{v}}\in{{A}}^{\mathcal{J}}$.

  * •

${p}\sqsubseteq{r}$. Let $(u,v)\in{{p}}^{\mathcal{J}}$. By definition of
${{p}}^{\mathcal{J}}$, there exists
$(u_{0},v_{0})\in{{p}}^{\mathcal{I}^{\prime}}$ such that
${\overline{u_{0}}}=u$ and ${\overline{v_{0}}}=v$. Since
$\mathcal{I}^{\prime}$ is a model, it ensures
$(u_{0},v_{0})\in{{r}}^{\mathcal{I}^{\prime}}$, hence
$({\overline{u_{0}}},{\overline{v_{0}}})=(u,v)\in{{r}}^{\mathcal{J}}$ by
definition of ${{r}}^{\mathcal{J}}$.

It remains to prove that $\mathcal{J}$ is minimal w.r.t. $<_{\sf CP}$. We use
Lemma 2 with $\mathcal{I}$ as reference model, and it suffices to show that
the preconditions of that lemma are satisfied. This is in fact easy based on
Remark 2, following exactly the same lines as the final part of the proof of
Lemma 3.

We now prove $\mathcal{J}\not\models q(\bar{a})$. By contradiction, assume we
have $p\in q$ and a homomorphism $\pi:p\rightarrow\mathcal{J}$ s.t.
$p(\bar{x})=\bar{a}$. Consider the set of variables
${\mathbf{v}}_{\pi}:=\\{v\mid
v\in{\bar{y}},\pi(v)\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}\\}$.
Let $\mathcal{C}$ denote the set of connected components of
${\mathbf{v}}_{\pi}$ in $p_{\mid{\mathbf{v}}_{\pi}}$ (that is the query
obtained by keeping only those atoms containing variables from
${\mathbf{v}}_{\pi}$). For each connected component $C\in\mathcal{C}$, choose
a reference variable $v_{C}\in C$. Since $\pi$ is a homomorphism and
${\left|{C}\right|}\leq{\left|{q}\right|}$, every variable $v\in C$ satisfies
$\pi(v)\in\mathcal{N}_{{\left|{q}\right|}}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}(\pi(v_{C}))$.
Let $d_{C}\in\Delta^{\mathcal{I}^{\prime}}$ denote one’s favorite
representative for the class of $\pi(v_{C})$ (that is
${\overline{d_{C}}}=\pi(v_{C})$). From Lemma 19, we have a homomorphism
$\rho_{C}:\mathcal{N}_{{\left|{q}\right|}}^{\mathcal{J},{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}}(\pi(v_{C}))\rightarrow\mathcal{N}_{{\left|{q}\right|}}^{\mathcal{I}^{\prime},{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}(d_{C})$.
Using these $\rho_{C}$, one per $C\in\mathcal{C}$, we define:

$\begin{array}[]{rcl}\pi^{\prime}:{\bar{x}}\cup{\bar{y}}&\rightarrow&\Delta^{\mathcal{I}^{\prime}}\\\
v&\mapsto&\left\\{\begin{array}[]{ll}\rho_{C}(\pi(v))&\text{ if }v\in
C,C\in\mathcal{C}\\\ e&\text{ if
}\pi(v)={\overline{e}}\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}\end{array}\right.\end{array}$

Since each $\rho_{C}$ is a homomorphism (again Lemma 19), we can check the
overall $\pi^{\prime}$ is also a homomorphism:

  * •

Consider ${{A}}(v)\in q$. If $v\in C$ for some $C\in\mathcal{C}$, then
$\rho_{C}$ being a homomorphism gives
$\pi^{\prime}(v)\in{{A}}^{\mathcal{I}^{\prime}}$. Otherwise
$\pi(v)={\overline{e}}\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$,
but since $\pi$ is a homomorphism we have $\pi(v)\in{{A}}^{\mathcal{J}}$.
Since ${\overline{e}}=\\{e\\}$ and by definition of ${{A}}^{\mathcal{J}}$, it
ensures $e\in{{A}}^{\mathcal{I}^{\prime}}$, that is
$\pi^{\prime}(v)\in{{A}}^{\mathcal{I}^{\prime}}$.

  * •

Consider ${{r}}(u,v)\in q$.

    * –

If both
$\pi(u),\pi(v)\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$, then
we can find $C\in\mathcal{C}$ such that $u,v\in C$, and then we use $\rho_{C}$
being a homomorphism.

    * –

If both $\pi(u),\pi(v)\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$,
then the definition of ${{r}}^{\mathcal{J}}$ provides
$(u_{0},v_{0})\in{{r}}^{\mathcal{I}^{\prime}}$ with
${\overline{u_{0}}}=\pi(u)\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$
and
${\overline{v_{0}}}=\pi(v)\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$.
Hence ${\overline{u_{0}}}=\\{u_{0}\\}$ and ${\overline{v_{0}}}=\\{v_{0}\\}$,
which gives
$(\pi^{\prime}(u),\pi^{\prime}(v))\in{{r}}^{\mathcal{I}^{\prime}}$.

    * –

If $\pi(u)\notin{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$ and
$\pi(v)\in{\overline{{\Delta_{\mathsf{base}}^{\mathcal{I}}}}}$, then we have
$\pi^{\prime}(u)=\rho_{C}(\pi(u))$ for some $C\in\mathcal{C}$. Lemma 19
ensures $\pi^{\prime}(u)\sim_{1}\pi(u)$, and since $\pi$ is a homomorphism, we
also have $(\pi(u),\pi(v))\in{{r}}^{\mathcal{J}}$. Therefore we can apply
Condition 2.(b) and we obtain
$(\pi^{\prime}(u),\pi^{\prime}(v))\in{{r}}^{\mathcal{I}^{\prime}}$.

In particular, $\pi^{\prime}$ is a homomorphism s.t.
$\pi^{\prime}(\bar{x})=\bar{a}$, hence the desired contradiction with
$\mathcal{I}^{\prime}$ being a countermodel.

∎

See 3

###### Proof.

Assume that we are given a circumscribed $\mathcal{ALCHI}$ KB ${\sf Circ_{\sf
CP}}(\mathcal{K})$ with $\mathcal{K}=(\mathcal{T},\mathcal{A})$ and a UCQ $q$.
We describe a $\Sigma^{p}_{2}$ procedure to decide whether ${\sf Circ_{\sf
CP}}(\mathcal{K})\not\models q(\bar{a})$.

We first guess an interpretation $\mathcal{I}$ with
$|\Delta^{\mathcal{I}}|\leq|\mathcal{A}|+(2^{|\mathcal{T}|+2}+1)^{3|q|}$. We
next check in polynomial time that $\mathcal{I}$ is a model of $\mathcal{K}$
and that $\mathcal{I}$ is minimal w.r.t. $<_{{\sf CP}}$ by co-guessing a model
$\mathcal{J}$ of $\mathcal{K}$ with $\mathcal{J}<_{{\sf CP}}\mathcal{I}$. If
one of the checks fails, we reject. Otherwise, for each CQ $p$ in $q$, we
verify whether there is a homomorphism from $p$ to $\mathcal{I}$. This is done
brute-force, in time $O(|\Delta^{\mathcal{I}}|^{|q|})$. We accept if there is
no such homomorphism and reject otherwise. This procedure is correct due to
Lemma 7. ∎

See 4

###### Proof.

We give a polynomial time reduction from $\forall\exists{\sf 3SAT}$ (?), that
is, the problem to decide whether a given $\forall\exists$-3CNF sentence is
true. Thus let $\forall\bar{x}\exists\bar{y}\,\varphi$ be such a sentence
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 ${\cal EL}$ 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 minimizes the concept name ${\mathsf{Min}}$ and
lets all other concept names vary, and the instance query is
$q={\mathsf{Goal}}(c_{0})$. We now describe how to construct the KB
$\mathcal{K}=(\mathcal{T},\mathcal{A})$, not strictly separating $\mathcal{T}$
from $\mathcal{A}$. We first represent $\varphi$ in $\mathcal{A}$ using the
following assertions:

$\displaystyle{\mathsf{Var}}(v)$ $\displaystyle\quad\text{for all
}v\in{\bar{x}}\cup{\bar{y}}$ (18) $\displaystyle{\mathsf{pos}}_{j}(c_{i},v)$
$\displaystyle\quad\text{if }L_{ij}=v$ (19)
$\displaystyle{\mathsf{neg}}_{j}(c_{i},v)$ $\displaystyle\quad\text{if
}L_{ij}=\lnot v$ (20)
$\displaystyle{\mathsf{First}}(c_{0}),{\mathsf{Last}}(c_{\ell})$ (21)
$\displaystyle{\mathsf{next}}(c_{i},c_{i+1})$ $\displaystyle\quad 0\leq
i<\ell$ (22)

We next require each variable to be connected via the role name
${\mathsf{eval}}$ to two instances of ${\mathsf{Min}}$, a “positive” one and a
“negative” one:

$\displaystyle{\mathsf{Var}}$
$\displaystyle\sqsubseteq\,\exists{\mathsf{eval}}.({\mathsf{Min}}\sqcap{\mathsf{Pos}})$
(23) $\displaystyle{\mathsf{Var}}$
$\displaystyle\sqsubseteq\,\exists{\mathsf{eval}}.({\mathsf{Min}}\sqcap{\mathsf{Neg}}).$
(24)

As potential witnesses for the above existential restrictions, we provide
several instances of ${\mathsf{Min}}$, a positive and a negative one for each
truth value:

$\displaystyle{\mathsf{Min}}(t_{+})$ $\displaystyle{\mathsf{Min}}(t_{-})$
$\displaystyle{\mathsf{Min}}(f_{+})$ $\displaystyle{\mathsf{Min}}(f_{-})$ (25)
$\displaystyle{\mathsf{True}}(t_{+})$ $\displaystyle{\mathsf{True}}(t_{-})$
$\displaystyle{\mathsf{False}}(f_{+})$ $\displaystyle{\mathsf{False}}(f_{-})$
(26) $\displaystyle{\mathsf{Pos}}(t_{+})$ $\displaystyle{\mathsf{Neg}}(t_{-})$
$\displaystyle{\mathsf{Pos}}(f_{+})$ $\displaystyle{\mathsf{Neg}}(f_{-})$ (27)

If such an instance is used as a witness, then the respective variable is
assigned the corresponding truth value:

$\displaystyle\exists{\mathsf{eval}}.{\mathsf{True}}$
$\displaystyle\sqsubseteq\,{\mathsf{True}}$ (28)
$\displaystyle\exists{\mathsf{eval}}.{\mathsf{False}}$
$\displaystyle\sqsubseteq\,{\mathsf{False}}$ (29)

We next introduce a mechanism for “freezing” the valuation of the ${\bar{x}}$
variables in the sense that this valuation must be identical in all models
that are smaller w.r.t. ‘$<_{\sf CP}$’. This reflects the fact that the
${\bar{x}}$ variables are chosen prior to the ${\bar{y}}$ variables. Freezing
is achieved by the following:

$\displaystyle{\mathsf{freeze}}_{\mathsf{True}}({x}_{{\mathsf{True}}},x)$
$\displaystyle\quad\text{for all }x\in{\bar{x}}$ (30)
$\displaystyle{\mathsf{freeze}}_{\mathsf{False}}({x}_{{\mathsf{False}}},x)$
$\displaystyle\quad\text{for all }x\in{\bar{x}}$ (31)
$\displaystyle\exists{\mathsf{freeze}}_{\mathsf{True}}.{\mathsf{True}}$
$\displaystyle\sqsubseteq\,{\mathsf{Min}}$ (32)
$\displaystyle\exists{\mathsf{freeze}}_{\mathsf{False}}.{\mathsf{False}}$
$\displaystyle\sqsubseteq\,{\mathsf{Min}}$ (33)

Note that if a variable $x\in\bar{x}$ satisfies ${\mathsf{True}}$, then
${x}_{{\mathsf{True}}}$ must satisfy ${\mathsf{Min}}$, and likewise for
${\mathsf{False}}$. Since ${\mathsf{Min}}$ is minimized, any model that is
smaller w.r.t. ‘$<_{\sf CP}$’ must thus have the same valuation for the
variables in $\bar{x}$.

There is a problem with this approach, though. On the one hand,
${\mathsf{Min}}$ acts as an incentive to use $t_{+}$, $t_{-}$, $f_{+}$, and
$f_{-}$ as witnesses for (23) and (24). On the other hand, freezing implies
that if a variable $x$ does so, then it triggers an instance of
${\mathsf{Min}}$ on ${x}_{{\mathsf{True}}}$ or ${x}_{{\mathsf{False}}}$. There
can hence be models in which fresh instances $e^{+}$ of
${\mathsf{Min}}\sqcap{\mathsf{Pos}}$ and $e^{-}$ of
${\mathsf{Min}}\sqcap{\mathsf{Neg}}$ are created instead, leading to $x$
satisfying neither ${\mathsf{True}}$ nor ${\mathsf{False}}$. Since
${\mathsf{Min}}$ is minimized, however, it must then hold that $e^{+}=e^{-}$,
_i.e._ $x$ is connected to an instance of
${\mathsf{Pos}}\sqcap{\mathsf{Neg}}$. Such models are easily detected due to
our use of positive and negative instances of ${\mathsf{Min}}$. We make sure
that problematic models satisfy the query and are thus ruled out as a
countermodel:

$\displaystyle{\mathsf{checks}}(c_{0},v)$ $\displaystyle\quad\text{for all
}v\in{\bar{x}}\cup{\bar{y}}$ (34)
$\displaystyle\exists{\mathsf{checks}}.(\exists{\mathsf{eval}}.({\mathsf{Pos}}\sqcap{\mathsf{Neg}}))$
$\displaystyle\sqsubseteq\,{\mathsf{Goal}}$ (35)

Now that we can assume that each variable is given a proper truth value, we
encode the evaluation of $\varphi$. The truth value of each clause is
represented by concept name ${\mathsf{True}}$ or ${\mathsf{False}}$ holding on
the corresponding individual $c_{i}$. Let
$X_{i}=\\{\exists{\mathsf{pos}}_{i}.{\mathsf{False}},\exists{\mathsf{neg}}_{i}.{\mathsf{True}}\\}$
and $X=X_{1}\times X_{2}\times X_{3}$, and add:

$\displaystyle\exists{\mathsf{pos}}_{i}.{\mathsf{True}}$
$\displaystyle\sqsubseteq\,{\mathsf{True}}\quad\text{for }1\leq i\leq 3$ (36)
$\displaystyle\exists{\mathsf{neg}}_{i}.{\mathsf{False}}$
$\displaystyle\sqsubseteq\,{\mathsf{True}}\quad\text{for }1\leq i\leq 3$ (37)
$\displaystyle C_{1}\sqcap C_{2}\sqcap C_{3}$
$\displaystyle\sqsubseteq\,{\mathsf{False}}\quad\text{for all
}(C_{1},C_{2},C_{3})\in X$ (38)

We next determine the truth value of $\varphi$ by walking along the
${\mathsf{next}}$-chain of clauses in $\mathcal{A}$. If the formula evaluates
to true, then we make ${\mathsf{Goal}}$ true at $c_{0}$ and thus satisfy the
query. If it evaluates to false, we make ${\mathsf{Min}}$ true at $c_{0}$.
This reflects the existential quantification over the variables $\bar{y}$:
when they exist, we prefer valuations that make $\varphi$ true since making
$\varphi$ false gives us an additional instance of the minimized concept name.
Formally:

$\displaystyle\exists{\mathsf{next}}.({\mathsf{Last}}\sqcap{\mathsf{True}})$
$\displaystyle\sqsubseteq\,{\mathsf{Last}}$ (39)
$\displaystyle{\mathsf{First}}\sqcap{\mathsf{Last}}$
$\displaystyle\sqsubseteq\,{\mathsf{Goal}}$ (40)
$\displaystyle\exists{\mathsf{next}}.{\mathsf{False}}$
$\displaystyle\sqsubseteq\,{\mathsf{False}}$ (41)
$\displaystyle{\mathsf{False}}\sqcap{\mathsf{First}}$
$\displaystyle\sqsubseteq\,{\mathsf{Min}}$ (42)

It remains to solve another technical issue. As explained above, we make
${\mathsf{Min}}$ true not only at the individuals $t_{+},t_{-},f_{+},f_{-}$,
but also at some individuals ${x}_{{\mathsf{True}}},{x}_{{\mathsf{False}}}$
and possibly at $c_{0}$. However, we do not want these individuals to be used
as witnesses for (23) and (24) as then there could be variables that do not
receive a truth value. We can again detect this and then make ${\mathsf{Min}}$
true at a fresh individual $a$:

$\displaystyle{\mathsf{checks}}(a,{x}_{{\mathsf{True}}}),{\mathsf{checks}}(a,{x}_{{\mathsf{False}}})$
$\displaystyle\quad\text{for all }x\in{\bar{x}}$ (43)
$\displaystyle{\mathsf{checks}}(a,c_{0})$ (44)
$\displaystyle\exists{\mathsf{checks}}.{\mathsf{Pos}}$
$\displaystyle\sqsubseteq\,{\mathsf{Min}}$ (45)
$\displaystyle\exists{\mathsf{checks}}.{\mathsf{Neg}}$
$\displaystyle\sqsubseteq\,{\mathsf{Min}}.$ (46)

We now set $\mathcal{K}=(\mathcal{T},\mathcal{A})$ with $\mathcal{T}$ and
$\mathcal{A}$ as defined above. It is easily verified that $\mathcal{T}$ does
not depend on the instance of $\forall\exists{\sf 3SAT}$. It remains to prove
the following claim:
Claim. ${\sf Circ_{\sf CP}}(\mathcal{K})\models{\mathsf{Goal}}(c_{0})$ iff
$\forall{\bar{x}}\,\exists{\bar{y}}\,\varphi({\bar{x}},{\bar{y}})$.
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

$\begin{array}[]{rcl}A^{\mathcal{I}_{V}}&=&\\{a\mid
A(a)\in\mathcal{A}\\}\\\\[2.84526pt] r^{\mathcal{I}_{V}}&=&\\{(a,b)\mid
r(a,b)\in\mathcal{A}\\}\end{array}$

for all concept names
$A\in\\{{\mathsf{Var}},{\mathsf{First}},{\mathsf{Pos}},{\mathsf{Neg}}\\}$ and
all role names

$r\in\\{{\mathsf{pos}}_{i},{\mathsf{neg}}_{i},{\mathsf{next}},{\mathsf{freeze}}_{\mathsf{True}},{\mathsf{freeze}}_{\mathsf{False}},{\mathsf{checks}}\\}.$

We interpret ${\mathsf{eval}}$ according to $V$, that is

$\begin{array}[]{r@{\;}c@{\;}l}{\mathsf{eval}}^{\mathcal{I}_{V}}&=&\\{(v,t_{+}),(v,t_{-})\mid
v\in\bar{x}\cup\bar{y}\text{ and }V(v)=1\\}\,\cup\\\\[2.84526pt]
&&\\{(v,f_{+}),(v,f_{-})\mid v\in\bar{x}\cup\bar{y}\text{ and
}V(v)=0\\}.\end{array}$

The valuation $V$ also assigns a truth value to each clause, let $V(c_{i})$
denote the value of the $i^{th}$ clause. Put

$\begin{array}[]{rcl}{\mathsf{True}}^{\mathcal{I}_{V}}&=&\\{t_{+},t_{-}\\}\,\cup\\\\[2.84526pt]
&&\\{v\mid v\in\bar{x}\cup\bar{y}\text{ and }V(v)=1\\}\,\cup\\\\[2.84526pt]
&&\\{c_{i}\mid 1\leq i\leq\ell\text{ and }V(c_{i})=1\\}\\\\[2.84526pt]
{\mathsf{False}}^{\mathcal{I}_{V}}&=&\\{f_{+},f_{-}\\}\,\cup\\\\[2.84526pt]
&&\\{v\mid v\in\bar{x}\cup\bar{y}\text{ and }V(v)=0\\}\,\cup\\\\[2.84526pt]
&&\\{c_{i}\mid 1\leq i\leq\ell\text{ and }V(c_{i})=1\\}.\end{array}$

Let $q$ be largest such that valuation $V$ makes the last $q$ of the $\ell$
clauses in $\varphi$ true. Put

${\mathsf{Last}}^{\mathcal{I}_{V}}=\\{c_{\ell}\\}\cup\\{c_{\ell-1},\dots,c_{\ell-q+1}\\}.$

It remains to interpret ${\mathsf{Min}}$ and ${\mathsf{Goal}}$. As an
abbreviation, set

$\begin{array}[]{rcl}M&=&\\{t_{+},t_{-},f_{+},f_{-},\\}\,\cup\\\\[2.84526pt]
&&\\{{x}_{{\mathsf{True}}}\mid x\in\bar{x}\text{ and }V(x)=1\\}\\\\[2.84526pt]
&&\\{{x}_{{\mathsf{False}}}\mid x\in\bar{x}\text{ and }V(x)=0\\}.\end{array}$

Now if $V$ satisfies all clauses in $\varphi$, then put

$\begin{array}[]{rcl}{\mathsf{Min}}^{\mathcal{I}_{V}}&=&M\\\\[2.84526pt]
{\mathsf{Goal}}^{\mathcal{I}_{V}}&=&\\{c_{0}\\}\end{array}$

and otherwise put

$\begin{array}[]{rcl}{\mathsf{Min}}^{\mathcal{I}_{V}}&=&M\cup\\{c_{0}\\}\\\\[2.84526pt]
{\mathsf{Goal}}^{\mathcal{I}_{V}}&=&\emptyset.\end{array}$

It is straightforward to verify that $\mathcal{I}_{V}$ is indeed a model of
$\mathcal{K}$. Moreover, $\mathcal{I}_{V}\models q$ if and only if $V$
satisfies all clauses in $\varphi$. 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}$. Then the interpretation $\mathcal{I}_{V}$ is a
model of $\mathcal{K}$ with $\mathcal{I}_{V}\not\models q$, to show that ${\sf
Circ_{\sf CP}}(\mathcal{K})\not\models q$ 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}$. Then

$\begin{array}[]{rcl}{\mathsf{Min}}^{\mathcal{J}}\subsetneq{\mathsf{Min}}^{\mathcal{I}_{v}}&=&\\{t_{+},t_{-},f_{+},f_{-},c_{0}\\}\,\cup\\\\[2.84526pt]
&&\\{{x}_{{\mathsf{True}}}\mid x\in\bar{x}\text{ and }V(x)=1\\}\\\\[2.84526pt]
&&\\{{x}_{{\mathsf{False}}}\mid x\in\bar{x}\text{ and }V(x)=0\\}.\end{array}$

$\mathcal{J}$ being a model of $\mathcal{A}$ implies
$\\{t_{+},t_{-},f_{+},f_{-}\\}\subseteq{\mathsf{Min}}^{\mathcal{J}}$.

Since $\mathcal{J}$ satisfies (18), (23) and (24), we can choose for each
$v\in{\bar{x}}\cup{\bar{y}}$ an element
$v^{+}\in{\mathsf{Pos}}^{\mathcal{J}}\cap{\mathsf{Min}}^{\mathcal{J}}$ such
that $(v,v^{+})\in{\mathsf{eval}}^{\mathcal{J}}$. Since $\mathcal{J}$
satisfies (43) to (46) and $a\notin{\mathsf{Min}}^{\mathcal{J}}$, we must have
$v^{+}\in\\{t_{+},t_{-},f_{+},f_{-}\\}$. From (28) and (29), it follows that
$v\in{\mathsf{True}}^{\mathcal{J}}\cup{\mathsf{False}}^{\mathcal{J}}$. Let
$V_{\mathcal{J}}$ be the valuation defined by setting, for all
$v\in\bar{x}\cup\bar{y}$:

$V_{\mathcal{J}}(v)=\left\\{\begin{array}[]{ll}1&\text{ if
}v\in{\mathsf{True}}^{\mathcal{J}}\\\\[2.84526pt] 0&\text{
otherwise.}\end{array}\right.$

From (30) to (33), we further obtain that

$\begin{array}[]{rcl}{\mathsf{Min}}^{\mathcal{J}}&\supseteq&\\{{x}_{{\mathsf{True}}}\mid
x\in\bar{x}\text{ and }V_{\mathcal{J}}(x)=1\\}\\\\[2.84526pt]
&&\\{{x}_{{\mathsf{False}}}\mid x\in\bar{x}\text{ and
}V_{\mathcal{J}}(x)=0\\}.\end{array}$

which implies that
${\mathsf{Min}}^{\mathcal{I}_{V}}\setminus{\mathsf{Min}}^{\mathcal{J}}=\\{c_{0}\\}$
and, through $\mathcal{J}<_{\sf CP}\mathcal{I}$, that $V$ and
$V_{\mathcal{J}}$ agree on $\bar{x}$. From
$\forall\bar{y}\,\lnot\varphi^{\prime}$, it follows that
$V_{\mathcal{J}}\not\models\varphi$ and thus the soundness of the evaluation
of $\varphi$ implemented by (36) to (42) yields
$c_{0}\in{\mathsf{Min}}^{\mathcal{J}}$, 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$.

Since $\mathcal{I}$ satisfies (18), (23) and (24), we can choose for every
$v\in{\bar{x}}\cup{\bar{y}}$ two elements
$v^{+}\in{\mathsf{Pos}}^{\mathcal{I}}\cap{\mathsf{Min}}^{\mathcal{I}}$ and
$v^{-}\in{\mathsf{Neg}}^{\mathcal{I}}\cap{\mathsf{Min}}^{\mathcal{I}}$ such
that $(v,v^{+}),(v,v^{-})\in{\mathsf{eval}}^{\mathcal{I}}$. If $v^{+}=v^{-}$
for some $v$, then by (34) and (35) we have
$c_{0}\in{\mathsf{Goal}}^{\mathcal{I}}$, thus $\mathcal{I}\models q$ and we
are done. For the remaining proof, we may thus assume $v^{+}\neq v^{-}$ for
all $v\in{\bar{x}}\cup{\bar{y}}$.

We next argue that for all $v\in\bar{x}\cup\bar{y}$,

$\\{v^{+},v^{-}\\}\cap\\{t_{+},t_{-},f_{+},f_{-}\\}\neq\emptyset$ ($\ast$)

Assume to the contrary that ($*$) is violated by some
$v_{0}\in\bar{x}\cup\bar{y}$, that is,
$v_{0}^{+},v_{0}^{-}\notin\\{t_{+},t_{-},f_{+},f_{-}\\}$. Then we can find a
model $\mathcal{J}<_{\sf CP}\mathcal{I}$ of $\mathcal{K}$, contradicting the
minimality of $\mathcal{I}$. We distinguish two cases:

  1. 1.

$a\in{\mathsf{Min}}^{\mathcal{I}}$.

We construct $\mathcal{J}$ by choosing $\Delta^{\mathcal{J}}={\sf
ind}(\mathcal{A})$ and interpreting the concept names ${\mathsf{Var}}$ and
${\mathsf{First}}$ as well as the role names
${\mathsf{pos}}_{i},{\mathsf{neg}}_{i},{\mathsf{next}},{\mathsf{freeze}}_{\mathsf{True}},{\mathsf{freeze}}_{\mathsf{False}},{\mathsf{checks}}$
as in the initially defined interpretations $\mathcal{I}_{V}$—note that this
is independent of $V$. We further set

$\begin{array}[]{rcl}{\mathsf{eval}}^{\mathcal{J}}&=&\\{(v,a)\mid
v\in\bar{x}\cup\bar{y}\\}\\\\[2.84526pt]
{\mathsf{Pos}}^{\mathcal{J}}&=&\\{t_{+},f_{+},a\\}\\\\[2.84526pt]
{\mathsf{Neg}}^{\mathcal{J}}&=&\\{t_{-},f_{-},a\\}\\\\[2.84526pt]
{\mathsf{True}}^{\mathcal{J}}&=&\\{t_{+},t_{-}\\}\\\\[2.84526pt]
{\mathsf{False}}^{\mathcal{J}}&=&\\{f_{+},f_{-}\\}\\\\[2.84526pt]
{\mathsf{Last}}^{\mathcal{J}}&=&\\{c_{\ell}\\}\\\\[2.84526pt]
{\mathsf{Min}}^{\mathcal{J}}&=&\\{t_{+},t_{-},f_{+},f_{-},a\\}\\\\[2.84526pt]
{\mathsf{Goal}}^{\mathcal{J}}&=&\emptyset.\end{array}$

It can be verified that $\mathcal{J}$ is a model of $\mathcal{K}$. Moreover,
at least one of the (distinct!) $v_{0}^{+},v_{0}^{-}$ is not in
${\mathsf{Min}}^{\mathcal{J}}$ and thus
${\mathsf{Min}}^{\mathcal{J}}\subsetneq{\mathsf{Min}}^{\mathcal{I}}$ and
$\mathcal{J}<_{\sf CP}\mathcal{I}$.

  2. 2.

$a\notin{\mathsf{Min}}^{\mathcal{I}}$.

We construct $\mathcal{J}$ exactly as in Case 1, but with $a$ replaced by
$v^{+}_{0}$ in ${\mathsf{Pos}}^{\mathcal{J}}$, ${\mathsf{Neg}}^{\mathcal{J}}$,
and ${\mathsf{Min}}^{\mathcal{J}}$.

We have thus established $(*)$.

It follows from $(*)$ together with (26), (28), and (29) that
$v\in{\mathsf{True}}^{\mathcal{J}}\cup{\mathsf{False}}^{\mathcal{J}}$ for all
$v\in\bar{x}\cup\bar{y}$ and thus we find a valuation $V$ such that $V(v)=1$
implies $v\in{\mathsf{True}}^{\mathcal{J}}$ and $V(v)=0$ implies
$v\in{\mathsf{False}}^{\mathcal{J}}$ for all $v$. We show below that
$V\models\varphi$. Then the soundness of the evaluation of $\varphi$
implemented by (36) to (42) yields $c_{0}\in{\mathsf{Goal}}^{\mathcal{I}}$ and
thus $\mathcal{I}\models q$ as desired.

Assume to the contrary of what remains to be shown that $V\not\models\varphi$.
Soundness of evaluation ensures $c_{0}\in{\mathsf{Min}}^{\mathcal{I}}$. Since
$\forall{\bar{x}}\,\exists{\bar{y}}\,\varphi({\bar{x}},{\bar{y}})$ is true, we
find a valuation $V^{\prime}$ that agrees with $V$ on the variables in
$\bar{x}$ and that satisfies $\varphi$. Now consider the model
$\mathcal{I}_{V^{\prime}}$ of $\mathcal{K}$. It satisfies

$\begin{array}[]{rcl}{\mathsf{Min}}^{\mathcal{I}_{V^{\prime}}}&=&\\{t_{+},t_{-},f_{+},f_{-},\\}\,\cup\\\\[2.84526pt]
&&\\{{x}_{{\mathsf{True}}}\mid x\in\bar{x}\text{ and }V(x)=1\\}\\\\[2.84526pt]
&&\\{{x}_{{\mathsf{False}}}\mid x\in\bar{x}\text{ and }V(x)=0\\}.\end{array}$

and it is easy to verify that
${\mathsf{Min}}^{\mathcal{I}_{V^{\prime}}}\subseteq{\mathsf{Min}}^{\mathcal{I}}$.
But then $\mathcal{I}_{V^{\prime}}<\mathcal{I}_{V}$ since
$c_{0}\in{\mathsf{Min}}^{\mathcal{I}}$. ∎

##  Appendix D Proofs for Section 4.1

See 5

###### Proof.

We reduce from (Boolean) UCQ evaluation on $\textrm{DL-Lite}^{\cal H}$ KBs
with closed concept names, which is defined in the expected way and known to
be 2Exp-hard (?). Let $\mathcal{K}_{\Sigma}$ be a $\textrm{DL-Lite}^{\cal H}$
KB with closed concept names, $\mathcal{K}=(\mathcal{T},\mathcal{A})$, and let
$q$ be a Boolean UCQ. We construct a circumscribed $\textrm{DL-Lite}^{\cal H}$
KB ${\sf Circ}_{\sf CP}(\mathcal{K}^{\prime})$, with
$\mathcal{K}^{\prime}=(\mathcal{T}^{\prime},\mathcal{A}^{\prime})$, and a CQ
$q^{\prime}$ such that $\mathcal{K}_{\Sigma}\models q$ iff ${\sf Circ}_{\sf
CP}(\mathcal{K}^{\prime})\models q^{\prime}$.

As in the proof of Theorem 2, we minimize only a single concept name $M$ and
include $\mathcal{A}$ in $\mathcal{A}^{\prime}$. To construct
$\mathcal{T}^{\prime}$, we start from $\mathcal{T}$ and extend with additional
concept inclusions. For $q^{\prime}$, we start from $q$ and extend with
additional disjuncts. We will actually use individuals $a\in{\sf
Ind}(\mathcal{A})$ as constants in $q^{\prime}$. These can be eliminated by
introducing a fresh concept name $A_{a}$, extending $\mathcal{A}$ with
$A_{a}(a)$, and replacing in each CQ in $q^{\prime}$ the constant $a$ with a
fresh variable $x_{a}$ and adding the atom $A_{a}(x_{a})$.

As in the proof of Theorem 2, we include in $\mathcal{T}^{\prime}$ the CI

$\displaystyle A\sqsubseteq M$ $\displaystyle\quad\text{for all }A\in\Sigma$
(47)

and then have to rule out non-asserted instances of closed concept names. To
rule out non-asserted instances inside of ${\sf ind}(\mathcal{A})$, we add to
$q^{\prime}$ the disjunct $A(a)$ for all $A\in\Sigma$ and $a\in{\sf
ind}(\mathcal{A})$ with $A(a)\notin\mathcal{A}$.

To rule out instances of closed concept names outside of ${\sf
ind}(\mathcal{A})$, add

$\displaystyle M(t)$ (48)

where $t$ is a fresh individual. As in the proof of Theorem 2, this guarantees
that models with instances of closed concept names outside of ${\sf
ind}(\mathcal{A})$ are not minimal. To ensure that no closed concept names are
made true at $t$, we extend $q^{\prime}$ with the disjunct $r(x,t)$ for every
role name $r$ used in $\mathcal{T}$.
Claim. $\mathcal{K}_{\Sigma}\models q$ iff ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})\models q^{\prime}$.
The proof is rather straightforward; we omit the details. ∎

We now work towards a proof of Theorem 6, first establishing the following.
See 8

Refining the unraveling begins by noticing the set $\Omega$ now only contains
elements with shape $r\top$ as $\textrm{DL-Lite}_{\sf bool}$ TBoxes are
considered. We drop the $\top$ concept for simplicity. Recall that we assume
chosen a representative $e_{t}\in\Delta^{\mathcal{I}}$ for each non-core type
$t\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$. We define the set
$\mathcal{P}_{\mathsf{bool}}$ of $\mathsf{bool}$-paths through $\mathcal{I}$
along with a mapping $h$ that assigns to each
$p\in\mathcal{P}_{\mathsf{bool}}$ an element of $\Delta^{\mathcal{I}}$:

  * •

each element $d$ of the set

$\Delta_{\mathsf{base}}^{\mathcal{I}}:={\sf
ind}(\mathcal{A})\cup\Delta_{\mathsf{core}}^{\mathcal{I}}\cup\\{e_{t}\mid
t\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})\\}.$

is a path in $\mathcal{P}_{\mathsf{bool}}$ and $h(d)=d$;

  * •

if $p\in\mathcal{P}_{\mathsf{bool}}$ with $h(p)=d$ and $r\in\Omega$ such that:

    1. (a)

$f(d,r)$ is defined and not from $\Delta^{\mathcal{I}}_{{\sf core}}$ and

    2. (b)

$p$ does not end by $r^{-}$, which we denote ${\sf tail}(p)\neq r^{-}$.

then $p^{\prime}=pr$ is a path in $\mathcal{P}_{\mathsf{bool}}$ and
$h(p^{\prime})=f(d,r)$.

For every role $r$, define

$\begin{array}[]{@{}r@{\;}c@{\;}l}R_{r}&=&\\{(a,b)\mid a,b\in{\sf
ind}(\mathcal{A}),\mathcal{K}\models r(a,b)\\}\,\cup\\\\[2.84526pt]
&&\\{(d,e)\mid d,e\in\Delta_{\mathsf{core}}^{\mathcal{I}},(d,e)\in
r^{\mathcal{I}}\\}\,\cup\\\\[2.84526pt] &&\\{(p,p^{\prime})\mid
p^{\prime}=pr\\}\,\cup\\\\[2.84526pt] &&\\{(p,e)\mid
e=f(h(p),r)\in\Delta^{\mathcal{I}}_{{\sf core}},{\sf tail}(p)\neq
r^{-}\\}.\end{array}$

Now the $\mathsf{bool}$-unraveling of $\mathcal{I}$ is defined by setting

$\begin{array}[]{r@{\;}c@{\;}l}\Delta^{\mathcal{I}^{\prime}}&=&\mathcal{P}_{\mathsf{bool}}\\\\[2.84526pt]
A^{\mathcal{I}^{\prime}}&=&\\{p\in\mathcal{P}_{\mathsf{bool}}\mid h(p)\in
A^{\mathcal{I}}\\}\\\\[2.84526pt] r^{\mathcal{I}^{\prime}}&=&\displaystyle
R_{r}\cup\\{(e,d)\mid(d,e)\in R_{r^{-}}\\}\end{array}$

for all concept names $A$ and role names $r$. It is easy to verify that $h$ is
a homomorphism from $\mathcal{I}^{\prime}$ to $\mathcal{I}$. It is a
technicality to verify that $\mathcal{I}^{\prime}_{\mathsf{bool}}$ satisfies
the same properties as the previous unraveling ${\mathcal{I}}^{\prime}$, that
is: if $\mathcal{I}$ is a countermodel for $q$ over ${\sf Circ_{\sf
CP}}(\mathcal{K})$, then so is $\mathcal{I}^{\prime}_{\mathsf{bool}}$. The key
additional property satisfied by $\mathcal{I}^{\prime}_{\mathsf{bool}}$ is the
following:

######  Lemma 20.

For any ${{r}}\in\mathsf{N_{R}}$ and
$d_{1}\in\Delta^{\mathcal{I}^{\prime}_{\mathsf{bool}}}\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$,
there is at most one element
$d_{2}\in\Delta^{\mathcal{I}^{\prime}_{\mathsf{bool}}}$ such that
$(d_{1},d_{2})\in{{r}}^{\mathcal{I}^{\prime}_{\mathsf{bool}}}$.

###### Proof.

Unfolding the definition of ${{r}}^{\mathcal{I}^{\prime}_{\mathsf{bool}}}$ and
recalling $d_{1}\notin\Delta_{\mathsf{base}}^{\mathcal{I}}$, we obtain that if
$d_{1}\in\Delta^{\mathcal{I}^{\prime}_{\mathsf{bool}}}\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$
and $(d_{1},d_{2})\in{{r}}^{\mathcal{I}^{\prime}_{\mathsf{bool}}}$, then
either:

  * •

$(d_{1},d_{2})\in R_{r}$ and either $d_{2}=d_{1}r$ (Case 1) or
$d_{2}=f(h(d_{1}),r)\in\Delta_{\mathsf{base}}^{\mathcal{I}}$ and ${\sf
tail}(d_{1})\neq r^{-}$ (Case 2).

  * •

$(d_{2},d_{1})\in R_{r^{-}}$ and we have $d_{1}=d_{2}r^{-}$ (Case 3).

To verify uniqueness, let us assume there exist $d_{2}$ and $d_{2}^{\prime}$
s.t.
$(d_{1},d_{2}^{\prime}),(d_{1},d_{2}^{\prime})\in{{r}}^{\mathcal{I}^{\prime}_{\mathsf{bool}}}$.
We want to prove $d_{2}=d_{2}^{\prime}$. From the small analysis above, there
are $3\times 3$ cases to consider:

  1. 1.

if $d_{2}=d_{1}r$, then:

    1. 1.

if $d_{2}^{\prime}=d_{1}r$, we obtain directly $d_{2}^{\prime}=d_{2}$.

    2. 2.

if $d_{2}^{\prime}=f(h(d_{1}),r)\in\Delta_{\mathsf{base}}^{\mathcal{I}}$ and
${\sf tail}(d_{1})\neq r^{-}$, then it contradicts
$d_{1}r\in\mathcal{P}_{\mathsf{bool}}$ (Condition (a)).

    3. 3.

if $d_{1}=d_{2}^{\prime}r^{-}$, then $d_{2}=d_{2}^{\prime}r^{-}r$, which
contradicts $d_{2}\in\mathcal{P}_{\mathsf{bool}}$ (Condition (b)).

  2. 2.

if $d_{2}=f(h(d_{1}),r)\in\Delta_{\mathsf{base}}^{\mathcal{I}}$ and ${\sf
tail}(d_{1})\neq r^{-}$, then:

    1. 1.

if $d_{2}^{\prime}=d_{1}r$, then same argument as 1.2.

    2. 2.

if $d_{2}^{\prime}=f(h(d_{1}),r)\in\Delta_{\mathsf{base}}^{\mathcal{I}}$ and
${\sf tail}(d_{1})\neq r^{-}$, then $d_{2}^{\prime}=d_{2}$ from $h$ and $f$
being functions.

    3. 3.

if $d_{1}=d_{2}^{\prime}r^{-}$, then it contradicts ${\sf tail}(d_{1})\neq
r^{-}$.

  3. 3.

if $d_{1}=d_{2}r^{-}$, then:

    1. 1.

if $d_{2}^{\prime}=d_{1}r$, then same argument as 1.3.

    2. 2.

if $d_{2}^{\prime}=f(h(d_{1}),r)\in\Delta_{\mathsf{base}}^{\mathcal{I}}$ and
${\sf tail}(d_{1})\neq r^{-}$, then same argument as 2.3.

    3. 3.

if $d_{1}=d_{2}^{\prime}r^{-}$, we obtain directly $d_{2}^{\prime}=d_{2}$.

∎

Repeated applications of Lemma 20 ensure that each partial homomorphism of a
CQ $p\in q$ in the non-$\Delta_{\mathsf{base}}^{\mathcal{I}}$ part of the
bool-unraveling can be completed uniquely in a maximal such partial
homomorphism (see further Lemma 21). This motivates a refined notion of the
neighborhood of an element $d$, restricting the (usual) neighborhood to those
elements $e$ that can be reached by a homomorphism of some connected subquery
involving both $d$ and $e$. Formally, for $n\geq 0$ and
$\Delta\subseteq\Delta^{\mathcal{I}}$, we use
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I},\Delta}(d)$ to denote the _$n$
-bool-neighborhood of $d$ in $\mathcal{I}$ up to_ $\Delta$, that is, the set
of all elements $e\in\mathcal{N}_{n}^{\mathcal{I},\Delta}(d)$ such that there
exists a connected subquery $p^{\prime}\subseteq p$ for some $p\in q$ and a
homomorphism
$\pi:p^{\prime}\rightarrow\mathcal{N}_{n}^{\mathcal{I},\Delta}(d)$ s.t.
$d,e\in\pi(\mathsf{var}(p^{\prime}))$.

The following polynomial bound on their size in the bool-unraveling is the
central property allowing bool-neighborhoods to improve our construction.

######  Lemma 21.

Let $\mathcal{I}$ be a model of $\mathcal{K}$ and
$\mathcal{I}^{\prime}_{\mathsf{bool}}$ its bool-unraveling. Consider
$d\in\Delta^{\mathcal{I}^{\prime}_{\mathsf{bool}}}\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$,
then
${\left|{\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(d)}\right|}\leq{\left|{q}\right|}^{2}({\left|{\mathcal{T}}\right|}+1)$.

###### Proof.

Let
$c\in\Delta^{\mathcal{I}^{\prime}_{\mathsf{bool}}}\setminus\Delta^{\mathcal{I}_{\mathsf{base}}}$
in a first step, we prove the number of elements in
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta^{\mathcal{I}_{\mathsf{base}}}}(c)\setminus\Delta^{\mathcal{I}_{\mathsf{base}}}$
is at most ${\left|{q}\right|}^{2}$. In a second step, we notice each element
$e\in\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta^{\mathcal{I}_{\mathsf{base}}}}(c)\cap\Delta^{\mathcal{I}_{\mathsf{base}}}$
must be connected to an element
$d\in\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta^{\mathcal{I}_{\mathsf{base}}}}(c)\setminus\Delta^{\mathcal{I}_{\mathsf{base}}}$
by construction of (usual) neighborhoods. However, from Lemma 20, each such
element $d$ is connected to at most ${\left|{\mathcal{T}}\right|}$ elements.
From the first step it follows there are at most
${\left|{q}\right|}^{2}\cdot{\left|{\mathcal{T}}\right|}$ elements in
$e\in\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta^{\mathcal{I}_{\mathsf{base}}}}(c)\cap\Delta^{\mathcal{I}_{\mathsf{base}}}$,
hence the claimed bound.

It remains to prove the first step. We start by proving that if the connected
subquery $p^{\prime}\subseteq p$ for some $p\in q$ and the variable $v_{0}$
that shall map on $c$ are fixed, then all homomorphisms
$p^{\prime}\rightarrow{(\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\,\setminus\,\Delta_{\mathsf{base}}^{\mathcal{I}})}$
mapping $v_{0}$ on $c$ are equal. Consider two such homomorphisms $\pi_{1}$
and $\pi_{2}$. We proceed by induction on the variables $v$ of $p^{\prime}$
being connected. For $v=v_{0}$, we have $\pi_{1}(v_{0})=\pi_{2}(v_{0})$ by
definition. For a further term $v$, we use the induction hypothesis, that is,
the existence of an atom ${{r}}(v^{\prime},v)\in p^{\prime}$ (or the other way
around) such that $\pi_{1}(v^{\prime})=\pi_{2}(v^{\prime})$. Recall $\pi_{1}$
and $\pi_{2}$ are homomorphisms of $p^{\prime}$ in
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\,\setminus\,\Delta_{\mathsf{base}}^{\mathcal{I}}$,
in particular
$\pi_{1}(v^{\prime}),\pi_{2}(v^{\prime})\notin\Delta_{\mathsf{base}}^{\mathcal{I}}$,
hence we can apply Lemma 20, yielding $\pi_{1}(v)=\pi_{2}(v)$.

This proves that, for a fixed $v_{0}\in\mathsf{var}(p)$, each connected
subquery $p^{\prime}\subseteq p$ admitting a homomorphism in
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\,\setminus\,\Delta_{\mathsf{base}}^{\mathcal{I}}$
defines at most ${\left|{p}\right|}$ new neighbors, but also that if
$p^{\prime}\subseteq p^{\prime\prime}\subseteq p$ are two such subqueries,
then the neighbors defined by $p^{\prime}$ are subsumed by those defined by
$p^{\prime\prime}$ (the restriction to the variables of $p^{\prime}$ of the
unique homomorphism of $p^{\prime\prime}$ mapping $v_{0}$ on $c$ must coincide
with the unique homomorphism of $p^{\prime}$ mapping $v_{0}$ on $c$). Still,
for a fixed $v_{0}$, consider now two connected subqueries
$p_{1},p_{2}\subseteq p$, each admitting a (unique) homomorphism $\pi_{1}$
resp. $\pi_{2}$, to
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\,\setminus\,\Delta_{\mathsf{base}}^{\mathcal{I}}$
mapping $v_{0}$ to $c$, and each maximal, w.r.t. the inclusion, for this
property. By the previous property, we know $\pi_{1}$ and $\pi_{2}$ coincide
on $\mathsf{var}(p_{1})\cap\mathsf{var}(p_{2})$. Therefore, $p_{1}\cup p_{2}$
admits a homomorphism to
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\,\setminus\,\Delta_{\mathsf{base}}^{\mathcal{I}}$
mapping $v_{0}$ to $c$, being $\pi_{1}\cup\pi_{2}$. However, since $p_{1}$ and
$p_{2}$ are assumed maximal for this property, we must have $p_{1}=p_{2}$.

Therefore, for a fixed $v_{0}\in\mathsf{var}(p)$, there is a unique maximal
connected subquery $p_{\textsf{max}}\subseteq p$ admitting a homomorphism in
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\,\setminus\,\Delta_{\mathsf{base}}^{\mathcal{I}}$
and mapping $v_{0}$ to $c$. As previously seen, the neighbors defined by
$p_{\textsf{max}}$ subsume those defined by other subqueries of $p$, and since
the homomorphism for $p_{\textsf{max}}$ is unique, it defines at most
${\left|{p}\right|}$ neighbors. This holds for each possible choices of term
$v_{0}$, hence a total number of possible neighbors issued by $p$ bounded by
${\left|{p}\right|}^{2}$. Iterating over each $p\in q$, we hence obtain the
claimed bound of at most ${\left|{q}\right|}^{2}$ elements in
$\mathcal{N}_{n,\mathsf{bool}}^{\mathcal{I}^{\prime}_{\mathsf{bool}},\Delta_{\mathsf{base}}^{\mathcal{I}}}(c)\,\setminus\,\Delta_{\mathsf{base}}^{\mathcal{I}}$.
∎

Using bool-neighborhoods in the quotient construction presented in Section
3.3, the number of equivalence classes drops, which yieldings Lemma 8.

######  Lemma 22.

For all $\mathcal{P}\subseteq\Delta^{\mathcal{I}}$,
$\mathcal{I}_{\mathcal{P}}$ is a model of $\mathcal{K}$.

###### Proof.

Let $\mathcal{P}\subseteq\Delta^{\mathcal{I}}$, we have:

  * •

$\mathcal{I}_{\mathcal{P}}$ models $\mathcal{A}$ as it inherits
interpretations of concepts and roles on ${\sf ind}(\mathcal{A})$ 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}}$ having some $r$-edge
already has one in $\mathcal{I}$ (and interpretations of concept names are
preserved).

  * •

Role inclusions $r\sqsubseteq s$ are satisfied on ${\sf
ind}(\mathcal{A})\times{\sf ind}(\mathcal{A})$ from $\mathcal{I}$ being a
model of $\mathcal{T}$ in the first place, otherwise directly from the
definition of $s^{\mathcal{I}_{\mathcal{P}}}$.

This proves $\mathcal{I}_{\mathcal{P}}\models\mathcal{K}$ as desired. ∎

See 9 To piece together the $\mathcal{J}_{e}$ and reconstruct an eventual
$\mathcal{J}$, we first prove the following property:

######  Lemma 23.

Let $\mathcal{P}_{1},\mathcal{P}_{2}\subseteq\Delta^{\mathcal{I}}$ and
$\mathcal{J}_{1}$, $\mathcal{J}_{2}$ two models of $\mathcal{K}$ s.t.
$\mathcal{J}_{1}<_{\sf CP}\mathcal{I}_{\mathcal{P}_{1}}$ and
$\mathcal{J}_{2}<_{\sf CP}\mathcal{I}_{\mathcal{P}_{2}}$. If
$\mathcal{J}_{1}|_{\Delta^{\mathcal{J}_{2}}}=\mathcal{J}_{2}|_{\Delta^{\mathcal{J}_{1}}}$,
then $\mathcal{J}_{1}\cup\mathcal{J}_{2}<_{\sf
CP}\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}$.

###### Proof.

Assume
$\mathcal{J}_{1}|_{\Delta^{\mathcal{J}_{2}}}=\mathcal{J}_{2}|_{\Delta^{\mathcal{J}_{1}}}$.
It is easily verified that $\mathcal{J}_{1}\cup\mathcal{J}_{2}$ is also a
model of $\mathcal{K}$ since $\mathcal{J}_{1}$ and $\mathcal{J}_{2}$ agree on
their shared domain. We now check that all four conditions from the definition
of $<_{\sf CP}$ are satisfied:

  1. 1.

From $\mathcal{J}_{1}<_{\sf CP}\mathcal{I}_{\mathcal{P}_{1}}$ we have
$\Delta^{\mathcal{J}_{1}}=\Delta^{\mathcal{I}_{\mathcal{P}_{1}}}$ and
similarly for $\mathcal{J}_{2}$ we have
$\Delta^{\mathcal{J}_{2}}=\Delta^{\mathcal{I}_{\mathcal{P}_{2}}}$. It follows
from its definition that
$\Delta^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}=\Delta^{\mathcal{I}_{\mathcal{P}_{1}}}\cup\Delta^{\mathcal{I}_{\mathcal{P}_{2}}}$.
Therefore we have as desired
$\Delta^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}=\Delta^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$.

  2. 2.

Let $A\in\mathsf{F}$. From $\mathcal{J}_{1}<_{\sf
CP}\mathcal{I}_{\mathcal{P}_{1}}$ we have
$A^{\mathcal{J}_{1}}=A^{\mathcal{I}_{\mathcal{P}_{1}}}$ and similarly for
$\mathcal{J}_{2}$ we have
$A^{\mathcal{J}_{2}}=A^{\mathcal{I}_{\mathcal{P}_{2}}}$. It follows from its
definition that
$A^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}=A^{\mathcal{I}_{\mathcal{P}_{1}}}\cup
A^{\mathcal{I}_{\mathcal{P}_{2}}}$. Therefore we have as desired
$A^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}=A^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$.

  3. 3.

Let $A\in\mathsf{M}$ such that
$A^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\not\subseteq
A^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$. We may assume w.l.o.g.
that $A$ is minimal w.r.t. $\prec$ for this property. We thus have $e\in
A^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\setminus
A^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$. We either have
$e\in\Delta^{\mathcal{J}_{1}}$ or $e\in\Delta^{\mathcal{J}_{2}}$. We treat the
case $e\in\Delta^{\mathcal{J}_{1}}$, the arguments for
$e\in\Delta^{\mathcal{J}_{2}}$ are similar. From $\mathcal{J}_{1}<_{\sf
CP}\mathcal{I}_{\mathcal{P}_{1}}$, there exists a concept $B_{1}\prec A$ s.t.
$B_{1}^{\mathcal{J}_{1}}\subsetneq B_{1}^{\mathcal{I}_{\mathcal{P}_{1}}}$. We
chose such a $B_{1}$ that is minimal for this property, that is s.t. for all
$B\prec B_{1}$, we have
$B^{\mathcal{J}_{1}}=B^{\mathcal{I}_{\mathcal{P}_{1}}}$ (recall $A$ is minimal
for its property so that such a $B$ must verify
$B^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\subseteq
B^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$ hence
$B^{\mathcal{J}_{1}}\subseteq B^{\mathcal{I}_{\mathcal{P}_{1}}}$). If
$B_{1}^{\mathcal{J}_{2}}\subseteq B_{1}^{\mathcal{I}_{\mathcal{P}_{2}}}$, then
we are done as we obtain $B_{1}^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\subsetneq
B_{1}^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$. Otherwise, we have
$B_{1}^{\mathcal{J}_{2}}\not\subseteq B_{1}^{\mathcal{I}_{\mathcal{P}_{2}}}$
and from $\mathcal{J}_{2}<_{\sf CP}\mathcal{I}_{\mathcal{P}_{2}}$, there
exists a concept $B_{2}\prec B_{1}$ s.t. $B_{2}^{\mathcal{J}_{2}}\subsetneq
B_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$. Since $B_{1}$ has been chosen minimal,
we have in particular
$B_{2}^{\mathcal{J}_{1}}=B_{2}^{\mathcal{I}_{\mathcal{P}_{1}}}$, which yields
$B_{2}^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\subsetneq
B_{2}^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$.

  4. 4.

From $\mathcal{J}_{1}<_{\sf CP}\mathcal{I}_{\mathcal{P}_{1}}$, there exists a
concept $A_{1}\in\mathsf{M}$ s.t. $A_{1}^{\mathcal{J}_{1}}\subsetneq
A_{1}^{\mathcal{I}_{\mathcal{P}_{1}}}$ and for all $B\prec A_{1}$, we have
$B^{\mathcal{J}_{1}}=B^{\mathcal{I}_{\mathcal{P}_{1}}}$. If
$A_{1}^{\mathcal{J}_{2}}\subsetneq A_{2}^{\mathcal{P}_{2}}$ and for all
$B\prec A_{1}$, $B^{\mathcal{J}_{2}}=B^{\mathcal{P}_{2}}$, then we obtain
directly $A_{1}^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\subsetneq
A_{1}^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$ and for all $B\prec
A_{1}$,
$B^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}=B^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$
and we are done. Otherwise:

     * •

If $A_{1}^{\mathcal{J}_{2}}\not\subseteq
A_{1}^{\mathcal{I}_{\mathcal{P}_{2}}}$, then from $\mathcal{J}_{2}<_{\sf
CP}\mathcal{I}_{\mathcal{P}_{2}}$, there exists a concept $A_{2}\prec A_{1}$
s.t. $A_{2}^{\mathcal{J}_{2}}\subsetneq
A_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$. Consider a minimal such $A_{2}$, that
is s.t. for all $A\prec A_{2}$, we have
$A^{\mathcal{J}_{2}}=A^{\mathcal{I}_{\mathcal{P}_{2}}}$ or
$A^{\mathcal{J}_{2}}\not\subseteq A^{\mathcal{I}_{\mathcal{P}_{2}}}$. Notice
the second option cannot happen otherwise from $\mathcal{J}_{2}<_{\sf
CP}\mathcal{I}_{\mathcal{P}_{2}}$ we could obtain $A_{3}\prec A_{2}$ s.t.
$A_{2}^{\mathcal{J}_{2}}\subsetneq A_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$,
contradicting the minimality of $A_{2}$. Therefore $A_{2}$ being minimal
yields that for all $A\prec A_{2}$, we have
$A^{\mathcal{J}_{2}}=A^{\mathcal{I}_{\mathcal{P}_{2}}}$. Now, from the
minimality of $A_{1}$, we extend this to $\mathcal{J}_{1}\cup\mathcal{J}_{2}$
and obtain $A_{2}^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\subsetneq
A_{2}^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$ and for all $B\prec
A_{2}$,
$B^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}=B^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$.

     * •

If there exists $A_{2}\prec A_{1}$ s.t. $A_{2}^{\mathcal{J}_{2}}\neq
A_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$. Consider a minimal such $A_{2}$, that
is s.t. for all $A\prec A_{2}$, we have
$A^{\mathcal{J}_{2}}=A^{\mathcal{I}_{\mathcal{P}_{2}}}$. Notice we must have
$A_{2}^{\mathcal{J}_{2}}\subseteq A_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$,
otherwise from $\mathcal{J}_{2}<_{\sf CP}\mathcal{I}_{\mathcal{P}_{2}}$ we
could obtain $A_{3}\prec A_{2}$ s.t. $A_{2}^{\mathcal{J}_{2}}\subsetneq
A_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$, contradicting that for all $A\prec
A_{2}$, we have $A^{\mathcal{J}_{2}}=A^{\mathcal{I}_{\mathcal{P}_{2}}}$.
Therefore, since $A_{2}^{\mathcal{J}_{2}}\neq
A_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$, it must be that
$A_{2}^{\mathcal{J}_{2}}\subsetneq A_{2}^{\mathcal{I}_{\mathcal{P}_{2}}}$.
Now, from the minimality of $A_{1}$, we extend this to
$\mathcal{J}_{1}\cup\mathcal{J}_{2}$ and obtain
$A_{2}^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}\subsetneq
A_{2}^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$ and for all $B\prec
A_{2}$,
$B^{\mathcal{J}_{1}\cup\mathcal{J}_{2}}=B^{\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}}$.

Overall, this proves $\mathcal{J}_{1}\cup\mathcal{J}_{2}<_{\sf
CP}\mathcal{I}_{\mathcal{P}_{1}\cup\mathcal{P}_{2}}$ as desired. ∎

We are now ready to properly prove Lemma 9.

###### Proof of Lemma 9.

“$1\Rightarrow 2$”. Assume there exists $\mathcal{J}\models\mathcal{K}$ s.t.
$\mathcal{J}<_{\sf CP}\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 $\mathcal{J}<_{\sf CP}\mathcal{I}$ ensures 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}_{e}$ as:

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

It is easily verified that $\mathcal{J}_{e}$ is a model of $\mathcal{K}$, and
we now prove $\mathcal{J}_{e}<_{\sf CP}\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$.
We check that all four conditions from the definition of $<_{\sf CP}$ are
satisfied:

  1. 1.

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

  2. 2.

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

  3. 3.

Let $A\in\mathsf{M}$ such that $A^{\mathcal{J}_{e}}\not\subseteq
A^{\mathcal{I}_{\mathcal{P}\cup\\{e\\}}}$. 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}_{e}}\subseteq B^{\mathcal{I}_{\mathcal{P}\cup\\{e\\}}}$ being
trivial, $e_{A}$ additionally witnesses that $B^{\mathcal{J}_{e}}\subsetneq
B^{\mathcal{I}_{\mathcal{P}\cup\\{e\\}}}$.

  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}_{e}}\subsetneq A^{\mathcal{I}_{\mathcal{P}\cup\\{e\\}}}$ and
for all $B\prec A$,
$B^{\mathcal{J}_{e}}=B^{\mathcal{I}_{\mathcal{P}\cup\\{e\\}}}$.

This proves $\mathcal{J}_{e}<_{\sf CP}\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$.
It is straightforward from the definition of each $\mathcal{J}_{e}$ that for
all $e,e^{\prime}$ in $\Delta^{\mathcal{I}}$, we have
$\mathcal{J}_{e}|_{\Delta^{\mathcal{I}_{\mathcal{P}}}}=\mathcal{J}_{e^{\prime}}|_{\Delta^{\mathcal{I}_{\mathcal{P}}}}$,
concluding the proof of “$1\Rightarrow 2$”.

“$2\Rightarrow 1$”. Assume there exist
$\mathcal{P}\subseteq\Delta^{\mathcal{I}}$ with
${\left|{\mathcal{P}}\right|}\leq 2{\left|{\mathcal{T}}\right|}+1$ and a
family $(\mathcal{J}_{e})_{e\in\Delta^{\mathcal{I}}}$ of models of
$\mathcal{K}$ such that $\mathcal{J}_{e}<_{\sf
CP}\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$ and
$\mathcal{J}_{e}|_{\Delta^{\mathcal{I}_{\mathcal{P}}}}=\mathcal{J}_{e^{\prime}}|_{\Delta^{\mathcal{I}_{\mathcal{P}}}}$
for all $e,e^{\prime}\in\Delta^{\mathcal{I}}$. Consider such a
$\mathcal{P}\subseteq\Delta^{\mathcal{I}}$, and family of models
$\mathcal{J}_{e}$ for each $e\in\Delta^{\mathcal{I}}$. We build:

$\mathcal{J}=\bigcup_{e\in\Delta^{\mathcal{I}}}\mathcal{J}_{e}$

It is clear $\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}}$ and since all
$\mathcal{J}_{e}$ agree on the shared domain
$\Delta^{\mathcal{I}_{\mathcal{P}}}$, we apply Lemma 23 to obtain
$\mathcal{J}<_{\sf CP}\mathcal{I}$. ∎

See 6

###### Proof.

We exhibit a NExp procedure to decide the complement of our problem, that is,
existence of a countermodel for UCQ $q$ over $\textrm{DL-Lite}_{\sf bool}$ 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^{{\left|{\mathcal{T}}\right|}{\left|{q}\right|}}$. This can be
done in exponentially many non-deterministic steps. 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 simply exponential w.r.t. our input. 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 over each 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 $\mathcal{J}_{\mathcal{P}}$, we can find a
$\mathcal{J}_{\mathcal{P},e}$ for each
$e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{\mathcal{P}}}$ s.t.
$\mathcal{J}_{\mathcal{P},e}\models\mathcal{K}$ with
$\mathcal{J}_{\mathcal{P},e}<_{\sf CP}\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$
and
$\mathcal{J}_{\mathcal{P},e}|_{\Delta^{\mathcal{J}_{\mathcal{P}}}}=\mathcal{J}_{\mathcal{P}}$,
then our procedure rejects. Otherwise, that is all choices of $\mathcal{P}$
and $\mathcal{J}_{\mathcal{P}}$ led to the existence of a
$e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{\mathcal{P}}}$ without
a fitting $\mathcal{J}_{\mathcal{P},e}$, then it accepts. 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 polynomial size, iterating over each
$\mathcal{J}_{\mathcal{P}}$ can be done naively with exponentially many steps.
Further iterating over each
$e\in\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{\mathcal{P}}}$ can be
done in ${\left|{\Delta^{\mathcal{I}}}\right|}$ steps, which is at most
exponential by construction. Since each $\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$
has polynomial size, deciding the existence of $\mathcal{J}_{\mathcal{P},e}$
can be done naively in exponentially many steps. Overall, the procedure uses
an exponential number of non-deterministic steps at the beginning and further
performs several checks using exponentially many more deterministic steps.

It remains to prove an accepting run exists iff 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 it must also comply with ${\sf
CP}$. Otherwise, the “$1\Rightarrow 2$” direction from Lemma 9 ensures the
procedure would have rejected it. Conversely, if a countermodel exists, Lemma
8 ensures the existence of a countermodel $\mathcal{I}$ whose domain has
exponential size. This $\mathcal{I}$ can be guessed by the procedure that
checks whether it is indeed a model of $\mathcal{K}$ not entailing $q$; hence,
do not reject it at first. The “$2\Rightarrow 1$” direction from Lemma 9
further ensures $\mathcal{I}$ also passes the remaining check performed by the
procedure; otherwise, it would contradict $\mathcal{I}$ being a model of ${\sf
Circ_{\sf CP}}(\mathcal{K})$. ∎

See 7

###### 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 $C$ with $2n$ input gates. The graph $G_{C}$ encoded by $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 $G_{C}$ iff $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 $G_{C}$ is 3-colorable has been proven to be
NExp-complete in (?).

Let $C$ be a Boolean circuit with $2n$ input gates. Let $G=(V,E)$ be the
corresponding graph with $V=\\{v_{1},v_{2},\cdots,v_{2^{n}}\\}$. We denote
$\bar{i}$ the binary encoding on $n$ bits of vertex $v_{i}$. We also identify
${\sf t}$ (True) and ${\sf f}$ (False) with their usual binary valuation $1$
and $0$, respectively. We construct a circumscribed $\textrm{DL-Lite}_{\sf
core}$ KB ${\sf Circ_{\sf CP}}(\mathcal{K})$ with
$\mathcal{K}=(\mathcal{T},\mathcal{A})$ and a UCQ $q$ that encode a given
problem instance. With the aim to restrict colors and truth values to those
defined in the ABox (see axioms (53)), we minimize exactly the concept name
${\sf Min}$ and let others vary freely. Our reduction starts by representing
the colors (49) and truth values (51) in the ABox. The role name ${\sf neq}$
makes the inequality relations within them explicit; see axioms (50) and (52).

$\displaystyle{\sf Col}(c)$ $\displaystyle\text{ for all }c\in\\{{\sf r},{\sf
g},{\sf b}\\}$ (49) $\displaystyle{\sf neq}(c,c^{\prime})$
$\displaystyle\text{ for all }c,c^{\prime}\in\\{{\sf r},{\sf g},{\sf
b}\\}\text{ with }c\neq c^{\prime}$ (50) $\displaystyle{\sf Val}_{b}({\sf
val}_{b})$ $\displaystyle\text{ for all }b\in\\{{\sf f},{\sf t}\\}$ (51)
$\displaystyle{\sf neq}({\sf val}_{b},{\sf val}_{b^{\prime}})$
$\displaystyle\text{ for all }b,b^{\prime}\in\\{{\sf f},{\sf t}\\}\text{ with
}b\neq b^{\prime}$ (52) $\displaystyle{\sf Min}(x)$ $\displaystyle\text{ for
all }x\in\\{{\sf r},{\sf g},{\sf b},{\sf val}_{\sf t},{\sf val}_{\sf f}\\}$
(53)

We aim countermodels to contain $2^{2n}$ elements that each encode a pair
$(v_{k},v_{l})\in V^{2}$. Towards this goal, we lay the foundation to branch a
binary tree of depth $n$ from a root $a_{\sf tree}$, which will be later
enforced via the constructed UCQ further down. The concept names $({\sf
Index}_{i})_{i=1,\cdots,2n}$ encode the tree levels, which fork via the role
names ${\sf next}_{i,{\sf t}}$ and ${\sf next}_{i,{\sf f}}$, encoding whether
the $i$-th bit in $\bar{k}\cdot\bar{l}$ should be set to ${\sf t}$ or ${\sf
f}$, respectively. The desired elements will therefore be (a subset of) the
extension ${\sf Index}_{2n}$. A role name $({\sf hBit}_{j})_{j=1,\cdots,2n}$
will later set the actual bit values. Note that axioms (57) require any $i$-th
tree level to set the bits $1$ to $i$ so that the UCQ can later ensure the
truth values to coincide with the choice via ${\sf next}$. Formally:

$\displaystyle\mathclap{{\sf Index}_{0}(a_{\sf tree})}$ (54)
$\displaystyle{\sf Index}_{i-1}$ $\displaystyle\sqsubseteq\exists{\sf
next}_{i,b}$ (55) $\displaystyle\exists{\sf next}^{-}_{i,b}$
$\displaystyle\sqsubseteq{\sf Index}_{i}$ (56) $\displaystyle{\sf Index}_{i}$
$\displaystyle\sqsubseteq\exists{\sf hBit}_{j}$ $\displaystyle\text{ for all
}j\in\\{1,\cdots,i\\}$ (57) $\displaystyle\exists{\sf hBit}_{j}^{-}$
$\displaystyle\sqsubseteq{\sf Min}$ $\displaystyle\text{ for all
}j\in\\{1,\cdots,2n\\}$ (58)

for all $i\in\\{1,\cdots,2n\\}$ and $b\in\\{{\sf t},{\sf f}\\}$.

We encode the color assignments of $(v_{k},v_{l})$ only at the $2n$-th level
via the role name ${\sf hCol}$ for $v_{k}$ and ${\sf hCol}^{\prime}$ for
$v_{l}$:

$\displaystyle{\sf Index}_{2n}$ $\displaystyle\sqsubseteq\exists{\sf hCol}$
$\displaystyle{\sf Index}_{2n}$ $\displaystyle\sqsubseteq\exists{\sf
hCol}^{\prime}$ (59) $\displaystyle\exists{\sf hCol}^{-}$
$\displaystyle\sqsubseteq{\sf Min}$ $\displaystyle\exists{{\sf
hCol}^{\prime}}^{-}$ $\displaystyle\sqsubseteq{\sf Min}$ (60)

Finally, the computation of a gate $g$ in $C$ is enforced for each pair by an
outgoing edge ${\sf gate}_{g}$ at the $2n$-th level. Add:

$\displaystyle{\sf Index}_{2n}$ $\displaystyle\sqsubseteq\exists{\sf
gate}_{g}$ (61) $\displaystyle\exists{\sf gate}_{g}$
$\displaystyle\sqsubseteq{\sf Min}$ (62)

for all gates $g$ in $C$.

Let the constructed UCQ $q$ be the disjunction over all subsequent queries. We
first make sure that no color is used as a truth value (CQs (63) and (64)) or
vice-versa (CQs (65) and (66)):

$\displaystyle\exists x,y\,{\sf hBit}_{j}(x,y)\wedge{\sf Col}(y)$
$\displaystyle\text{ for all }j\in\\{1,\cdots,2n\\}$ (63)
$\displaystyle\exists x,y\,{\sf gate}_{g}(x,y)\wedge{\sf Col}(y)$
$\displaystyle\text{ for all gates }g\text{ in }G^{\prime}$ (64)
$\displaystyle\exists x,y\,{\sf hCol}(x,y)\wedge{\sf Val}_{b}(y)$
$\displaystyle\text{ for all }b\in\\{{\sf t},{\sf f}\\}$ (65)
$\displaystyle\exists x,y\,{\sf hCol}^{\prime}(x,y)\wedge{\sf Val}_{b}(y)$
$\displaystyle\text{ for all }b\in\\{{\sf t},{\sf f}\\}$ (66)

We next simultaneously enforce that a) the structure constructed by axioms
(54)–(56) really is a tree, and b) that the valuation required by axioms (57)
and (58) is consistent with the branching of the tree. We achieve this via CQs
(67), which makes countermodels assign the bits by ${\sf hBit}$ as dictated by
${\sf next}$, and via CQs (68), which makes countermodels propagate the bit
assignment of a node downwards the tree to all successors:

$\displaystyle\begin{split}\exists x,y,z_{1},z_{2}\,&{\sf
next}_{i-1,b}(x,y)\wedge{\sf hBit}_{j}(y,z_{1})\\\ &\wedge{\sf
neq}(z_{1},z_{2})\wedge{\sf Val}_{b}(z_{2})\end{split}$ (67)
$\displaystyle\begin{split}\exists x,y,z_{1},z_{2}\,&{\sf
next}_{i-1,b}(x,y)\wedge{\sf hBit}_{j}(x,z_{1})\\\ &\wedge{\sf
hBit}_{j}(x,z_{2})\wedge{\sf neq}(z_{1},z_{2})\end{split}$ (68)

for all $i\in\\{1,\cdots,2n\\}$, $j\in\\{1,\cdots,i\\}$ and $b\in\\{{\sf
t},{\sf f}\\}$. Observe that the above indeed enforces a tree.

We go on to construct CQs (69) and (70), which prohibit any two encoded pairs
of vertices $(v,u)$ and $(v,u^{\prime})$ or $(v,u)$ and $(u,u^{\prime})$ to
assign different colors to $v$ or $u$, respectively:

$\displaystyle\begin{split}\exists&x,y,c,d,z_{1},\cdots,z_{n}\,{\sf
hCol}(x,c)\wedge{\sf hCol}(y,d)\\\ &\wedge{\sf neq}(c,d)\wedge\bigwedge_{1\leq
j\leq n}\big{(}{\sf hBit}_{j}(y,z_{j})\wedge{\sf
hBit}_{j}(x,z_{j})\big{)}\end{split}$ (69)
$\displaystyle\begin{split}\exists&x,y,c,d,z_{1},\cdots,z_{n}\,{\sf
hCol}(x,c)\wedge{\sf hCol}^{\prime}(y,d)\\\ &\wedge{\sf
neq}(c,d)\wedge\bigwedge_{1\leq j\leq n}\big{(}{\sf
hBit}_{j}(y,z_{j})\wedge{\sf hBit}^{\prime}_{j+n}(x,z_{j})\big{)}\end{split}$
(70)

To ensure that the computation of the boolean circuit is consistent, we
construct CQs restricting ${\sf gate}_{g}$ to follow the logical operator of
$g$. For this, we assume w.l.o.g. that $C$ only contains unary NOT-gates,
binary AND- and OR-gates, and $2n$ nullary INPUT-gates (each encoding a bit in
$\bar{k}\cdot\bar{l}$). Given an INPUT-gate $g$ from $C$, we denote the index
of the encoded bit from $\bar{k}\cdot\bar{l}$ with $i_{g}$. Construct, for
each INPUT-gate $g$ from $C$, the CQ as given next:

$\displaystyle\begin{split}\exists x,y,z\,{\sf gate}_{g}(x,y)\wedge{\sf
hBit}_{i_{g}}(x,z)\wedge{\sf neq}(y,z)\end{split}$ (71)

For all NOT-gates $g$ with their parent $g^{\prime}$, construct

$\displaystyle\begin{split}\exists x,y\,{\sf gate}_{g}(x,y)\wedge{\sf
gate}_{g^{\prime}}(x,y)\end{split}$ (72)

For all AND-gates $g$ with parents $g_{1},g_{2}$, construct

$\displaystyle\begin{split}\exists x,y,z\,&{\sf gate}_{g}(x,y)\wedge{\sf
Val}_{\sf t}(y)\wedge{\sf gate}_{g_{1}}(x,z)\\\ &\wedge{\sf Val}_{\sf
f}(z)\end{split}$ (73) $\displaystyle\begin{split}\exists x,y,z\,&{\sf
gate}_{g}(x,y)\wedge{\sf Val}_{\sf t}(y)\wedge{\sf gate}_{g_{2}}(x,z)\\\
&\wedge{\sf Val}_{\sf f}(z)\end{split}$ (74)
$\displaystyle\begin{split}\exists x,y,z\,&{\sf gate}_{g}(x,y)\wedge{\sf
Val}_{\sf f}(y)\wedge{\sf gate}_{g_{1}}(x,z)\\\ &\wedge{\sf Val}_{\sf
t}(z)\wedge{\sf gate}_{g_{2}}(x,z)\end{split}$ (75)

For all OR-gates $g$ with parents $g_{1},g_{2}$, construct

$\displaystyle\begin{split}\exists x,y,z\,&{\sf gate}_{g}(x,y)\wedge{\sf
Val}_{\sf f}(y)\wedge{\sf gate}_{g_{1}}(x,z)\\\ &\wedge{\sf Val}_{\sf
t}(z)\end{split}$ (76) $\displaystyle\begin{split}\exists x,y,z\,&{\sf
gate}_{g}(x,y)\wedge{\sf Val}_{\sf f}(y)\wedge{\sf gate}_{g_{2}}(x,z)\\\
&\wedge{\sf Val}_{\sf t}(z)\end{split}$ (77)
$\displaystyle\begin{split}\exists x,y,z\,&{\sf gate}_{g}(x,y)\wedge{\sf
Val}_{\sf t}(y)\wedge{\sf gate}_{g_{1}}(x,z)\\\ &\wedge{\sf Val}_{\sf
f}(z)\wedge{\sf gate}_{g_{2}}(x,z)\end{split}$ (78)

Finally, we rule out the existence of monochromatic edges in countermodels via
CQ (79):

$\displaystyle\exists x,y,z\,{\sf hCol}(x,y)\wedge{\sf
hCol}^{\prime}(x,y)\wedge{\sf gate}_{\dot{g}}(x,z)\wedge{\sf Val}_{\sf t}(z)$
(79)

where we here and in what follows denote by $\dot{g}$ the output gate of $C$.

######  Lemma 24.

$G$ is 3-colorable iff ${\sf Circ_{\sf CP}}(\mathcal{K})\not\models q$.

“$\Rightarrow$”. Let $G$ be 3-colorable. Then there exists a 3-coloring
$\pi:V\rightarrow\\{{\sf r},{\sf g},{\sf b}\\}$ such that $\pi(v)\neq\pi(u)$
for all $(v,u)\in V$. To show that ${\sf Circ_{\sf
CP}}(\mathcal{K})\not\models q$, we construct a countermodel $\mathcal{I}$ of
${\sf Circ_{\sf CP}}(\mathcal{K})$ as follows. Let
$X\coloneqq\bigcup_{j=1,\cdots,2n}\\{a_{j,1},\cdots,a_{j,2^{j}}\\}$; then set

$\displaystyle\Delta^{\mathcal{I}}\coloneqq$ $\displaystyle{\sf
ind}(\mathcal{A})\cup X$ $\displaystyle A^{\mathcal{I}}\coloneqq$
$\displaystyle\\{a\mid A(a)\in\mathcal{A}\\}$ $\displaystyle{\sf
neq}^{\mathcal{I}}\coloneqq$ $\displaystyle\\{(a,b)\mid{\sf
neq}(a,b)\in\mathcal{A}\\}$ $\displaystyle{\sf
Index}^{\mathcal{I}}_{i}\coloneqq$
$\displaystyle\\{a_{i,1},\cdots,a_{i,2^{i}}\\}$ $\displaystyle{\sf
next}^{\mathcal{I}}_{i,{\sf t}}\coloneqq$
$\displaystyle\bigcup_{j=1,\cdots,2^{i-1}}\\{(a_{i-1,j},a_{i,2j})\\}$
$\displaystyle{\sf next}^{\mathcal{I}}_{i,{\sf f}}\coloneqq$
$\displaystyle\bigcup_{j=1,\cdots,2^{i-1}}\\{(a_{i-1,j},a_{i,2j-1})\\}$
$\displaystyle\begin{split}{\sf
hBit}^{\mathcal{I}}_{i}\coloneqq&\bigcup_{j=1,\cdots,2^{i-1}}\big{(}\\{(a,{\sf
val}_{\sf t})\mid a\in R(a_{i,2j})\\}\\\ &\phantom{\bigcup_{1\leq j\leq
2^{i-1}}\big{(}}\cup\\{(a,{\sf val}_{\sf f})\mid a\in
R(a_{i,2j-1})\\}\big{)}\end{split}$

for all concept names $A\in\\{{\sf Col},{\sf Val}_{\sf t},{\sf Val}_{\sf
f},{\sf Min},{\sf Index}_{0}\\}$ and $i\in\\{1,\cdots,2n\\}$, where we use

  * •

$a_{0,1}$ to denote $a_{\sf tree}$, and

  * •

$R(a_{k,l})$ to denote the set of instances that are reachable in
$\mathcal{I}$ from $a_{k,l}\in X$ via the family of role names ${\sf
next}_{i,{\sf t}}$ and ${\sf next}_{i,{\sf f}}$ (including $a_{k,l}$ itself).

We furthermore set ${\sf hCol}^{\mathcal{I}},{{\sf
hCol}^{\prime}}^{\mathcal{I}}$ as follows. Given some $a_{2n,i}\in X$ with
$i\in\\{1,\cdots 2^{2n}\\}$, we denote by $\vartheta(a_{2n,i})$ the encoded
pair $(v_{k},u_{l})\in V^{2}$, i.e., such that for all
$j\in\\{1,\cdots,2n\\}$, we have $(a_{2n,i},{\sf val}_{b})\in{\sf
hBit}_{j}^{\mathcal{I}}$ iff the $j$-th bit in $\bar{k}\cdot\bar{l}$ is $b$
with $b\in\\{{\sf t},{\sf f}\\}$.

$\displaystyle{\sf hCol}^{\mathcal{I}}\coloneqq$
$\displaystyle\left\\{\big{(}a_{2n,i},\pi(v)\big{)}\mid\vartheta(a_{2n,i})=(v,u)\right\\}$
$\displaystyle{{\sf hCol}^{\prime}}^{\mathcal{I}}\coloneqq$
$\displaystyle\left\\{\big{(}a_{2n,i},\pi(u)\big{)}\mid\vartheta(a_{2n,i})=(v,u)\right\\}$

Finally, we set ${\sf gate}_{g}$ for all gates $g$ in $G_{C}$. We denote the
sub-circuit of $G_{C}$ that contains exactly $g$ and all its ancestors with
$G_{C}^{g}$. Note that the output gate of $G_{C}^{g}$ is $g$, i.e.,
$G_{C}^{g}(\bar{k},\bar{l})$ computes the value of $g$ in $G_{C}$ given the
input $(\bar{k},\bar{l})$. Then, for all gates $g$, set:

$\displaystyle\begin{split}{\sf
gate}_{g}^{\mathcal{I}}\coloneqq&\\{(a_{2n,i},{\sf
val}_{b})\mid\vartheta(a_{2n,i})=(v_{k},u_{l})\\\ &\phantom{\\{(a_{2n,i},{\sf
val}_{\sf t})\mid}\text{ and }G_{C}^{g}(\bar{k},\bar{l})=b\\}\\\ \end{split}$

It is obvious that $\mathcal{I}$ is a model of $\mathcal{K}$. As $a\in{\sf
Min}^{\mathcal{I}}$ iff ${\sf Min}(a)$ for all $a\in\Delta^{\mathcal{I}}$, and
${\sf Min}$ is the only minimized concept, $\mathcal{I}$ must furthermore be
minimal.

To see that $\mathcal{I}\not\models q$, it is readily checked that

  * •

$\mathcal{I}$ by definition has no answer to CQs (63)–(70),

  * •

additionally, $\mathcal{I}$ has no answer to CQs (71)–(78), as otherwise, the
computation of $G_{C}$ would be inconsistent, and

  * •

finally, $\mathcal{I}$ has no answer to CQ (79), as otherwise, $\pi$ would not
be a 3-coloring of $G$.

“$\Leftarrow$”. Let ${\sf Circ_{\sf CP}}(\mathcal{K})\not\models q$. Then
there is a model $\mathcal{I}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$ such that
$\mathcal{I}\not\models q$. We aim to extract a function
$\pi:V\rightarrow\\{{\sf r},{\sf g},{\sf b}\\}$ and to show that $\pi$ is
indeed a 3-coloring of $G$. This is rather laborious, as we have to prepare
the final argument in five steps. In Claim (3)–(7), respectively, we

  1. 1.

briefly argue that ${\sf hBit}$ and ${\sf gate}$ have the range $\\{{\sf
val}_{\sf t},{\sf val}_{\sf f}\\}$ and that ${\sf hCol}$ and ${\sf
hCol}^{\prime}$ have the range $\\{{\sf r},{\sf g},{\sf b}\\}$, which will be
convenient later on,

  2. 2.

identify within $\mathcal{I}$ the intended tree-structure,

  3. 3.

show that each leaf indeed encodes a pair $(v_{k},v_{l})\in V^{2}$, setting
precisely the bits from $\bar{k}\cdot\bar{l}$,

  4. 4.

extract $\pi$ from $\mathcal{I}$ and show that it is sound in the sense that
any two leaves that encode the same vertex also assign it the same color, and

  5. 5.

proof that the leaves correctly compute all gates.

We start with the ranges of ${\sf hBit},{\sf gate}$ and ${\sf hCol}$:

######  Claim 3.

The following properties hold.

  * •

both $(x,y)\in{\sf hBit}^{\mathcal{I}}_{i}$ and $(x,y)\in{\sf
gate}^{\mathcal{I}}_{g}$ entail $y\in\\{{\sf val}_{\sf t},{\sf val}_{\sf
f}\\}$ for all $i\in\\{1,\cdots,2n\\}$ and gates $g$ in $C$, and

  * •

both $(x,y)\in{\sf hCol}^{\mathcal{I}}$ and $(x,y)\in{{\sf
hCol}^{\prime}}^{\mathcal{I}}$ entail $y\in\\{{\sf r},{\sf g},{\sf b}\\}$.

The proof is simple: As $\mathcal{I}$ is a model of $\mathcal{A}$, axioms (53)
imply $\\{{\sf r},{\sf g},{\sf b},{\sf val}_{\sf t},{\sf val}_{\sf
f}\\}\subseteq{\sf Min}^{\mathcal{I}}$. Furthermore, it is obvious that there
cannot be any $a\in{\sf Min}^{\mathcal{I}}$ with ${\sf
Min}(a)\notin\mathcal{A}$, since $\mathcal{I}$ would otherwise not be $<_{\sf
CP}$ minimal (it would then be straightforward to construct a smaller model).
Ergo, ${\sf Min}^{\mathcal{I}}=\\{{\sf r},{\sf g},{\sf b},{\sf val}_{\sf
t},{\sf val}_{\sf f}\\}$.

The rest of the claim follows from axioms (49), (51), (58), (60), (62), CQs
(63)–(66), and $\mathcal{I}\not\models q$: For example, in the case of ${\sf
hCol}$, consider some $(x,y)\in{\sf hCol}^{\mathcal{I}}$. By axiom (60), we
have that $y\in{\sf Min}^{\mathcal{I}}$. CQ (65) and the fact that
$\mathcal{I}\not\models q$ together yield $y\in{\sf
Min}^{\mathcal{I}}\setminus({\sf Val}_{\sf t}\cup{\sf Val}_{\sf f})$. As
$\\{{\sf val}_{\sf t},{\sf val}_{\sf f}\\}\subseteq{\sf Val}_{\sf t}\cup{\sf
Val}_{\sf f}$ by axioms (51), we thus have that $y\in\\{{\sf r},{\sf g},{\sf
b}\\}$. The other cases are analogous.

This finishes the proof of Claim (3).

We go on by identifying within $\mathcal{I}$ the intended tree structure:

######  Claim 4.

For all $i\in\\{1,\cdots,2n\\}$ there is a set $Y_{i}\subseteq{\sf
Index}^{\mathcal{I}}_{i}$ that satisfies the following properties:

  1. 1.

for all $y\in Y_{i}$, there is exactly one _parent $p\in Y_{i-1}$ of $y$_ with
$(p,y)\in{\sf next}_{i-1,b}^{\mathcal{I}}$ for some $b\in\\{{\sf t},{\sf
f}\\}$ (we set $Y_{0}=\\{a_{\sf tree}\\}$),

  2. 2.

for all $y\in Y_{i}$ and $j\in\\{1,\cdots,i\\}$, there is exactly one
$b\in\\{{\sf t},{\sf f}\\}$ such that $(y,{\sf val}_{n})\in{\sf hBit}_{j}$,

  3. 3.

for all $x,y\in Y_{i}$ with $x\neq y$, there is some $j\in\\{1,\cdots,i\\}$
such that $(x,{\sf val}_{\sf t})\in{\sf hBit}_{j}$ iff $(y,{\sf val}_{\sf
f})\in{\sf hBit}_{j}$, and

  4. 4.

$|Y_{i}|=2^{i}$.

The proof of Claim (4) goes via induction over $i$:

Base case ($i=1)$.

Axioms (54)–(56) require the existence of some $x,y\in{\sf
Index}_{1}^{\mathcal{I}}$ such that $(a_{\sf tree},x)\in{\sf next}_{1,{\sf
t}}^{\mathcal{I}}$ and $(a_{\sf tree},y)\in{\sf next}_{1,{\sf
f}}^{\mathcal{I}}$. Set $Y_{1}=\\{x,y\\}$. Property 1. of Claim (4) obviously
holds as $a_{\sf tree}$ is, on the one hand, the only element in $Y_{0}$, and,
on the other hand, the parent of both $x$ and $y$. Together with Claim (3),
axioms (52), and (57), and CQs (67) (and the fact that $\mathcal{I}\not\models
q$), we have that $(x,{\sf val}_{\sf t})\in{\sf hBit}_{1}^{\mathcal{I}}$ and
$(y,{\sf val}_{\sf f})\in{\sf hBit}_{1}^{\mathcal{I}}$, while $(x,{\sf
val}_{\sf f})\notin{\sf hBit}_{1}^{\mathcal{I}}$ and $(y,{\sf val}_{\sf
t})\notin{\sf hBit}_{1}^{\mathcal{I}}$, i.e., also properties 2. and 3. hold.
The above furthermore entails $x\neq y$, which is why also property 4. must
hold.

Induction step ($i>1$).

By the induction hypothesis, there is a set $Y_{i-1}$ with the claimed
properties. For all $y\in Y_{i-1}$, axioms (54)–(56) entail the existence of
elements $a_{y},a_{y}^{\prime}\in{\sf Index}_{i}^{\mathcal{I}}$ such that
$(y,a_{y})\in{\sf next}_{i,{\sf t}}^{\mathcal{I}}$ and
$(y,a^{\prime}_{y})\in{\sf next}_{i,{\sf f}}^{\mathcal{I}}$. Similar as in the
base case, we deduct that $(a_{y},{\sf val}_{\sf t})\in{\sf
hBit}_{i}^{\mathcal{I}}$ and $(a^{\prime}_{y},{\sf val}_{\sf f})\in{\sf
hBit}_{i}^{\mathcal{I}}$, while $(a_{y},{\sf val}_{\sf f})\notin{\sf
hBit}_{i}^{\mathcal{I}}$ and $(a^{\prime}_{y},{\sf val}_{\sf t})\notin{\sf
hBit}_{i}^{\mathcal{I}}$ $({\dagger})$ via Claim (3), axioms (52) and (57),
and CQs (67) (and the fact that $\mathcal{I}\not\models q$). Set
$Y_{i}=\bigcup_{y\in Y_{i-1}}\\{a_{y},a_{y}^{\prime}\\}$.

To see that $Y_{i}$ satisfies property 1., assume to the contrary that there
is some $a\in Y_{i}$ with two parents from $Y_{i-1}$, i.e., that there are two
elements $y,y^{\prime}\in Y_{i-1}$ such that $(y,a)\in{\sf
next}_{i-1,b}^{\mathcal{I}}$ and $(y^{\prime},a)\in{\sf
next}_{i-1,b^{\prime}}^{\mathcal{I}}$ for some $b,b^{\prime}\in\\{{\sf t},{\sf
f}\\}$. By property 3. of the induction hypothesis, there must be some
$j\in\\{1,\cdots,i-1\\}$ such that $(x,{\sf val}_{\sf t})\in{\sf
hBit}_{j}^{\mathcal{I}}$ iff $(x^{\prime},{\sf val}_{\sf f})\in{\sf
hBit}_{j}^{\mathcal{I}}$. Furthermore observe that Claim (3) and axioms (57)
require $a$ to assign the $j$-th bit, i.e., we have $(a,{\sf val}_{\sf
t})\in{\sf hBit}_{j}^{\mathcal{I}}$ or $(a,{\sf val}_{\sf f})\in{\sf
hBit}_{j}^{\mathcal{I}}$. In either case, due to axioms (52), we can find a
homomorphism from CQ (68) to $\mathcal{I}$, which contradicts the fact that
$\mathcal{I}$ is a countermodel to $q$. Ergo, $Y_{i}$ must satisfy property 1.

Property 2. follows, in case of $j=i$, from $({\dagger})$, and, if otherwise
$j\in\\{1,\cdots,i-1\\}$, from $Y_{i-1}$ satisfying property 2. and the fact
that Claim (3), axioms (52) and (57), and CQs (68) require all $a\in Y_{i}$ to
assign the bits $1,\cdots,i-1$ exactly as their parents.

For property 3, consider some $a,a^{\prime}\in Y_{i}$ with $a\neq a^{\prime}$.
If $a$ and $a^{\prime}$ have the same parent $x$, property 3. follows from
$({\dagger})$ and property 1. Otherwise, if $a$ has a parent $x$ and
$a^{\prime}$ has a parent $y$ such that $x\neq y$, observe that property 3. of
the induction hypothesis implies the existence of some
$j\in\\{1,\cdots,i-1\\}$ such that $(x,{\sf val}_{\sf t})\in{\sf hBit}_{j}$
iff $(y,{\sf val}_{\sf f})\in{\sf hBit}_{j}$. Property 3. then follows from
the fact that Claim (3), axioms (52) and (57), and CQs (68) require $a$ and
$a^{\prime}$ to assign the bits $1,\cdots,i-1$ exactly as their parents.

Regarding property 4., observe that by $({\dagger})$, $Y_{i}$ contains two
elements $a_{y},a_{y}^{\prime}$ with $a_{y}\neq a_{y}^{\prime}$ for each $y\in