$[k_{0}]=\\{1,\dots,k_{0}+1\\}$. All notions for
$\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled trees such as properness, the
associated ABox carry over to the extended alphabet. Additionally, we say that
a $\Sigma_{\varepsilon}\cup(\Sigma_{N}\times[k_{0}])$-labeled tree $(T,L)$ is
_counting_ if for every node $x\in T$ on level $i>0$, $L(T)=(\alpha,j)$
implies $j=\mathsf{min}(i,k_{0}+1)$.

The desired TWAPA $\mathfrak{A}$ is the intersection of five TWAPAs
$\mathfrak{A}_{0},\dots,\mathfrak{A}_{4}$. While $\mathfrak{A}_{0}$ makes sure
that the input tree $(T,L)$ is proper and counting, each of the automata
$\mathfrak{A}_{1},\dots,\mathfrak{A}_{4}$ makes sure that the ABox
$\mathcal{A}_{(T,L)}$ satisfies the corresponding condition from the above
list. In fact, we have already seen in Section C.4 how to build TWAPAs for
Conditions 1 and 2; they are easily adapted to the new input format and simply
ignore the additional counting component of input trees. Moreover, the
automaton $\mathfrak{A}_{Q}$ which ensures Condition 2 is easily modified to
ensure Conditions 3 and 4 provided that the input tree is counting; the
modified automaton simply ignores those parts of the input that are ‘truncated
away’.

It thus remains to verify that we can build the automaton $\mathfrak{A}_{0}$.
Properness was already dealt with in Section C.4. We additionally need to
verify that the input tree is counting. This can be done with
$O(\mathsf{log}(k_{0}))$ states: we send a copy to the automaton to every tree
node, for every $i$-th bit,
$i\in\\{1,\dots,\lceil\mathsf{log}(k_{0})\rceil\\}$. Based on the node label,
we determine the value $t\in\\{0,1\\}$ of the $i$-th bit at all successors and
send a copy of the automaton in state “$\mathsf{bit}\;i{=}t$” to all
successors nodes, where that value is verified.

It can be verified that the constructed overall TWAPA $\mathfrak{A}$ has
${2^{p(|q_{1}|+\mathsf{log}(|\mathcal{T}_{1}|))}}$ states, $p$ a polynomial.
From the complexity of TWAPA emptiness, we thus get Point 1 in Theorem 6. If
$\mathcal{T}$ is formulated in $\mathcal{ELIHF}_{\bot}$, then $\mathfrak{A}$
has only $p(|q_{1}|+|\mathcal{T}_{1}|)$ states due to the improved bounds for
this logic in Theorem 11 and Proposition 13. Consequently, we also obtain the
upper bound in Point 2 of Theorem 5.

##  Appendix D Rooted Queries

We now establish the coNExpTime upper bounds for rooted queries (Theorem 15).
We first give the proof for containment, and afterwards we explain how the
construction can be modified to handle FO-rewritability.

###  D.1 Overview of upper bound for containment

For convenience, we repeat the result we aim to prove.

######  Theorem 39.

Containment for OMQs in $(\mathcal{ELIHF}_{\bot},\text{rCQ})$ is in
coNExpTime.

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\mathcal{ELIHF}_{\bot}$
TBoxes, let $\Sigma$ be an ABox signature, and let $q_{1}$ and $q_{2}$ be
rooted CQs. We recall that by Proposition 8,
$(\mathcal{T}_{1},\Sigma,q_{1})\not\subseteq(\mathcal{T}_{2},\Sigma,q_{2})$
iff there is a pseudo tree $\Sigma$-ABox $\mathcal{A}$ of outdegree at most
$|\mathcal{T}_{1}|$ and width at most $|q_{1}|$ that is consistent with both
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ and a tuple $\mathbf{a}$ from the core
of $\mathcal{A}$ such that $\mathcal{T}_{1},\mathcal{A}\models
q_{1}(\mathbf{a})$ and $\mathcal{T}_{2},\mathcal{A}\not\models
q_{2}(\mathbf{a})$. To test for the existence of such a witness ABox and
tuple, we proceed as follows.

Step 1 Guess the following:

  * •

pseudo tree $\Sigma$-ABox $\mathcal{A}_{\mathsf{init}}$ whose core is bounded
by $|q_{1}|$, whose outdegree is bounded by $|\mathcal{T}_{1}|$, whose depth
is bounded by $m_{q}=\mathsf{max}(|q_{1}|,|q_{2}|)$ (with $\mathcal{U}_{q}$
the set of individuals that are at distance exactly $m_{q}$ from the core)

  * •

tuple $\mathbf{a}$ of individuals from the core of $\mathcal{A}$, of the same
arity as $q_{1}$ and $q_{2}$

  * •

ABoxes $\mathcal{B}_{1}$ and $\mathcal{B}_{2}$ such that
$\mathcal{A}\subseteq\mathcal{B}_{i}$ and
$\mathcal{B}_{i}\setminus\mathcal{A}\subseteq\\{B(a)\mid
a\in\mathsf{Ind}(\mathcal{A}),B\in{\sf N_{C}}\\}$, for $i\in\\{1,2\\}$

  * •

two ‘global’ candidate transfer sequences
$\mathcal{Y}_{0}^{1},\ldots,\mathcal{Y}^{1}_{N_{1}}$ and
$\mathcal{Y}^{2}_{0},\ldots,\mathcal{Y}^{2}_{N_{2}}$ for
$(\mathcal{U}_{q},\mathcal{T}_{1})$ and $(\mathcal{U}_{q},\mathcal{T}_{2})$
respectively (precise definition given later)

Intuitively, the guessed ABox $\mathcal{A}_{\mathsf{init}}$ is the initial
portion of a witness for non-containment, obtained by restricting the witness
ABox to individuals within distance $m_{q}=\mathsf{max}(|q_{1}|,|q_{2}|)$ of
the core, and $\mathbf{a}$ is a tuple witnessing the non-containment. The ABox
$\mathcal{B}_{i}$ ($i\in\\{1,2\\}$) enriches $\mathcal{A}_{\mathsf{init}}$
with the concept assertions over $\mathsf{Ind}(\mathcal{A})$ that are entailed
from the full witness ABox and the TBox $\mathcal{T}_{i}$. To keep track of
the interactions between the guessed part $\mathcal{A}_{\mathsf{init}}$ and
the missing trees, we generalize the notion of transfer sequence to sets of
individuals (rather than a single individual). The guessed sequence
$\mathcal{Y}^{i}_{0},\ldots,\mathcal{Y}^{i}_{N_{i}}$ ($i\in\\{1,2\\}$)
corresponds to the transfer sequence of the full witness ABox with respect to
the individuals in $\mathcal{U}_{q}$ (occuring at depth $m_{q}$) and the TBox
$\mathcal{T}_{i}$.

Step 2 Verify that:

  * •

for $i\in\\{1,2\\}$, $\mathcal{B}_{i}$ is consistent with $\mathcal{T}_{i}$

  * •

$\mathcal{B}_{1},\mathcal{T}_{1}\models q_{1}(\mathbf{a})$ and
$\mathcal{B}_{2},\mathcal{T}_{2}\not\models q_{2}(\mathbf{a})$

  * •

for $i\in\\{1,2\\}$, the candidate transfer sequence
$\mathcal{Y}^{i}_{0},\ldots,\mathcal{Y}^{i}_{N_{i}}$ is compatible with
$(\mathcal{A},\mathcal{B}_{i})$

and return no if one of these conditions fails to hold.

The second point corresponds to checking that, with respect to the full
witness, we have $q_{1}(\mathbf{a})$ but not $q_{2}(\mathbf{a})$. Indeed,
since $q_{1}$ and $q_{2}$ are rooted, we know that query matches only involve
individuals that are within distance $m_{q}$ of the core. Since
$\mathcal{B}_{i}$ contains all concept assertions for these individuals that
are entailed w.r.t. the full witness ABox, it can be used in place of the
witness. The compatibility checks in the third item (which will be made
precise further) will be used to ensure that
$\mathcal{Y}^{i}_{0},\ldots,\mathcal{Y}^{i}_{N_{i}}$ is the transfer sequence
of the full witness ABox w.r.t. $\mathcal{U}_{q}$ and $\mathcal{T}_{i}$.

Step 3 For each individual $u\in\mathcal{U}_{q}$, construct a tree automaton
that checks whether there is a tree-shaped ABox $\mathcal{A}_{u}$ rooted at
$u$ that does not contain any concept assertion $A(u)$ and is such that for
both $i\in\\{1,2\\}$, we have:

  * •

$\mathcal{Y}^{i}_{0},\ldots,\mathcal{Y}^{i}_{N_{i}}$ is compatible with
$\mathcal{A}_{u}$ at $u$ w.r.t. $\mathcal{T}_{i}$

  * •

$\mathcal{A}_{u}\cup\mathcal{Y}^{i}_{N_{i}}$ is consistent with
$\mathcal{T}_{i}$

  * •

if $\mathsf{func}(r)\in\mathcal{T}_{i}$ and $r(u,u^{\prime})\in\mathcal{A}$,
then $\mathcal{A}_{u}$ does not contain any assertion of the form
$r(u,u^{\prime\prime})$

Return yes if all of these automata are non-empty, otherwise return no.

The final step checks that it is possible to construct, for every individual
$u$ at depth $m_{q}$, a tree-shaped ABox $\mathcal{A}_{u}$, such that the ABox
$\mathcal{A}_{\mathsf{init}}\cup\bigcup_{u\in\mathcal{U}_{q}}\mathcal{A}_{u}$
that is obtained by attaching all of these trees to
$\mathcal{A}_{\mathsf{init}}$ yields the full witness ABox (by renaming
individuals, we can assume that
$\mathsf{Ind}(\mathcal{A}_{\mathsf{init}})\cap\mathsf{Ind}(\mathcal{A}_{u})=\\{u\\}$
and $\mathsf{Ind}(\mathcal{A}_{u})\cap\mathsf{Ind}(\mathcal{A}_{v})=\emptyset$
for $u,v\in$ with $u\neq v$). For this to be the case, we need to ensure that
the tree-shaped ABoxes allow us to infer exactly those concept assertions
present in the candidate transfer sequence (this is the purpose of the
compatibility condition, formalized further). We must also ensure that after
adding the entailed assertions $\mathcal{Y}^{i}_{N_{i}}$ to ABox
$\mathcal{A}_{u}$, the resulting ABox is consistent with both TBoxes and that
no violations of functionality assertions are introduced when attaching
$\mathcal{A}_{u}$ to $\mathcal{A}_{\mathsf{init}}$.

In what follows, we provide more details on Steps 2 and 3 of this procedure.

###  D.2 Query entailment checks in Step 2

We briefly explain how to perform the query entailment checks in Step 2. We
focus on the first entailment check $\mathcal{B}_{1},\mathcal{T}_{1}\models
q_{1}(\mathbf{a})$, but the same construction can be used to decide whether
$\mathcal{B}_{2},\mathcal{T}_{2}\not\models q_{2}(\mathbf{a})$. The idea is as
follows: to decide whether $\mathcal{B}_{1},\mathcal{T}_{1}\models
q_{1}(\mathbf{a})$, we will compute the restriction
$\mathcal{I}_{\mathcal{B}_{1},\mathcal{T}}^{q_{1}}$ of the canonical model
$\mathcal{I}_{\mathcal{B}_{1},\mathcal{T}}$ to the ABox individuals in
$\mathcal{B}$ and the new domain elements that are within distance $|q_{1}|$
of one of these individuals. Then it suffices to iterate over all
(exponentially many) mappings $\pi$ from the variables of $q_{1}$ into
$\Delta^{\mathcal{I}_{\mathcal{B},\mathcal{T}}^{q_{1}}}$ and to check if one
of these mappings is a match for the query.

We sketch how to construct the interpretation
$\mathcal{I}^{q_{1}}_{\mathcal{B}_{1},\mathcal{T}}$ in exponential time. For
convenience, we adopt the ABox representation of interpretations. We first
include all concept and role assertions that are entailed from
$\mathcal{B}_{1},\mathcal{T}$; such assertions can be computed in exponential
time (e.g., by applying the modified closure rules from Appendix B.2). Next,
for each individual $a\in\mathsf{Ind}(\mathcal{B}_{1})$, we let $C_{a}$ be the
conjunction of concepts $A$ such that $A(a)\in\mathcal{B}_{1}$. To determine
which successors we need to connect to $a$, we compute all axioms of the form
$C_{a}\sqsubseteq\exists R.D$, where $R$ is a conjunction of roles from
$\mathsf{sig}(\mathcal{T})$ and $D$ is a conjunction of concept names from
$\mathsf{sig}(\mathcal{T})$. We keep only the ‘strongest’ such axioms, i.e.
those for which there does not exist an entailed axioms
$C_{a}\sqsubseteq\exists R^{\prime}.D^{\prime}$ where $R^{\prime}$ (resp.
$D^{\prime}$) contains a superset of role (resp. concept) names, and at least
one of these superset relationships is strict. It is not hard to show that
there can be at most $|\mathcal{T}|$ strongest axioms, one for each
existential restriction on the right-hand side of an inclusion in
$\mathcal{T}$. If $C_{a}\sqsubseteq\exists R.D$ is a strongest entailed axiom,
and there is no $b\in\mathsf{Ind}(\mathcal{A})$ such that
$\mathcal{A},\mathcal{T}\models R(a,b)$ and $\mathcal{A},\mathcal{T}\models
D(b)$, then we pick a fresh individual $c$ and add the following assertions:
$\\{r(a,c)\mid r\in R\\}\cup\\{A(c)\mid A\in D\\}$. For each of the newly
introduced individuals, we proceed in exactly the same manner to construct its
successors, stopping when an individual has no successors, or when the
individual occurs at distance $|q|$ from one of the original individuals.
Since the number of successors of an individual is bounded by $|\mathcal{T}|$,
and we stop producing successors at depth $|q|$, we only introduce
exponentially many individuals. Moreover, to decide which successors to add
(and which concepts and roles they should satisfy), we perform at most
exponentially many entailment checks, and every such check can be performed in
exponential time.

###  D.3 Transfer sequences for frontier individuals

We next formally introduce the generalized notion of transfer sequence, as
well as the candidate transfer sequences that we guess in Step 1.

Consider an arbitrary pseudo tree ABox $\mathcal{A}$. We call a set of
individuals $\\{u_{1},\ldots,u_{\ell}\\}\subseteq\mathsf{Ind}(\mathcal{A})$ a
_valid frontier for $\mathcal{A}$_ if there do not exist $u_{i}\neq u_{j}$
such that $u_{i}$ is a descendant of $u_{j}$ in one of the tree-shaped ABoxes
of $\mathcal{A}$. If $\mathcal{U}=\\{u_{1},\ldots,u_{\ell}\\}$ is a valid
frontier for $\mathcal{A}$, then we use $\mathcal{A}_{\mathcal{U}}^{\uparrow}$
to denote the ABox obtained from $\mathcal{A}$ by dropping the subtrees
$\mathcal{A}_{u_{1}}^{\downarrow}$, $\ldots$,
$\mathcal{A}_{u_{\ell}}^{\downarrow}$ from $\mathcal{A}$, excepting the
individuals $u_{1},\ldots,u_{\ell}$. Slightly abusing notation, we will extend
the notation ${\sf AT}_{\mathcal{A}}^{\vdash}$ to sets of individuals as
follows:

${\sf AT}_{\mathcal{A},\mathcal{T}}^{\vdash}(\mathcal{U}):=\\{A(u)\mid
u\in\mathcal{U},A(u)\in\mathcal{A}^{c}_{\mathcal{T}}\\}.$

(Note that we add $\mathcal{T}$ to the subscript to make clear which TBox was
used to complete $\mathcal{A}$.)

If $\mathcal{U}=\\{u_{1},\ldots,u_{\ell}\\}$ is a valid frontier for
$\mathcal{A}$, then the _transfer sequence
$\mathcal{X}_{0},\mathcal{X}_{1},\ldots$ of $(\mathcal{A},\mathcal{U})$ w. r.
t. $\mathcal{T}$_ is defined inductively as follows:

  * •

$\mathcal{X}_{0}={\sf AT}_{\mathcal{A}^{0}}^{\vdash}(\mathcal{U})$, where
$\mathcal{A}^{0}=\mathcal{A}_{\mathcal{U}}^{\uparrow}$;

  * •

$\mathcal{X}_{1}={\sf AT}_{\mathcal{A}^{1}}^{\vdash}(\mathcal{U})$, where
$\mathcal{A}^{1}=\bigcup_{u\in\mathcal{U}}\mathcal{A}_{u}^{\downarrow}\cup\mathcal{X}_{0}$;

  * •

for $i\geq 0$, $\mathcal{X}_{2i+2}={\sf
AT}_{\mathcal{A}^{2i+2}}^{\vdash}(\mathcal{U})$, where
$\mathcal{A}^{2i+2}=\mathcal{A}^{2i}\cup\mathcal{X}_{2i+1}$ (equivalently:
$\mathcal{A}^{2i+2}=\mathcal{A}_{\mathcal{U}}^{\uparrow}\cup\mathcal{X}_{2i+1}$);

  * •

for $i\geq 1$, $\mathcal{X}_{2i+1}={\sf
AT}_{\mathcal{A}^{2i+1}}^{\vdash}(\mathcal{U})$, where
$\mathcal{A}^{2i+1}=\mathcal{A}^{2i-1}\cup\mathcal{X}_{2i}$ (equivalently:
$\mathcal{A}^{2i+1}=\bigcup_{u\in\mathcal{U}}\mathcal{A}_{u}^{\downarrow}\cup\mathcal{X}_{2i}$).

An analogue of Lemma 26 can be shown:

######  Lemma 40.

Let $N=(|\mathcal{U}|\cdot|\mathsf{sig}(\mathcal{T})|)+1$. Then
$\mathcal{X}_{N}=\mathcal{X}_{N^{\prime}}$ for all $N^{\prime}>N$ and
$(\mathcal{A}^{N-1})^{c}_{\mathcal{T}}\cup(\mathcal{A}^{N})^{c}_{\mathcal{T}}=\mathcal{A}_{\mathcal{T}}^{c}$.

By _candidate transfer sequence_ for $(\mathcal{U},\mathcal{T})$ we mean a
sequence $\mathcal{X}_{0},\mathcal{X}_{1},\ldots,\mathcal{X}_{N}$ such that
$N=(|\mathcal{U}|\cdot|\mathsf{sig}(\mathcal{T})|)+1$ and for every $j\geq 0$,
$\mathcal{X}_{j}\subseteq\\{A(u_{i})\mid A\in{\sf
N_{C}}\cap\mathsf{sig}(\mathcal{T}),u_{i}\in\mathcal{U}\\}$ and
$\mathcal{X}_{j}\subseteq\mathcal{X}_{j+1}$. In our procedure, we consider
candidate transfer sequences for $(\mathcal{U}_{q},\mathcal{T}_{1})$ and
$(\mathcal{U}_{q},\mathcal{T}_{2})$, which will terminate by the indices
$N_{1}=(|\mathcal{U}_{q}|\cdot|\mathsf{sig}(\mathcal{T}_{1})|)+1$ and
$N_{2}=(|\mathcal{U}_{q}|\cdot|\mathsf{sig}(\mathcal{T}_{2})|)+1$,
respectively. Observe that $|\mathcal{U}_{q}|\leq|\mathcal{T}_{i}|^{m_{q}}$,
so $N_{i}$ is polynomial in $|\mathcal{T}_{i}|$ and exponential in
$\mathsf{max}(|q_{1}|,|q_{2}|)$.

###  D.4 Compatibility of candidate transfer sequences

Let $\mathcal{A}$ be a pseudo tree ABox and $\mathcal{B}\supseteq\mathcal{A}$
be an ABox with $\mathcal{B}\setminus\mathcal{A}\subseteq\\{B(a)\mid
a\in\mathsf{Ind}(\mathcal{A}),B\in{\sf N_{C}}\\}$. Further let
$\mathcal{U}\subseteq\mathsf{Ind}(\mathcal{A})$ be a subset of the leaves of
$\mathcal{A}$ (i.e. individuals occurring in one of the trees of $\mathcal{A}$
but without any successors), and let
$\mathcal{X}=\mathcal{X}_{0},\mathcal{X}_{1},\ldots,\mathcal{X}_{N}$ be a
candidate transfer sequence for $(\mathcal{U},\mathcal{T})$. We say that
$\mathcal{X}$ is _compatible with ( $\mathcal{A}$, $\mathcal{B}$) w.r.t.
$(\mathcal{U},\mathcal{T})$_ iff:

  1. 1.

$\mathcal{X}_{0}={\sf
AT}_{\mathcal{A}^{0},\mathcal{T}}^{\vdash}(\mathcal{U})$, where
$\mathcal{D}^{0}=\mathcal{A}$;

  2. 2.

for every $i\geq 0$ with $2i+2<N$:
$\mathcal{X}_{2i+2}={\sf
AT}_{\mathcal{A}^{2i+2},\mathcal{T}}^{\vdash}(\mathcal{U})$ where
$\mathcal{D}^{2i+2}=\mathcal{A}\cup\mathcal{X}_{2i+1}$;

  3. 3.

$\mathcal{X}_{N}=\\{A(u)\in\mathcal{B}\mid u\in\mathcal{U}\\}$;

  4. 4.

for every $B(a)$ with $a\in\mathsf{Ind}(\mathcal{A})$ and $B\in{\sf N_{C}}$:
$B(a)\in\mathcal{B}$ iff $\mathcal{T},\mathcal{A}\cup\mathcal{X}_{N}\models
B(a)$

Checking compatibility of a candidate transfer sequence w.r.t. a pair of
ABoxes can be decided in ExpTime. Indeed, all four conditions involve
computing the closure of an exponential-sized ABox w.r.t. $\mathcal{T}$, which
can be done in exponential time. Indeed, there are only exponentially many
concept assertions that can be added, so only exponentially many rule
applications are needed to reach the closure, and finding the next rule to
apply involves an exponential number of (ExpTime) entailment checks.

Next let $u\in\mathcal{U}$, and let $\mathcal{G}$ be a tree-shaped ABox with
root $u$. We say that $\mathcal{X}$ is _compatible with $\mathcal{G}$ at $u$
w.r.t. $\mathcal{T}$_ if and only if:

  * •

$\mathcal{X}_{1}(u)={\sf AT}_{\mathcal{D}^{1},\mathcal{T}}^{\vdash}(u)$ where
$\mathcal{D}^{1}=\mathcal{G}\cup\mathcal{X}_{0}(u)$

  * •

for every $i\geq 1$ with $2i+1\leq N$: $\mathcal{X}_{2i+1}(u)={\sf
AT}_{\mathcal{D}^{2i+1},\mathcal{T}}^{\vdash}(u)$, where
$\mathcal{D}^{2i+1}=\mathcal{G}\cup\mathcal{X}_{2i}(u)$

where, slightly abusing notation, we use the notation $\mathcal{X}_{i}(u)$ to
mean the set $\\{A(u)\mid A(u)\in\mathcal{X}_{i}\\}$.

###  D.5 Automata construction

Let $\mathcal{A}$ be the guessed pseudo tree ABox, let $\mathcal{Y}^{1}$ and
$\mathcal{Y}^{2}$ be the guessed candidate transfer sequences for
$(\mathcal{U}_{q},\mathcal{T}_{1})$ and $(\mathcal{U}_{q},\mathcal{T}_{2})$
respectively, and let $\mathcal{U}_{q}=\\{u_{1},\ldots,u_{\ell_{q}}\\}$.

To implement Step 3 of the procedure, we need to construct, for every $1\leq
j\leq\ell_{q}$, a TWAPA $\mathfrak{A}_{j}$ that accepts encodings of tree-
shaped ABoxes $\mathcal{G}_{j}$ with root node $u_{j}$ satisfying the
conditions of Proposition 41. The desired automaton $\mathfrak{A}_{j}$ can be
obtained by intersecting the following automaton:

  * •

$\mathfrak{A}_{\mathsf{cons}}$ that ensures that the encoded ABox is
consistent with the TBoxes $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$.

  * •

$\mathfrak{A}_{\mathsf{funct}}$ that ensures that the encoded ABox, when added
to the ABox $\mathcal{A}$, does not violate the functionality assertions in
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$. Specifically, we need to ensure that
if $\mathsf{func}(r)\in\mathcal{T}_{k}$ ($k\in\\{1,2\\}$) and
$r(u_{j},u^{\prime})\in\mathcal{A}$, then the encoded ABox (whose root
individual is $u_{j}$) does not contain any assertion of the form
$r(u_{j},u^{\prime\prime})$.

  * •

for every $1\leq 2i+1\leq N$ and $k\in\\{1,2\\}$, an automaton
$\mathfrak{A}^{\mathcal{Y}^{k}}_{2i+1}$ that determines whether
$\mathcal{Y}_{2i+1}^{k}(u_{j})$ is precisely the set of concept assertions
about $u_{j}$ that are entailed from $\mathcal{T}$, the encoded ABox, and the
assertions in $\mathcal{Y}_{2i}^{k}(u_{j})$.

Note that the automaton $\mathfrak{A}^{\mathcal{Y}^{k}}_{2i+1}$ in the third
item can be constructed by intersecting automata that check whether a given
concept assertion $A(u_{j})\in\mathcal{Y}_{2i+1}^{k}(u_{j})$ is entailed with
those checking that each concept assertion
$A(u_{j})\not\in\mathcal{Y}_{2i+1}^{k}(u_{j})$ (with $A\in{\sf
N_{C}}\cap\mathsf{sig}(\mathcal{T})$) is not entailed. Moreover, the automata
checking whether a concept is not entailed at the root $u_{j}$ can be obtained
by complementing the automaton that accepts trees in which the concept is
entailed at the root.

Importantly, because the sets $\mathcal{Y}_{i}(u_{j})$ increase monotonically
and only contain concept assertions about the individual $u_{j}$, there are
only _polynomially many_ different elements in the set
$\\{(\mathcal{Y}_{2i+1}(u_{j}),\mathcal{Y}_{2i}(u_{j}))\mid 1\leq 2i+1\leq
N\\}$. It follows that $\mathfrak{A}_{j}$ can be obtained by _intersecting a
polynomial number of automata_. Moreover, it is not hard to see that each of
the component automata can be _constructed in polynomial time_. Since there
are (at most) single exponentially many elements in $\mathcal{U}_{q}$, and
emptiness of TWAPAs can be tested in single-exponential time, it follows that
Step 3 can be performed in ExpTime.

###  D.6 Correctness of the procedure

We have already given the main lines of the argument in the overview, so here
we concentrate on the following proposition, which is the key step to
establishing correctness.

######  Proposition 41.

Let $\mathcal{A}$ be a pseudo tree ABox, let $\mathcal{B}\supseteq\mathcal{A}$
be an ABox with $\mathcal{B}\setminus\mathcal{A}\subseteq\\{B(a)\mid
a\in\mathsf{Ind}(\mathcal{A}),B\in{\sf N_{C}}\\}$ that is consistent with
$\mathcal{T}$, and let
$\mathcal{U}=\\{u_{1},\ldots,u_{\ell}\\}\subseteq\mathsf{Ind}(\mathcal{A})$ be
a subset of the leaves in $\mathcal{A}$. Suppose that

  1. 1.

the candidate transfer sequence
$\mathcal{X}=\mathcal{X}_{0},\ldots,\mathcal{X}_{N}$ is compatible with
$(\mathcal{A},\mathcal{B})$ w.r.t. $(\mathcal{U},\mathcal{T})$, and

  2. 2.

there exist tree-shaped ABoxes $\mathcal{G}_{1},\ldots,\mathcal{G}_{\ell}$
such that
$\mathsf{Ind}(\mathcal{G}_{j})\cap\mathsf{Ind}(\mathcal{G}_{j}^{\prime})=\emptyset$
for every $j\neq j^{\prime}$ and for every $1\leq j\leq\ell$:

     * •

$\mathsf{Ind}(\mathcal{A})\cap\mathsf{Ind}(\mathcal{G}_{j})=\\{u_{j}\\}$,

     * •

$\mathcal{G}_{j}$ does not contain any concept assertion $A(u_{j})$,

     * •

$\mathcal{G}_{j}\cup\mathcal{X}_{N}$ is consistent with $\mathcal{T}$,

     * •

$\mathcal{A}\cup\mathcal{G}_{j}$ does not violate any functionality assertion
in $\mathcal{T}$,

     * •

$\mathcal{G}_{j}$ is compatible with $\mathcal{X}$ at $u_{j}$ w.r.t.
$\mathcal{T}$.

Let $\mathcal{A}^{*}=\mathcal{A}\cup\bigcup_{1\leq j\leq\ell}\mathcal{G}_{j}$.
Then:

  * •

$\mathcal{A}^{*}$ is consistent with $\mathcal{T}$,

  * •

$\mathcal{X}$ is the transfer sequence for
$(\mathcal{A}^{*},\\{u_{1},\ldots,u_{\ell}\\})$, and

  * •

$\mathcal{T},\mathcal{A}^{*}\models A(a)$ iff $A(a)\in\mathcal{B}$ (for
$a\in\mathsf{Ind}(\mathcal{A})$, $A\in{\sf N_{C}}$)

###### Proof.

Let
$\mathcal{A},\mathcal{B},\mathcal{G}_{1},\ldots,\mathcal{G}_{\ell},\mathcal{U},\mathcal{T},\mathcal{X}$
be as in the statement.

To show consistency of $\mathcal{A}^{*}$ with $\mathcal{T}$, first note that
$\mathcal{A}^{*}$ does not violate any functionality assertions in
$\mathcal{T}$, since each of the ABoxes
$\mathcal{A},\mathcal{G}_{1},\ldots,\mathcal{G}_{\ell}$ is consistent with
$\mathcal{T}$, there is no individual shared by two different
$\mathcal{G}_{j}$, and by assumption, for every $1\leq j\leq\ell$, the ABox
$\mathcal{A}\cup\mathcal{G}_{j}$ does not violate any functionality assertion
in $\mathcal{T}$.

Let $\mathcal{A}^{+}=\mathcal{A}\cup\mathcal{X}_{N}$, and let
$\mathcal{G}_{j}^{+}=\mathcal{G}_{j}\cup\mathcal{X}_{N}(u_{j})$ for $1\leq
j\leq\ell$. We know that each of the ABoxes
$\mathcal{A}^{+},\mathcal{G}_{1}^{+},\ldots,\mathcal{G}_{\ell}^{+}$ is
consistent with $\mathcal{T}$, and hence possesses a canonical model. We let
$\mathcal{I}_{\mathcal{A}^{+},\mathcal{T}}$ and
$\mathcal{I}_{\mathcal{G}_{j}^{+},\mathcal{T}}$ be the canonical models for
$\mathcal{A}^{+},\mathcal{T}$ (resp. $\mathcal{G}_{j}^{+},\mathcal{T}$), as
defined in Appendix B.2. Without loss of generality, we may assume that
$\Delta^{\mathcal{I}_{\mathcal{G}_{j},\mathcal{T}}}\cap\Delta^{\mathcal{I}_{\mathcal{G}_{k},\mathcal{T}}}=\emptyset$
for every $j\neq k$, and that
$\Delta^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}\cap\Delta^{\mathcal{I}_{\mathcal{G}_{j},\mathcal{T}}}=\emptyset$
for every $1\leq j\leq\ell$. We recall that these interpretations can be seen
as adding to the original ABox all entailed assertions about the ABox
individuals, and additionally attaching weakly tree-shaped interpretations to
each of the ABox individuals in order to witness the existential restrictions
on the right-hand side of TBox axioms. For every $u_{j}\in\mathcal{U}$, we let
$\mathcal{I}_{j}^{\mathcal{A}}$ (resp. $\mathcal{I}_{j}^{\mathcal{G}}$) be the
weakly tree-shaped interpretation that is attached to the individual $u_{j}$
in $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ (resp.
$\mathcal{I}_{\mathcal{G}_{k},\mathcal{T}}$). Define the interpretation
$\mathcal{J}$ as the union of the interpretations
$\mathcal{A}^{+},\mathcal{G}_{1}^{+},\ldots,\mathcal{G}_{\ell}^{+}$:

  * •

$\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}\cup\bigcup_{1\leq
j\leq\ell}\Delta^{\mathcal{I}_{\mathcal{G}_{j},\mathcal{T}}}$

  * •

for every $A\in{\sf N_{C}}$:
$A^{\mathcal{J}}=A^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}\cup\bigcup_{1\leq
j\leq\ell}A^{\mathcal{I}_{\mathcal{G}_{j},\mathcal{T}}}$

  * •

for every $r\in{\sf N_{R}}$:
$r^{\mathcal{J}}=r^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}\cup\bigcup_{1\leq
j\leq\ell}r^{\mathcal{I}_{\mathcal{G}_{j},\mathcal{T}}}$

To satisfy the functionality assertions, we proceed as follows. For every
$u_{j}\in\mathcal{U}$ and functional role $R$:

  * •

If $u_{j}\in\exists R^{\mathcal{I}_{\mathcal{A}^{+},\mathcal{T}}}$ and there
is no $b$ such that $\mathcal{A}^{+},\mathcal{T}\models R(u_{j},b)$, then let
$e$ be the unique element in $\Delta^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}$
such that $(u_{j},e)\in R^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}$. This
element must belong to the weakly tree-shaped subinterpretation
$\mathcal{I}_{j}^{\mathcal{A}}$. Remove the element $e$ and all of its
descendants in $\mathcal{I}_{j}^{\mathcal{A}}$ from $\Delta^{\mathcal{J}}$.

  * •

If $u_{j}\in\exists R^{\mathcal{I}_{\mathcal{G}_{j}^{+},\mathcal{T}}}$ and
there is no $b$ such that $\mathcal{G}_{j}^{+},\mathcal{T}\models R(u_{j},b)$,
then let $e$ be the unique element in
$\Delta^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}$ such that $(u_{j},e)\in
R^{\mathcal{I}_{\mathcal{G}_{j}^{+},\mathcal{T}}}$. This element must belong
to the weakly tree-shaped subinterpretation $\mathcal{I}_{j}^{\mathcal{G}}$.
Remove the element $e$ and all of its descendants in
$\mathcal{I}_{j}^{\mathcal{G}}$ from $\Delta^{\mathcal{J}}$.

Call the resulting interpretation $\mathcal{J}^{-}$. We claim that
$\mathcal{J}^{-}$ is a model of $\mathcal{A}^{*}$ and $\mathcal{T}$. First
observe that $\mathcal{J}^{-}$ makes true all ABox assertions in
$\mathcal{A}^{*}$, since $\mathcal{J}$ satisfies this property and the
modifications that were made to $\mathcal{J}$ only involve elements that did
not occur in the original ABoxes. Because of our modifications, we have
resolved all of the violations of functionality axioms that were introduced
when combining the interpretations. It can also be easily seen that axioms of
the forms $A\sqsubseteq\bot$, $\top\sqsubseteq A$, $B_{1}\sqcap
B_{2}\sqsubseteq A$, and $\exists r.B\sqsubseteq A$ are all satisfied in
$\mathcal{J}^{-}$, since they were satisfied in each of the interpretations
$\mathcal{I}_{\mathcal{A}^{+},\mathcal{T}}$,
$\mathcal{I}_{\mathcal{G}_{j}^{+},\mathcal{T}}$, $\ldots$,
$\mathcal{I}_{\mathcal{G}_{j}^{+},\mathcal{T}}$. Finally, if $e\in
A^{\mathcal{J}^{-}}$ and $A\sqsubseteq\exists r.B\in\mathcal{T}$, then either
we have the same witnessing $r$-successor $e^{\prime}$ as was used in the
component interpretation containing the element $e$, or $e\in\mathcal{U}$, and
we were only allowed to remove $e^{\prime}$ (and the whole tree-shaped
interpretation rooted at $e^{\prime}$) because in the ABox $\mathcal{A}^{*}$,
there was an ABox individual that acted as the witnessing $r$-successor. (and
which is present in $\mathcal{J}^{-}$) Thus, $\mathcal{J}^{-}$ is a model of
$\mathcal{A}^{*},\mathcal{T}$, so $\mathcal{A}^{*}$ is consistent with
$\mathcal{T}$.

We next prove by induction that
$\mathcal{X}=\mathcal{X}_{0},\ldots,\mathcal{X}_{n}$ is the transfer sequence
for $(\mathcal{A}^{*},\mathcal{U})$. We start by considering the first set in
the sequence ($\mathcal{X}_{0}$). We know that $\mathcal{X}_{0}={\sf
AT}_{\mathcal{A},\mathcal{T}}^{\vdash}(\mathcal{U})$ since $\mathcal{X}$ is
compatible with $(\mathcal{A},\mathcal{B})$ w.r.t.
$(\mathcal{U},\mathcal{T})$. We then use the fact that, for every $1\leq
j\leq\ell$, the ABox $\mathcal{G}_{j}$ is such that
$\mathsf{Ind}(\mathcal{A})\cap\mathsf{Ind}(\mathcal{G}_{j})=\\{u_{j}\\}$ and
does not contain any assertion $A(u_{j})$ to infer that
$(\mathcal{A}^{*})^{\uparrow}_{\mathcal{U}}=\mathcal{A}$. Thus,
$\mathcal{X}_{0}$ is the first element in the transfer sequence for
$(\mathcal{A}^{*},\mathcal{U})$.

For the second element $\mathcal{X}_{1}$, we first note that, for every $0\leq
i\leq n$, $\mathcal{X}_{i}=\bigcup_{1\leq j\leq\ell}\mathcal{X}_{i}(u_{j})$.
Further note that for every $1\leq j\leq\ell$, by the compatibility of
$\mathcal{X}$ with $\mathcal{G}_{j}$ at $u_{j}$, we have
$\mathcal{X}_{1}(u_{j})={\sf
AT}_{\mathcal{D}^{1}_{j},\mathcal{T}}^{\vdash}(u_{j})$ where
$\mathcal{D}^{1}_{j}=\mathcal{G}_{j}\cup\mathcal{X}_{0}(u_{j})$. Let
$\mathcal{D}^{1}=\bigcup_{1\leq j\leq\ell}\mathcal{D}^{1}_{j}$. Since
$\mathsf{Ind}(\mathcal{D}^{1}_{j})=\mathsf{Ind}(\mathcal{G}_{j})$ and we know
that
$\mathsf{Ind}(\mathcal{G}_{j})\cap\mathsf{Ind}(\mathcal{G}_{j}^{\prime})=\emptyset$
for every $j\neq j^{\prime}$, it follows that ${\sf
AT}_{\mathcal{D}^{1}_{j},\mathcal{T}}^{\vdash}(u_{j})={\sf
AT}_{\mathcal{D}^{1},\mathcal{T}}^{\vdash}(u_{j})$, and hence that
$\mathcal{X}_{1}={\sf
AT}_{\mathcal{D}^{1},\mathcal{T}}^{\vdash}(\mathcal{U})$. Finally, we note
that since $(\mathcal{A}^{*})^{\downarrow}_{u_{j}}=\mathcal{G}_{j}$, we have
that $(\mathcal{A}^{*})^{\downarrow}_{\mathcal{U}}=\bigcup_{1\leq
j\leq\ell}\mathcal{G}_{j}$, and thus
$\mathcal{D}^{1}=(\mathcal{A}^{*})^{\downarrow}_{\mathcal{U}}\cup\mathcal{X}_{0}$,
which shows that $\mathcal{X}_{1}$ is as desired.

Next consider an index $1<2i+2\leq N$. As we know that $\mathcal{X}$ is
compatible with $(\mathcal{A},\mathcal{B})$ w.r.t.
$(\mathcal{U},\mathcal{T})$, we can infer that $\mathcal{X}_{2i+2}={\sf
AT}_{\mathcal{D}^{2i+2},\mathcal{T}}^{\vdash}(\mathcal{U})$ where
$\mathcal{D}^{2i+2}=\mathcal{A}\cup\mathcal{X}_{2i+1}$. Since
$(\mathcal{A}^{*})^{\uparrow}_{\mathcal{U}}=\mathcal{A}$, it follows that
$\mathcal{X}_{2i+2}$ is the correct $2i+2$th element in the transfer sequence
for $(\mathcal{A}^{*},\mathcal{U})$.

Finally consider an index $0<2i+1\leq N$. We know that for every $1\leq
j\leq\ell$, the ABox $\mathcal{G}_{j}$ is compatible with $\mathcal{X}$ at
$u_{j}$ w.r.t. $\mathcal{T}$, so we have $\mathcal{X}_{2i+1}(u)={\sf
AT}_{\mathcal{D}^{2i+1}_{j},\mathcal{T}}^{\vdash}(u)$, where
$\mathcal{D}^{2i+1}_{j}=\mathcal{G}_{j}\cup\mathcal{X}_{2i}(u)$. Let
$\mathcal{D}^{2i+1}=\bigcup_{1\leq j\leq\ell}\mathcal{D}^{2i+1}_{j}$. Using
the same arguments as for $\mathcal{X}_{1}$, we can show that
$\mathcal{X}_{2i+1}={\sf
AT}_{\mathcal{D}^{2i+1},\mathcal{T}}^{\vdash}(\mathcal{U})$ and that
$\mathcal{D}^{2i+1}=(\mathcal{A}^{*})^{\downarrow}_{\mathcal{U}}\cup\mathcal{X}_{2i}$,
as required.

Now we show the third point. For the right-to-left direction, we note that
since $\mathcal{X}$ is compatible with ($\mathcal{A}$, $\mathcal{B}$) w.r.t.
$(\mathcal{U},\mathcal{T})$, we have
$\mathcal{T},\mathcal{A}\cup\mathcal{X}_{N}\models B(a)$ for every
$B(a)\in\mathcal{B}$. Since $\mathcal{X}$ is the transfer sequence for
$\mathcal{A}^{*}$ w.r.t. $\mathcal{T}$, we must have
$\mathcal{A}^{*},\mathcal{T}\models\mathcal{X}_{N}$, and by definition,
$\mathcal{A}^{*}$ contains $\mathcal{A}$. It follows that
$\mathcal{T},\mathcal{A}^{*}\models B(a)$ for every $B(a)\in\mathcal{B}$.

For the left-to-right direction, suppose that
$\mathcal{T},\mathcal{A}^{*}\models B(a)$, where
$a\in\mathsf{Ind}(\mathcal{A})$ and $B\in{\sf N_{C}}$. Then
$B(a)\in(\mathcal{A}^{*})^{c}_{\mathcal{T}}$. As $\mathcal{X}$ is the transfer
sequence for $(\mathcal{A}^{*},\mathcal{U})$, it follows from Lemma 40 that we
have
$(\mathcal{A}^{*})^{c}_{\mathcal{T}}=(\mathcal{D}_{N-1})^{c}_{\mathcal{T}}\cup(\mathcal{D}_{N})^{c}_{\mathcal{T}}$
where
$\mathcal{D}_{N-1}=(\mathcal{A}^{*})^{\downarrow}_{\mathcal{U}}\cup\mathcal{X}_{N-1}$
and
$\mathcal{D}_{N}=(\mathcal{A}^{*})^{\uparrow}_{\mathcal{U}}\cup\mathcal{X}_{N}$.
First suppose that $B(a)\in(\mathcal{D}_{N})^{c}_{\mathcal{T}}$. Since
$(\mathcal{A}^{*})^{\uparrow}_{\mathcal{U}}=\mathcal{A}$, we have
$\mathcal{D}_{N}=\mathcal{A}\cup\mathcal{X}_{N-1}$, so
$\mathcal{T},\mathcal{A}\cup\mathcal{X}_{N-1}\models B(a)$. As
$\mathcal{X}_{N-1}\subseteq\mathcal{X}_{N}$, we also have
$\mathcal{T},\mathcal{A}\cup\mathcal{X}_{N-1}\models B(a)$, which implies
$B(a)\in\mathcal{B}$, due to the fourth condition of compatibility of
$\mathcal{X}$ with ($\mathcal{A}$, $\mathcal{B}$) w.r.t.
$(\mathcal{U},\mathcal{T})$. Now consider the case in which
$B(a)\in(\mathcal{D}_{N-1})^{c}_{\mathcal{T}}$, but
$B(a)\not\in(\mathcal{D}_{N})^{c}_{\mathcal{T}}$. Since
$\mathcal{D}_{N-1}=(\mathcal{A}^{*})^{\downarrow}_{\mathcal{U}}\cup\mathcal{X}_{N-2}$,
we must have $a\in\mathcal{U}$, and from
$B(a)\in(\mathcal{D}_{N-1})^{c}_{\mathcal{T}}$, we obtain
$B(a)\in\mathcal{X}_{N-1}$. It follows that $B(a)\in\mathcal{D}^{N}$, which
contradicts our assumption that
$B(a)\not\in(\mathcal{D}_{N})^{c}_{\mathcal{T}}$. ∎

###  D.7 Upper bound for FO-rewritability

We aim to prove the following:

######  Theorem 42.

FO-rewritability in ($\mathcal{ELIHF}_{\bot}$, rCQ) is in coNExpTime.

By Lemma 28, we know that $(\mathcal{T},\Sigma,q(\mathbf{x}))$ is _not_ FO-
rewritable iff there exists a $k_{0}$-entailment witness for $\mathcal{T}$,
$\Sigma$, and $q(\mathbf{x})$ of outdegree bounded by $|\mathcal{T}|$ for
$k_{0}=|q|+2^{3m^{2}}$ where $m=|\mathcal{T}|$. Thus, it suffices to provide
an NExpTime procedure for deciding whether such a witness exists.

The procedure will be quite similar to the NExpTime procedure for testing non-
containment of rooted queries. In what follows, we outline the main
differences.

In Step 1, the guessed ABox $\mathcal{A}_{\mathsf{init}}$ corresponds to
initial portion of the $k_{0}$-entailment witness (up to depth $|q|$), the
tuple $\mathbf{a}$ is the answer tuple associated with the witness, and we
take $\mathcal{U}_{q}$ to be the set of individuals that occur in
$\mathcal{A}_{\mathsf{init}}$ at depth $|q|$. In place of the ABoxes
$\mathcal{B}_{1}$ and $\mathcal{B}_{2}$, we guess two ABoxes $\mathcal{B}$ and
$\mathcal{B}_{k_{0}}$, with the former being used for the concept assertions
involving the individuals in $\mathcal{A}_{\mathsf{init}}$ that hold in the
full entailment witness (i.e. once we have added back the missing trees), and
the latter containing only those assertions that can be obtained using the
entailment witness cut off at depth $k_{0}$. We also guess two candidate
transfer sequences $\mathcal{Y}=\mathcal{Y}_{0},\ldots,\mathcal{Y}_{N}$ and
$\mathcal{Z}=\mathcal{Z}_{0},\ldots,\mathcal{Z}_{N}$ (with
$N=(|\mathcal{U}|\cdot|\mathsf{sig}(\mathcal{T})|)+1$), both with respect to
$(\mathcal{U}_{q},\mathcal{T})$. The first sequence $\mathcal{Y}$ is intended
to track concept entailments w.r.t. the full entailment witness, and the
second is for the ABox obtained by restricting the entailment witness to those
individuals that occur at depth $k_{0}$ or less.

In Step 2, we test whether $\mathcal{T},\mathcal{B}\models q(\mathbf{a})$ and
$\mathcal{T},\mathcal{B}_{k_{0}}\not\models q(\mathbf{a})$. We also verify
that the first candidate transfer sequence $\mathcal{Y}$ is compatible with
$(\mathcal{A}_{\mathsf{init}},\mathcal{B})$ and the second candidate transfer
sequence $\mathcal{Z}$ is compatible with
$(\mathcal{A}_{\mathsf{init}},\mathcal{B}_{k_{0}})$.

In Step 3, for each $u_{j}\in U_{q}$, we build an automaton $\mathfrak{A}_{j}$
that accepts (encodings of) pseudo tree ABoxes $\mathcal{G}_{j}$ such that:

  * •

$\mathsf{Ind}(\mathcal{A}_{\mathsf{init}})\cap\mathsf{Ind}(\mathcal{G}_{j})=\\{u_{j}\\}$,

  * •

$\mathcal{G}_{j}$ is consistent with $\mathcal{T}$,

  * •

$\mathcal{A}_{\mathsf{init}}\cup\mathcal{G}_{j}$ does not violate any
functionality assertion in $\mathcal{T}$,

  * •

$\mathcal{G}_{j}$ is compatible with $\mathcal{Y}$ at $u_{j}$ w.r.t.
$\mathcal{T}$,

  * •

$\mathcal{G}_{j}|_{\leq k_{0}-|q|}$ is compatible with $\mathcal{Z}$ at
$u_{j}$ w.r.t. $\mathcal{T}$.

Note that in the last item, we cut off $\mathcal{G}_{j}$ at depth $k_{0}-|q|$
so that when we attach it to $\mathcal{A}_{\mathsf{init}}$ (in which $u_{j}$
occurs at depth $|q|$), we obtain an ABox having depth $k_{0}$.

Using similar arguments as for containment, we can show that the modified
procedure runs in NExpTime and it returns yes just in the case that
$(\mathcal{T},\Sigma,q(\mathbf{x}))$ is not FO-rewritable.

##  Appendix E Lower bounds

###  E.1 coNExpTime lower bounds for rooted CQs

An _(exponential torus) tiling problem_ $P$ is a triple $(T,H,V)$, where
$T=\\{0,\dots,k\\}$ is a finite set of _tile types_ and $H,V\subseteq T\times
T$ represent the _horizontal and vertical matching conditions_. An _initial
condition_ for $P$ takes the form $c=(c_{0},\dots,c_{n-1})\in T^{n}$. A
mapping $\tau:\\{0,\dots,2^{n}-1\\}\times\\{0,\dots,2^{n}-1\\}\to T$ is a
_solution_ for $P$ given $c$ if for all $x,y<2^{n}$, the following holds
(where $\oplus_{i}$ denotes addition modulo $i$):

  * •

if $\tau(x,y)=t_{1}$ and $\tau(x\oplus_{2^{n}}1,y)=t_{2}$, then
$(t_{1},t_{2})\in H$

  * •

if $\tau(x,y)=t_{1}$ and $\tau(x,y\oplus_{2^{n}}1)=t_{2}$, then
$(t_{1},t_{2})\in V$

  * •

$\tau(i,0)=c_{i}$ for all $i<n$.

It is well-known that there exists a tiling problem $P=(T,H,V)$ such that,
given an initial condition $c$, it is NExpTime-complete to decide whether
there exists a solution for $P$ given $c$. For the following constructions, we
fix such a $P$.

######  Lemma 43.

Given an input $c$ for $P$ of length $n$, one can construct in polynomial time
an $\mathcal{E\kern-1.00006ptLI}$ TBox $\mathcal{T}_{c}$, a rooted CQ
$q_{c}(x)$, and an ABox signature $\Sigma_{c}$ such that, for a selected
concept name $A^{*}\notin\Sigma_{c}$,

  1. 1.

$P$ has a solution given $c$ iff there is a $\Sigma_{c}$-ABox $\mathcal{A}$
and an $a\in\mathsf{Ind}(\mathcal{A})$ such that
$\mathcal{A},\mathcal{T}_{c}\models A^{*}(a)$ and
$\mathcal{A},\mathcal{T}_{c}\not\models q_{c}(a)$;

  2. 2.

there is an $\mathcal{E\kern-1.00006ptLI}$-concept $C_{q_{c}}$ such that $d\in
C_{q_{c}}^{\mathcal{I}}$ implies $\mathcal{I}\models q_{c}(d)$ for all
interpretations $\mathcal{I}$ and $d\in\Delta^{\mathcal{I}}$;

  3. 3.

$q_{c}$ is FO-rewritable relative to $\mathcal{T}_{c}$ and $\Sigma_{c}$.

We will now prove the containment and FO-rewritability lower bounds, assuming
the previous lemma. The proof of the lemma is given in the following
subsection.

######  Theorem 44.

Containment in $(\mathcal{E\kern-1.00006ptLI},\text{rCQ})$ is coNExpTime-hard.

###### Proof.

Let $c$ be an input to $P$, and let $\mathcal{T}_{c}$, $q_{c}(x)$,
$\Sigma_{c}$, and $A^{*}$ be as in Lemma 43. By Condition 1 of Lemma 43,
$(\mathcal{T}_{c},\Sigma_{c},A^{*})\not\subseteq(\mathcal{T}_{c},\Sigma_{c},q_{c})$
over $\Sigma_{c}$-ABoxes iff $P$ has a solution given $c$. ∎

######  Theorem 45.

FO-rewritability in $(\mathcal{E\kern-1.00006ptLI},\text{rCQ})$ is coNExpTime-
hard.

###### Proof.

Let $c$ be an input to $P$, and let $\mathcal{T}_{c}$, $q_{c}(x)$,
$\Sigma_{c}$, and $A^{*}$ be as in Lemma 43. We obtain a TBox $\mathcal{T}$ by
extending $\mathcal{T}_{c}$ with the following:

$\begin{array}[]{rcll}\exists r.A&\sqsubseteq&A\\\\[2.84526pt] A\sqcap
A^{*}&\sqsubseteq&C_{q_{c}}\end{array}$

where $A$ and $r$ do not occur in $\mathcal{T}_{c}$ and $q_{c}$,
$A^{*}\notin\Sigma_{c}$ is the concept name from Lemma 43 and $C_{q_{c}}$ the
concept from Point 2 of that lemma. Set $\Sigma=\Sigma_{c}\cup\\{A,r\\}$. It
remains to prove the following.
Claim. $P$ has a solution given $c$ iff $q_{c}$ is not FO-rewritable relative
to $\mathcal{T}$ and $\Sigma$.
First assume that $P$ has a solution given $c$. By Point 1 of Lemma 43, there
is a $\Sigma_{c}$-ABox $\mathcal{A}$ and an
$a_{0}\in\mathsf{Ind}(\mathcal{A})$ such that
$\mathcal{A},\mathcal{T}_{c}\models A^{*}(a_{0})$ and
$\mathcal{A},\mathcal{T}_{c}\not\models q_{c}(a_{0})$. Since every
$\mathcal{E\kern-1.00006ptLI}$ TBox is unraveling tolerant lutz-2012 and by
compactness, we can assume w.l.o.g. that $\mathcal{A}$ is tree-shaped with
root $a_{0}$. Let $\ell$ be the depth of $\mathcal{A}$. For each $k>\ell$, let
$\mathcal{A}_{k}$ be the ABox obtained by extending $\mathcal{A}$ with

$r(a_{0},a_{1}),\dots,r(a_{k-1},a_{k}),A(a_{k})$

where $a_{k},\dots,a_{1}$ do not occur in $\mathcal{A}$. Note that
$\mathcal{A}_{k}$ is tree-shaped and of depth at least $k$. Since
$\mathcal{A},\mathcal{T}_{c}\models A^{*}(a_{0})$, it follows from Point 2 of
Lemma 43 that $\mathcal{A}_{k},\mathcal{T}\models q_{c}(a_{0})$. Now consider
the ABox $\mathcal{A}_{k}|_{\leq k-1}$. We aim to show that
$\mathcal{A}_{k}|_{\leq k-1},\mathcal{T}\not\models q_{c}(a_{0})$ and then to
apply Theorem 9 to show that $q_{c}$ is not FO-rewritable relative to
$\mathcal{T}$ and $\Sigma$. Note that $\mathcal{A}_{k}|_{\leq k-1}$ does not
contain $A$. On such ABoxes, $\mathcal{T}$ can be replaced with
$\mathcal{T}_{c}$ since the left-hand sides of the concept inclusions in
$\mathcal{T}$ will never apply. It thus suffices to show that
$\mathcal{A}_{k}|_{k-1},\mathcal{T}_{c}\not\models q_{c}(a_{0})$. This follows
from $\mathcal{A},\mathcal{T}_{c}\not\models q_{c}(a_{0})$ and the fact that
$r$ (the only symbol in assertions from
$(\mathcal{A}_{k}|_{k-1})\setminus\mathcal{A}$) occurs neither in
$\mathcal{T}_{c}$ nor in $q_{c}$.

Now assume that $P$ has no solution given $c$. Let $\widehat{q}_{c}(x)$ be an
FO-rewriting of $q_{c}(x)$ relative to $\mathcal{T}_{c}$ and $\Sigma_{c}$. We
argue that $\widehat{q}_{c}(x)$ is also an FO-rewriting of $q_{c}(x)$ relative
to $\mathcal{T}$ and $\Sigma$.

First assume $\mathcal{A}\models\widehat{q}_{c}(a)$ for some $\Sigma$-ABox
$\mathcal{A}$. Since $\widehat{q}_{c}(x)$ uses only symbols from $\Sigma_{c}$,
this means that $\mathcal{A}^{\prime}\models\widehat{q}_{c}(a)$ where
$\mathcal{A}^{\prime}$ is the reduct of $\mathcal{A}$ to symbols in
$\Sigma_{c}$. Thus $\mathcal{A}^{\prime},\mathcal{T}_{c}\models q_{c}(a)$,
implying $\mathcal{A},\mathcal{T}\models q_{c}(a)$.

Conversely, assume that $\mathcal{A},\mathcal{T}\models q_{c}(a)$ for some
$\Sigma$-ABox $\mathcal{A}$ and $a\in\mathsf{Ind}(\mathcal{A})$. Using
canonical models and the construction of $\mathcal{T}$, one can show that this
implies (i) $\mathcal{A},\mathcal{T}_{c}\models q_{c}(a)$ or (ii)
$\mathcal{A},\mathcal{T}_{c}\models A^{*}(a)$. In Case (i), we get
$\mathcal{A}^{\prime},\mathcal{T}_{c}\models q_{c}(a)$, where
$\mathcal{A}^{\prime}$ is the $\Sigma_{c}$-reduct of $\mathcal{A}$. Thus
$\mathcal{A}^{\prime}\models\widehat{q}_{c}(a)$, which implies
$\mathcal{A}\models\widehat{q}_{c}(a)$. In Case (ii), Point 1 of Lemma 43
yields $\mathcal{A},\mathcal{T}_{c}\models q_{c}(a)$ and thus we can proceed
as in Case (i). ∎

###  E.2 Proof of Lemma 43

Let $c=(c_{0},\dots,c_{n-1})$ be an input for $P$. We show how to construct
the TBox $\mathcal{T}_{c}$, query $q_{c}$, and ABox signature $\Sigma_{c}$
that satisfy Points 1 and 2 of Lemma 43. We will first use a UCQ for $q_{c}$
and later show how to improve to a CQ. The general idea is that
$\mathcal{T}_{c}$ verifies in a bottom-up way the existence of (a homomorphic
image of) what we call a _torus tree_ in the ABox. A torus tree represents the
$2^{n}\times 2^{n}$-torus along with a tiling that respects the tiling
conditions in $P$ and initial condition c, except that the representation
might be defective in that there can be different elements which represent the
same grid node but are labeled with different tile types. If a torus tree is
found, then $\mathcal{T}_{c}$ ensures that $A^{*}$ is derived at the root of
the tree. The query $q_{c}$ will be constructed to become true at the root if
and only if the torus tree has a defect. It can then be verified that

  * ($*$)

there is a solution for $P$ given $c$ if and only if there is an ABox
$\mathcal{A}$ and an $a\in\mathsf{Ind}(\mathcal{A})$ with
$\mathcal{A},\mathcal{T}_{c}\models A^{*}(a)$ and
$\mathcal{A},\mathcal{T}_{c}\not\models q_{c}(a)$

where intuitively $\mathcal{A}$ is a defect-free torus tree with root $a$.

Torus trees are of depth $2n+2$ and all tree edges are labeled with the role
composition $r^{-};r$, where $r$ is the only role name used in the reduction.
For readability, we use $S$ to abbreviate $r^{-};r$. For example, $\exists
S.C$ stands for $\exists r^{-}.\exists r.C$. Note that $S$ behaves like a
reflexive-symmetric role. The ABox signature $\Sigma_{c}$ consists of the
following symbols:

  1. 1.

concept names $A_{0},\dots,A_{2n-1}$ and
$\overline{A}_{0},\dots,\overline{A}_{2n-1}$ that serve as bits in the binary
representation of a number between 0 and $2^{2n}-1$;

  2. 2.

concept names $T_{0},\dots,T_{k}$ which represent tile types;

  3. 3.

concept names $H$, $R$, $U$ which stand for “here”, “right”, “up”;

  4. 4.

concept names $L_{0},\dots,L_{2n}$ to identify the levels of torus trees and
concept names $F$ and $G$ to identify certain other nodes;

  5. 5.

the role name $r$ used in the composition $S$.

We refer to numbers between $0$ and $2^{2n}-1$ as a _grid position_ : in its
binary representation, bits $0$ to $n-1$ represent the horizontal position in
the grid and bits $n$ to $2n-1$ the vertical position.

The next step is to define the TBox $\mathcal{T}_{c}$. We first give a few
more details about torus trees, illustrated in Figure 1. There is binary
branching on levels 0 to $2n-1$ and, intuitively, nodes on levels 0 to $2n$
form the torus tree proper while nodes on levels $2n+1$ and $2n+2$ form
gadgets appended to the tree nodes on level $2n$. Such a gadget is highlighted
in Figure 1. All nodes on level $2n+2$ are labeled with the concept name $G$,
all nodes on level $2n+1$ with the concept name $F$, and all nodes on levels
$i=0..2n$ with the concept name $L_{i}$.

$F$$\cdots$$L_{2n}$$L_{0}$$L_{2}$$L_{1}$$\vdots$$L_{2n}$$G$$G$$G$$H$$R$$U$represents
$(i,j)$represents $(i+1,j)$represents $(i,j+1)$$F$$F$

Figure 1: Structure of torus trees.

Moreover, every $L_{2n}$-node is associated with a grid position via the
concept names $A_{i},\overline{A}_{i}$ (not shown in the figure). The $G$-node
leaf below it that is labeled $H$ is associated with the same position as its
$L_{2n}$-node ancestor. In contrast, the $R$-leaf is associated with the
neighboring position to the right and the $U$-leaf with the neighboring
position to the top (all via $A_{i},\overline{A}_{i}$). Every $G$-node is
labeled with a tile $T_{i}$ (not shown in the figure) such that the tiles of
$H$\- and $R$-nodes in the same gadget satisfy the horizontal matching
condition, and likewise for the $H$\- and $U$-node and the vertical matching
condition. For technical reasons related to the query construction, the
$F$-node is labeled complementarily regarding the concept names
$A_{i},\overline{A}_{i}$ compared to its $G$-node successor. Note that, so
far, we have only required that the matching conditions are satisfied locally
in each gadget. To ensure that a torus tree represents a solution, we will
enforce later using the query $q_{c}$ that whenever two $G$-nodes represent
the same position, then they are labeled with the same tile.

We now construct the TBox $\mathcal{T}_{c}$. The last level of torus trees
must be identified by the concept name $G$. Proper verification of that level
is indicated by the concept name $G\mathsf{ok}$ (which is not in
$\Sigma_{c}$):

$\begin{array}[]{c}A_{i}\sqsubseteq\mathsf{ok}_{i}\qquad\overline{A}_{i}\sqsubseteq\mathsf{ok}_{i}\qquad
T_{j}\sqsubseteq T\mathsf{ok}\\\\[2.84526pt]
\mathsf{ok}_{0}\sqcap\cdots\sqcap\mathsf{ok}_{2n-1}\sqcap T\mathsf{ok}\sqcap
G\sqsubseteq G\mathsf{ok}\end{array}$

where $i$ ranges over $0..2n-1$. Note that, to receive a $G\mathsf{ok}$ label,
a $G$-node must be labeled with at least one of $A_{i}$ and $\overline{A}_{i}$
for each $i$, and by at least one concept name of the form $T_{j}$. We next
verify $F$-nodes:

$\begin{array}[]{r@{\;}c@{\;}l}A_{i}\sqcap\exists
S.(G\mathsf{ok}\sqcap\overline{A}_{i})&\sqsubseteq&\mathsf{ok}^{\prime}_{i}\\\\[2.84526pt]
\overline{A}_{i}\sqcap\exists S.(G\mathsf{ok}\sqcap
A_{i})&\sqsubseteq&\mathsf{ok}^{\prime}_{i}\\\\[2.84526pt]
\mathsf{ok}^{\prime}_{0}\sqcap\cdots\sqcap\mathsf{ok}^{\prime}_{2n-1}\sqcap
F&\sqsubseteq&F\mathsf{ok}\end{array}$

where $i$ ranges over $0..2n-1$. Note that we have not yet guaranteed that
$G$-nodes make true at most one of $A_{i}$ and $\overline{A}_{i}$ for each
$i$. Moreover, the first two lines may speak about different $S$-successors.
It is thus not clear that they achieve the intended complementary labeling. We
fix these problems by adding the following inclusion:

$\begin{array}[]{r@{\;}c@{\;}l}\exists S^{2n+1}.(\exists S.(G\sqcap
A_{i})\sqcap\exists
S.(G\sqcap\overline{A_{i}}))&\sqsubseteq&C_{q_{c}}\end{array}$

where $i$ ranges over $0..2n-1$, $\exists S^{\ell}.C$ denotes $\ell$-fold
quantification $\exists S.\cdots\exists S.C$, and $C_{q_{c}}$ is an
$\mathcal{E\kern-1.00006ptLI}$-concept to be defined later that will satisfy
Point 2 of Lemma 43, that is, make the query $q_{c}$ true at the root of the
torus tree. To understand this, assume for example that there is a $G$-node
labeled with both $A_{0}$ and $\overline{A}_{0}$. Then $C_{q_{c}}$ will be
made true at the root of the torus tree and thus the ABox is ruled out as a
witness in ($*$) above.

We now verify the existence of level $2n$ of the tree, identified by the
concept name $L_{2n}$. Each $L_{2n}$-node needs to have three $S$-successors,
all of them $F$-nodes, labeled with $H,R,U$, respectively. Moreover, it must
be labeled with $A_{i},\overline{A}_{i}$ to represent the same grid position
as the $H$-leaf below:

$\begin{array}[]{r@{\;}c@{\;}l}A_{i}\sqcap\exists S.(F\mathsf{ok}\
\sqcap\exists S.(G\mathsf{ok}\sqcap H\sqcap
A_{i}))&\sqsubseteq&\mathsf{ok}^{\prime\prime}_{i}\\\\[2.84526pt]
\overline{A}_{i}\sqcap\exists S.(F\mathsf{ok}\sqcap\exists
S.(G\mathsf{ok}\sqcap
H\sqcap\overline{A}_{i}))&\sqsubseteq&\mathsf{ok}^{\prime\prime}_{i}\\\\[2.84526pt]
\exists S.(F\mathsf{ok}\sqcap\exists S.(G\mathsf{ok}\sqcap
R))&\sqsubseteq&R\mathsf{ok}\\\\[2.84526pt] \exists
S.(F\mathsf{ok}\sqcap\exists S.(G\mathsf{ok}\sqcap
U))&\sqsubseteq&U\mathsf{ok}\\\\[2.84526pt] \exists S^{2n}.(\exists
S^{2}.(G\sqcap X\sqcap A_{i})\sqcap\exists S^{2}.(G\sqcap
X\sqcap\overline{A}_{i}))&\sqsubseteq&C_{q_{c}}\end{array}$

where $i$ ranges over $0..2n-1$ and $X$ ranges over $H,R,U$. The last
inclusion makes such that all $H$-leaves below a $L_{2n}$-node have the same
labeling regarding $A_{i},\overline{A}_{i}$, and likewise for all $R$-leaves
and all $U$-leaves. We next verify that the the grid positions of the
$H,R,U$-nodes below a level $2n$-node relate in the intended way. We start
with copying up the grid positions from the $R$-leaf and the $U$-leaf, for
convenience:

$\begin{array}[]{r@{\;}c@{\;}l}L_{2n}\sqcap\exists S^{2}.(G\sqcap X\sqcap
A_{i})&\sqsubseteq&A^{X}_{i}\\\\[2.84526pt] L_{2n}\sqcap\exists
S^{2}.((G\sqcap
X\sqcap\overline{A}_{i}))&\sqsubseteq&\overline{A}^{X}_{i}\end{array}$

where $i$ ranges over $0..2n-1$ and $X$ ranges over $R,U$. The following
inclusions are then used to verify that the horizontal component of the
$R$-node is incremented compared to the $H$-node:

$\begin{array}[]{r@{\;}c@{\;}l}A_{0}\sqcap\cdots\sqcap
A_{i-1}\sqcap\overline{A}_{i}\sqcap
A^{R}_{i}&\sqsubseteq&\mathsf{ok}_{HRi}\\\\[2.84526pt] A_{0}\sqcap\cdots\sqcap
A_{i-1}\sqcap
A_{i}\sqcap\overline{A}^{R}_{i}&\sqsubseteq&\mathsf{ok}_{HRi}\\\\[2.84526pt]
\overline{A}_{j}\sqcap\overline{A}_{i}\sqcap\overline{A}^{R}_{i}&\sqsubseteq&\mathsf{ok}_{HRi}\\\\[2.84526pt]
\overline{A}_{j}\sqcap A_{i}\sqcap
A^{R}_{i}&\sqsubseteq&\mathsf{ok}_{HRi}\end{array}$

where $i$ ranges over $0..n$ and $j$ over $0..i$. We can use similar
inclusions setting concept names
$\mathsf{ok}_{HRn},\dots,\mathsf{ok}_{HR2n-1}$ when the vertical component of
the $R$-node is identical to that of the $H$-node, concept names
$\mathsf{ok}_{HU0},\dots,\mathsf{ok}_{HUn-1}$ when the horizontal component of
the $U$-node is identical to that of the $H$-node, and concept names
$\mathsf{ok}_{HUn},\dots,\mathsf{ok}_{HU2n-1}$ when the vertical component of
the $U$-node is incremented compared to the $H$-node. To make $L_{2n}$ true,
which identifies level $2n$-nodes, we require that all checks succeeded:

$\begin{array}[]{r@{\,}c@{\,}l}\mathsf{ok}_{HR0}\sqcap\cdots\sqcap\mathsf{ok}_{HRm-1}\,\sqcap\\\\[2.84526pt]
\mathsf{ok}_{HU0}\sqcap\cdots\sqcap\mathsf{ok}_{HUm-1}\,\sqcap\\\\[2.84526pt]
\mathsf{ok}^{\prime\prime}_{0}\sqcap\cdots\sqcap\mathsf{ok}^{\prime\prime}_{2n-1}\,\sqcap\\\\[2.84526pt]
R\mathsf{ok}\sqcap U\mathsf{ok}\sqcap
L_{2n}&\sqsubseteq&L_{2n}\mathsf{ok}.\end{array}$

To locally ensure the tiling conditions at $L_{2n}$-nodes, we put for all
$(i,j)\notin H$ and all $(i,\ell)\notin V$:

$\begin{array}[]{r@{\,}c@{\,}l}\exists S^{2n}.(\exists S^{2}.(H\sqcap
T_{i})\sqcap\exists S^{2}.(R\sqcap
T_{j}))&\sqsubseteq&C_{q_{c}}\\\\[2.84526pt] \exists S^{2n}.(\exists
S^{2}.(H\sqcap T_{i})\sqcap\exists S^{2}.(U\sqcap
T_{\ell}))&\sqsubseteq&C_{q_{c}}.\end{array}$

We next verify the existence of levels $2n-1$ to 0 of the tree. To make sure
that the required successors are present on all levels, we branch on the
concept names $A_{i}$, $\overline{A}_{i}$ at level $i$ and for all $j<i$, keep
our choice of $A_{j}$, $\overline{A}_{j}$:

$\begin{array}[]{r@{\;}c@{\;}l}\exists S.(L_{i+1}\mathsf{ok}\sqcap
A_{i})\sqcap\exists
S.(L_{i+1}\mathsf{ok}\sqcap\overline{A}_{i})&\sqsubseteq&\mathsf{succ}_{i}\\\\[2.84526pt]
A_{j}\sqcap\exists S.(L_{i+1}\mathsf{ok}\sqcap
A_{j})&\sqsubseteq&\mathsf{ok}_{i,j}\\\\[2.84526pt]
\overline{A}_{j}\sqcap\exists
S.(L_{i+1}\mathsf{ok}\sqcap\overline{A}_{j})&\sqsubseteq&\mathsf{ok}_{i,j}\\\\[2.84526pt]
\mathsf{succ}_{i}\sqcap\mathsf{ok}_{i,0}\sqcap\cdots\sqcap\mathsf{ok}_{i,i-1}\sqcap
L_{i}&\sqsubseteq&L_{i}\mathsf{ok}\\\\[2.84526pt] \exists S^{i}.(\exists
S.(L_{i+1}\sqcap A_{j})\sqcap\exists
S.(L_{i+1}\sqcap\overline{A_{j}}))&\sqsubseteq&C_{q_{c}}\end{array}$

where $i$ ranges over $0..2n-1$ and $j$ over $0..i-1$. The initial condition
is verified at the $G$-nodes. Put

$\exists S^{2n+2}.(\overline{A}_{0}\sqcap\cdots\sqcap\overline{A}_{2n-1}\sqcap
T_{i})\sqsubseteq C_{q_{c}}$

for all $i\in\\{0,\dots,k\\}$ with $i\neq c_{0}$, and similarly for the grid
positions $(1,0),\dots,(n-1,0)$.

We next define the query $q_{c}$ to ensure that all $G$-nodes that are
associated with the same grid position are labeled with the same tile type. A
bit more verbosely, we have to guarantee that

  * ($*$)

if $a$ and $b$ are $G$-nodes labeled identically regarding the concept names
$A_{i},\overline{A}_{i}$, then there are no distinct tile types $k,j$ such
that $a$ is labeled with $T_{k}$ and $b$ with $T_{j}$.

The UCQ $q_{c}^{\vee}$ contains one CQ for each choice of tile types $k,j$.
Fix concrete such $k,j$. We construct the required CQ $q$ from component
queries $p_{0},\dots,p_{n-1}$, which all take the form of the query show on
the left-hand side of Figure 2.

$x_{4n+3}=x^{\prime}_{4n+2}$$\vdots$$x^{\prime}_{2n+1}$$x^{\prime}_{2n+2}$$x^{\prime}_{4n+2}$$x_{2n+1}$$x_{2n+2}$$x_{4n+2}$$x_{4n+3}$$x^{\prime}$$A_{i}$$\vdots$$x_{2n+1}=x^{\prime}_{2n}$$A_{i}$$\vdots$$x_{4n+2}=x^{\prime}_{4n+3}$$A_{i}$$x^{\prime}=x^{\prime}_{4n+3}$$x_{4n+2}=x^{\prime}_{4n+1}$$\vdots$$x_{0}=x$$A_{i}$$\vdots$$x_{1}=x^{\prime}_{2}$$x=x^{\prime}_{0}$$x_{0}=x^{\prime}_{1}$$A_{i}$$x_{1}=x^{\prime}_{0}$$\vdots$$\vdots$$x_{0}$$x_{1}$$x$$A_{i}$$x^{\prime}_{1}$$\overline{A}_{i}$$x_{\mathsf{ans}}$$x_{\mathsf{ans}}=x_{2n+2}=x^{\prime}_{2n+1}$$x_{\mathsf{ans}}=x_{2n+1}=x^{\prime}_{2n+2}$$x_{2n+2}=x^{\prime}_{2n+3}$$x^{\prime}_{4n+3}$$x^{\prime}_{0}$$\vdots$$\overline{A}_{i}$$\overline{A}_{i}$$x_{4n+3}=x^{\prime}$$\overline{A}_{i}$$\overline{A}_{i}$$\overline{A}_{i}$$G$$G$$G$$G$$T_{i}$$T_{j}$$T_{i}$$T_{i}$$G$$G$$T_{j}$$T_{j}$

Figure 2: The query $p_{i}$ (left) and two of its identifications (middle and
right).

Note that all edges are $S$-edges, the only difference between the component
queries is which concept names $A_{i}$ and $\overline{A}_{i}$ are used, and
$x_{\mathsf{ans}}$ is the only answer variable. We assemble
$p_{0},\dots,p_{n-1}$ into the desired query $q_{c}^{\vee}$ by taking variable
disjoint copies of $p_{0},\dots,p_{n-1}$ and then identifying (i) the
$x$-variables of all components and (ii) the $x^{\prime}$-variables of all
components.

To see why $q^{\vee}_{c}$ achieves ($*$), first note that the variables $x$
and $x^{\prime}$ must be mapped to leaves of the torus tree because of their
$G$-label. Call these leaves $a$ and $a^{\prime}$. Since $x_{0}$ and
$x^{\prime}_{0}$ are connected to $x$ in the query, both must then be mapped
either to $a$ or to its predecessor; likewise, $x_{4n+3}$ and
$x^{\prime}_{4n+3}$ must be mapped either to $a^{\prime}$ or to its
predecessor. Because of the labeling of $a$ and $a^{\prime}$ and the
predecessors in the torus tree with $A_{i}$ and $\overline{A}_{i}$, we are
actually even more constrained: exactly one of $x_{0}$ and $x^{\prime}_{0}$
must be mapped to $a$, and exactly one of $x_{4n+3}$ and $x^{\prime}_{4n+3}$
to $a^{\prime}$. If $x_{0}$ is mapped to $a$, then $x_{\mathsf{ans}}$ must be
identified with $x_{2n+2}$ because as an answer variable it has to be mapped
to the root of the tree and the only other option (identifying
$x_{\mathsf{ans}}$ with $x_{2n+1}$) would thus require a path of length $2n+1$
between $a$ and the root. Also for path length reasons, this means that
$x_{4n+3}$ must be mapped to the predecessor of $a^{\prime}$, thus
$x^{\prime}_{4n+3}$ is mapped to $a^{\prime}$. Analogously, we can show that
mapping $x^{\prime}_{0}$ to $a$ requires mapping $x_{4n+3}$ to $a^{\prime}$.
These two options give rise to the two variable identifications in each query
$p_{i}$ shown in Figure 2. Note that the first case implies that $a$ and
$a^{\prime}$ are both labeled with $A_{i}$ while they are both labeled with
$\overline{A}_{i}$ in the second case. In summary, $a$ and $a^{\prime}$ must
thus agree on all concept names $A_{i}$, $\overline{A}_{i}$. Since $a$ must
satisfy $T_{i}$ and $a^{\prime}$ must satisfy $T_{j}$ due to the labeling of
$x$ and $x^{\prime}$, we have achieved ($*$).

We now show how to replace the UCQ $q_{c}^{\vee}$ with a single CQ $q_{c}$.
This requires the following changes:

  1. 1.

the $F$-nodes in configuration trees receive additional labels: when a
$G$-node is labeled with $T_{i}$, then its predecessor $F$-node is labeled
with $T_{j}$ for all $j\neq i$;

  2. 2.

the query construction is modified.

Point 1 is important for the CQ to be constructed to work correctly and can be
achieved in a straightforward way by modifying $\mathcal{T}_{c}$, details are
omitted. We thus concentrate on Point 2. The desired CQ $q_{c}$ is again
constructed from component queries. We use $n$ components as shown in Figure
2, except that the $T_{i}$\- and $T_{j}$-labels are dropped. We further add
the component shown in Figure 3 where again $x$ and $x^{\prime}$ are the
variables shared with the other components, and where we assume for simplicity
that $T=\\{0,1,2\\}$; the generalization to an unrestricted number of tile
types is straightforward, see Lutz-DL-07.

$T_{0}$$\vdots$$y_{2,2n+1}$$\vdots$$y_{2,2n+2}$$y_{2,4n+2}$$y_{2,4n+3}$$y_{2,1}$$x=y_{0,0}$$G$$y_{0,1}=y_{1,0}=y_{2,0}$$\vdots$$y_{0,2n+1}=y_{1,2n}=y_{2,2n}$$y_{0,4n+2}=y_{1,4n+1}=y_{2,4n+1}$$y_{0,4n+3}=y_{1,4n+2}$$\vdots$$x_{\mathsf{ans}}=y_{0,2n+2}=y_{1,2n+1}=y_{2,2n+1}$$y_{1,4n+3}=x^{\prime}$$G$$T_{0}$$T_{1}$$T_{2}$$=y_{2,4n+2}=y_{2,4n+3}$$T_{1},T_{2}$$T_{0},T_{2}$$y_{0,1}$$y_{1,1}$$\vdots$$\vdots$$y_{0,2n+1}$$y_{1,2n+1}$$x_{\mathsf{ans}}$$y_{0,2n+2}$$y_{1,2n+2}$$\vdots$$\vdots$$y_{0,4n+2}$$T_{0}$$y_{0,4n+3}$$T_{2}$$y_{1,4n+3}$$y_{1,4n+2}$$x$$G$$x^{\prime}$$G$$T_{1}$$T_{1}$$y_{1,0}$$y_{2,0}$$y_{0,0}$

Figure 3: The query $q_{\mathsf{tile}}$ (left) and one of its identifications
(right).

The additional component can be understood essentially in the same way as the
previous query components.

######  Lemma 46.

$\mathcal{T}_{c}$, $q_{c}$, and $\Sigma_{c}$ satisfy Points 1 and 2 from Lemma
43 when choosing $A^{*}=L_{0}\mathsf{ok}$.

###### Proof.

(sketch) We show the following:

  1. 1.

If $P$ has a solution given $c$, then there is a $\Sigma_{c}$-ABox
$\mathcal{A}$ and an $a\in\mathsf{Ind}(\mathcal{A})$ such that
$\mathcal{A},\mathcal{T}_{c}\models A^{*}(a)$ and
$\mathcal{A},\mathcal{T}_{c}\not\models q_{c}(a)$.

  2. 2.

If $P$ has no solution given $c$, then for any $\Sigma_{c}$-ABox $\mathcal{A}$
and $a\in\mathsf{Ind}(\mathcal{A})$, $\mathcal{A},\mathcal{T}_{c}\models
A^{*}(a)$ implies $\mathcal{A},\mathcal{T}_{c}\models q_{c}(a)$.

  3. 3.

There is an $\mathcal{E\kern-1.00006ptLI}$-concept $C_{q_{c}}$ such that $d\in
C^{\mathcal{I}}$ implies $\mathcal{I}\models q_{c}(d)$.

  4. 4.

$q_{c}$ is FO-rewritable relative to $\mathcal{T}_{c}$ and $\Sigma_{c}$.

(1) Take as $\mathcal{A}$ a torus tree that encodes a solution for $P$ given
$c$ (viewed as an ABox) and let $a$ be the root of the tree. The verification
of torus trees by $\mathcal{T}_{c}$ yields $\mathcal{A},\mathcal{T}_{c}\models
L_{0}\mathsf{ok}(a)$. Since the torus tree is not defective, we have
$\mathcal{A},\mathcal{T}_{c}\not\models q_{c}(a)$.

(2) Since the verification of (homomorphic images of) torus trees by
$\mathcal{T}_{c}$ is sound, $\mathcal{A},\mathcal{T}_{c}\models
L_{0}\mathsf{ok}(a)$ implies that $\mathcal{A}$ contains a homomorphic image
of a torus tree whose root is identified by $a$. Since there is no solution
for $P$ given $c$, that tree must be defective. Consequently,
$\mathcal{A},\mathcal{T}_{c}\models q_{c}(a)$.

(3) Set

$\begin{array}[]{r@{\,}c@{\,}l}G_{1}&=&G\sqcap\overline{A}_{0}\sqcap\cdots\sqcap\overline{A}_{k}\sqcap
T_{0}\\\\[2.84526pt]
G_{2}&=&G\sqcap\overline{A}_{0}\sqcap\cdots\sqcap\overline{A}_{k}\sqcap
T_{1}\\\\[2.84526pt] F_{1}&=&A_{0}\sqcap\cdots\sqcap A_{n}\sqcap
T_{1}\sqcap\cdots\sqcap T_{k}\\\\[2.84526pt] F_{2}&=&A_{0}\sqcap\cdots\sqcap
A_{n}\sqcap T_{0}\sqcap T_{2}\sqcap\cdots\sqcap T_{k}\\\\[2.84526pt]
C_{q_{c}}&=&\exists S^{2n+1}.(F_{1}\sqcap\exists S.G_{1})\sqcap\exists
S^{2n+1}.(F_{2}\sqcap\exists S.G_{2})\end{array}$

It can be verified that $C_{q_{c}}$ is as required.

(4) Note that whenever $D\sqsubseteq C_{q_{c}}$ is in $\mathcal{T}_{c}$, then
$D$ uses symbols from $\Sigma_{c}$, only. One can construct an FO-rewriting of
$q_{c}$ relative to $\mathcal{T}_{c}$ and $\Sigma_{c}$ that has the form

$q_{0}(x)\vee\bigvee_{D\sqsubseteq C_{q_{c}}\in\mathcal{T}_{c}}q_{D}(x)$

where $q_{D}$ is $D$ viewed as a CQ. To define $q_{0}$, let
$\mathcal{T}^{0}_{c}$ be the result of removing from $\mathcal{T}_{c}$ all CIs
of the form $D\sqsubseteq C_{q_{c}}$. Note that the recursion depth of
$\mathcal{T}^{0}_{c}$ is bounded by $2n+1$. We can thus choose

$q_{0}(x)=\bigvee_{\mathcal{A}\in\mathfrak{A}}q_{\mathcal{A}}(x)$

where $\mathfrak{A}$ is the set of all pseudo tree $\Sigma_{c}$-ABoxes
$\mathcal{A}$ of depth at most ${2n+1}$, width at most $|q_{c}|$, outdegree at
most $|\mathcal{T}_{c}|$, and with root $a_{0}$ such that
$\mathcal{A},\mathcal{T}_{c}\models q_{c}[a_{0}]$ and where $q_{\mathcal{A}}$
is $\mathcal{A}$ viewed as a CQ. ∎

###  E.3 2ExpTime lower bounds

We consider Boolean (connected) CQs. We reduce the word problem of
exponentially space bounded alternating Turing machines (ATMs), see
DBLP:journals/jacm/ChandraKS81. An _Alternating Turing Machine (ATM)_ is of
the form $M=(Q,\Sigma,\Gamma,q_{0},\Delta)$. The set of _states_
$Q=Q_{\exists}\uplus Q_{\forall}\uplus\\{q_{a}\\}\uplus\\{q_{r}\\}$ consists
of _existential states_ in $Q_{\exists}$, _universal states_ in $Q_{\forall}$,
an _accepting state_ $q_{a}$, and a _rejecting state_ $q_{r}$; $\Sigma$ is the
_input alphabet_ and $\Gamma$ the _work alphabet_ containing a _blank symbol_
$\square$ and satisfying $\Sigma\subseteq\Gamma$; $q_{0}\in Q_{\exists}\cup
Q_{\forall}$ is the _starting_ state; and the _transition relation_ $\Delta$
is of the form

$\Delta\;\subseteq\;Q\times\Gamma\times Q\times\Gamma\times\\{L,R\\}.$

We write $\Delta(q,\sigma)$ to denote
$\\{(q^{\prime},\sigma^{\prime},M)\mid(q,\sigma,q^{\prime},\sigma^{\prime},M)\in\Delta\\}$
and assume w.l.o.g. that the state $q_{0}$ cannot be reached by any
transition.

A _configuration_ of an ATM is a word $wqw^{\prime}$ with
$w,w^{\prime}\in\Gamma^{*}$ and $q\in Q$. The intended meaning is that the
one-side infinite tape contains the word $ww^{\prime}$ with only blanks behind
it, the machine is in state $q$, and the head is on the symbol just after $w$.
The _successor configurations_ of a configuration $wqw^{\prime}$ are defined
in the usual way in terms of the transition relation $\Delta$. A _halting
configuration_ is of the form $wqw^{\prime}$ with $q\in\\{q_{a},q_{r}\\}$.

A _computation_ of an ATM $M$ on a word $w$ is a (finite or infinite) sequence
of configurations $K_{0},K_{1},\dots$ such that $K_{0}=q_{0}w$ and $K_{i+1}$
is a successor configuration of $K_{i}$ for all $i\geq 0$. The ATMs considered
in the following have only _finite_ computations on any input. Since this case
is simpler than the general one, we define acceptance for ATMs with finite
computations, only. Let $M$ be such an ATM. A halting configuration is
_accepting_ iff it is of the form $wq_{a}w^{\prime}$. For other configurations
$K=wqw^{\prime}$, acceptance depends on $q$: if $q\in Q_{\exists}$, then $K$
is accepting iff at least one successor configuration is accepting; if $q\in
Q_{\forall}$, then $K$ is accepting iff all successor configurations are
accepting. Finally, the ATM $M$ with starting state $q_{0}$ _accepts_ the
input $w$ iff the _initial configuration_ $q_{0}w$ is accepting. We use $L(M)$
to denote the language accepted by $M$.

There is an exponentially space bounded ATM $M$ whose word problem is
2ExpTime-hard and we may assume that the length of every computation path of
$M$ on $w\in\Sigma^{n}$ is bounded by $2^{2^{n}}$, and all the configurations
$wqw^{\prime}$ in such computation paths satisfy $|ww^{\prime}|\leq 2^{n}$,
see DBLP:journals/jacm/ChandraKS81.

######  Lemma 47.

Given an input $w$ to $M$, one can construct in polynomial time an
$\mathcal{E\kern-1.00006ptLI}$ TBox $\mathcal{T}_{w}$, a Boolean connected CQ
$q_{w}$, and an ABox signature $\Sigma_{w}$ such that, for a selected concept
name $A^{*}\notin\Sigma_{w}$,

  1. 1.

$M$ accepts $w$ iff there is a $\Sigma_{w}$-ABox $\mathcal{A}$ such that
$\mathcal{A},\mathcal{T}_{w}\models\exists x\,A^{*}(x)$ and
$\mathcal{A},\mathcal{T}_{w}\not\models q_{w}$;

  2. 2.

$M$ accepts $w$ iff there is a $\Sigma_{w}$-ABox $\mathcal{A}$ and an
$a\in\mathsf{Ind}(\mathcal{A})$ such that $\mathcal{A},\mathcal{T}_{w}\models
A^{*}(a)$ and $\mathcal{A},\mathcal{T}_{w}\not\models q_{w}$;

  3. 3.

$q_{w}$ is FO-rewritable relative to $\mathcal{T}_{w}$ and $\Sigma_{w}$;

  4. 4.

there is an $\mathcal{E\kern-1.00006ptLI}$-concept $C_{q_{w}}$ such that
$C_{q_{w}}^{\mathcal{I}}\neq\emptyset$ implies $\mathcal{I}\models q_{w}$.

######  Theorem 48.

Containment in $(\mathcal{E\kern-1.00006ptLI},\text{CQ})$ is 2ExpTime-hard.

###### Proof.

Let $w$ be an input to $M$, $\mathcal{T}_{w}$, $q_{w}$, and $\Sigma_{w}$ as in
Lemma 47. By Point 1 of Lemma 47, $(\mathcal{T}_{w},\Sigma_{w},\exists
x\,A^{*}(x))\not\subseteq(\mathcal{T}_{w},\Sigma_{w},q_{w})$ over
$\Sigma_{w}$-ABoxes iff $M$ accepts $w$. ∎

######  Theorem 49.

FO-rewritability in $(\mathcal{E\kern-1.00006ptLI},\text{CQ})$ is 2ExpTime-
hard.

###### Proof.

Let $w$ be an input to $M$ and $\mathcal{T}_{w}$, $q_{w}$, $\Sigma_{w}$ as in
Lemma 47. We obtain a TBox $\mathcal{T}$ by extending $\mathcal{T}_{w}$ with
the following:

$\begin{array}[]{rcll}\exists r.A&\sqsubseteq&A\\\\[2.84526pt] A\sqcap B\sqcap
A^{*}&\sqsubseteq&C_{q_{w}}\end{array}$

where $A$, $B$, and $r$ do not occur in $\mathcal{T}_{w}$ and $q_{w}$,
$A^{*}\notin\Sigma_{w}$ is the concept name from Lemma 47 and $C_{q_{w}}$ the
concept from Point 4 of that lemma. Set $\Sigma=\Sigma_{w}\cup\\{A,B,r\\}$. It
remains to prove the following.
Claim. $M$ accepts $w$ iff $q_{w}$ is not FO-rewritable relative to
$\mathcal{T}$ and $\Sigma$.
First assume that $M$ accepts $w$. By Point 2 of Lemma 47, there is a
$\Sigma_{w}$-ABox $\mathcal{A}$ and $a_{0}\in\mathsf{Ind}(\mathcal{A})$ such
that $\mathcal{A},\mathcal{T}_{w}\models A^{*}(a_{0})$ and
$\mathcal{A},\mathcal{T}_{w}\not\models q_{w}$. Since every
$\mathcal{E\kern-1.00006ptLI}$ TBox is unraveling tolerant lutz-2012 and by
compactness, we can assume w.l.o.g. that $\mathcal{A}$ is tree-shaped with
root $a_{0}$. Let $\ell$ be the depth of $\mathcal{A}$. For each $k>\ell$, let
$\mathcal{A}_{k}$ be the ABox obtained by extending $\mathcal{A}$ with

$B(a_{0}),r(a_{0},a_{1}),\dots,r(a_{k-1},a_{k}),A(a_{k})$

where $a_{k},\dots,a_{1}$ do not occur in $\mathcal{A}$. Note that
$\mathcal{A}_{k}$ is tree-shaped and of depth at least $k$. Since
$\mathcal{A},\mathcal{T}_{w}\models A^{*}(a_{0})$, we have
$\mathcal{A}_{k},\mathcal{T}\models C_{q_{w}}(a_{0})$. Applying Point 4 of
Lemma 47, we obtain $\mathcal{A}_{k},\mathcal{T}\models q_{w}$. To prove that
$q_{w}$ is not FO-rewritable relative to $\mathcal{T}$ and $\Sigma$, by
Theorem 9 it suffices to show that $\mathcal{A}|_{>0},\mathcal{T}\not\models
q_{w}$ and $\mathcal{A}_{k}|_{\leq k-1},\mathcal{T}\not\models q_{w}$. Note
that neither $\mathcal{A}_{k}|_{>0}$ nor $\mathcal{A}_{k}|_{\leq k-1}$
contains an $r$-path from an individual satisfying $B$ to an individual
satisfying $A$. On such ABoxes, $\mathcal{T}$ can be replaced with
$\mathcal{T}_{w}$ since the left-hand sides of the second additional concept
inclusions in $\mathcal{T}$ will never apply, and that concept inclusion is
the only (additional) one whose right-hand side contains symbols from
$\mathcal{T}$ and $q_{w}$. It thus suffices to show that
$\mathcal{A}_{k}|_{>0},\mathcal{T}_{w}\not\models q_{w}$ and
$\mathcal{A}_{k}|_{k-1},\mathcal{T}_{w}\not\models q_{w}$. This follows from
$\mathcal{A},\mathcal{T}_{w}\not\models q_{w}$ and the fact that $A$, $B$, and
$r$ (the only symbols in assertions from
$(\mathcal{A}_{k}|_{>0})\setminus\mathcal{A}$ and
$(\mathcal{A}_{k}|_{k-1})\setminus\mathcal{A}$) occur neither in
$\mathcal{T}_{w}$ nor in $q_{w}$.

Now assume that $M$ does not accept $w$. By Point 3 of Lemma 47, there is an
FO-rewriting $\widehat{q}_{w}$ of $q_{w}$ relative to $\mathcal{T}_{w}$ and
$\Sigma_{w}$. We argue that $\widehat{q}_{w}$ is also an FO-rewriting of
$q_{w}$ relative to $\mathcal{T}$ and $\Sigma$.

First assume $\mathcal{A}\models\widehat{q}_{w}$ for some $\Sigma$-ABox
$\mathcal{A}$. Since $\widehat{q}_{w}$ uses only symbols from $\Sigma_{w}$,
this means that $\mathcal{A}^{\prime}\models\widehat{q}_{w}$ where
$\mathcal{A}^{\prime}$ is the reduct of $\mathcal{A}$ to symbols in
$\Sigma_{w}$. Thus $\mathcal{A}^{\prime},\mathcal{T}_{w}\models q_{w}$,
implying $\mathcal{A},\mathcal{T}\models q_{w}$.

Conversely, assume that $\mathcal{A},\mathcal{T}\models q_{w}$ for some
$\Sigma$-ABox $\mathcal{A}$. Using canonical models and the construction of
$\mathcal{T}$, one can show that this implies (i)
$\mathcal{A},\mathcal{T}_{w}\models q_{w}$ or (ii)
$\mathcal{A},\mathcal{T}_{w}\models\exists x\,A^{*}(x)$. In Case (i), we get
$\mathcal{A}^{\prime},\mathcal{T}_{w}\models q_{w}$, where
$\mathcal{A}^{\prime}$ is the $\Sigma_{w}$-reduct of $\mathcal{A}$. Thus
$\mathcal{A}^{\prime}\models\widehat{q}_{w}$, which implies
$\mathcal{A}\models\widehat{q}_{w}$. In Case (ii), Point 1 of Lemma 47 yields
$\mathcal{A},\mathcal{T}_{w}\models q_{w}$ and thus we can proceed as in Case
(i). ∎

###  E.4 Proof of Lemma 47

Let $w=\sigma_{0}\cdots\sigma_{m-1}\in\Sigma^{*}$ be an input to $M$. We show
how to construct a TBox $\mathcal{T}_{w}$, query $q_{w}$, and ABox signature
$\Sigma_{w}$ that satisfy Points 1 to 4 of Lemma 47. We first use a UCQ for
$q_{w}$, which results in a simpler reduction, and in a second step show how
to replace the UCQ with a CQ.

In the reduction, we represent each configuration of a computation of $M$ by
the leaves of a _configuration tree_ that has depth $n+2$ and whose edges are
represented by the role composition $S=r^{-};r$, similarly to the
representation of the $2^{n}\times 2^{n}$-torus in the previous reduction. The
trees representing configurations are then interconnected to a _computation
tree_ which represents the computation of $M$ on $w$. This is illustrated in
Figure 4, where

$S$$T_{1}$$T_{2}$$T_{3}$$T_{4}$$\cdots$$\cdots$$S$$S$

Figure 4: Representing ATM computations.

the tree $T_{1}$ represents an existential configuration and thus has only one
successor tree $T_{2}$, connected via the same role composition $S$ that is
also used inside configuration trees. In contrast, $T_{2}$ represents a
universal configuration with two successor configurations $T_{3}$ and $T_{4}$.

The above description is actually an oversimplification. In fact, every
configuration tree stores two configurations instead of only one: the current
configuration and the previous configuration in the computation. The query
$q_{w}$ to be defined later on makes sure that the previous configuration
stored in a configuration tree is identical to the current configuration
stored in its predecessor configuration tree. The actual transitions of $M$
are then represented locally inside configuration trees. This is illustrated
by a sequence of existential configurations in Figure 5 where each $C_{i}$
represents a stored configuration, “$\mathsf{step}$” denotes a transition of
$M$, and “$=$” denotes identity of stored configurations.

Since the role composition $S$ used to connect configuration trees is
symmetric, it is difficult to distinguish predecessor configuration trees from
successor configuration trees. To break this symmetry, we represent the
current and next configuration stored in configuration trees using six
different sets of concept names. This is also indicated in Figure 5 where
$C_{i}$ means that we use the $i$-th set of concept names for representing the
stored configuration.

$=$$C_{1}$$C_{2}$$C_{3}$$C_{4}$$C_{5}$$C_{6}$$C_{1}$$C_{2}$$S$$S$$S$step$\mathsf{tree}^{0}$$\mathsf{tree}^{1}$$\mathsf{tree}^{2}$$\mathsf{tree}^{0}$stepstepstep$=$$=$

Figure 5: Representing ATM computations.

We next construct the TBox $\mathcal{T}_{w}$, which is used to verify the
existence of an accepting computation tree of $M$ on input $w$ in the ABox,
apart from the described copying of stored configurations which will be
achieved by the query $q_{w}$ later on. The ABox signature $\Sigma_{w}$
consists of the following symbols:

  1. 1.

concept names $A_{0},\dots,A_{n-1}$ and
$\overline{A}_{0},\dots,\overline{A}_{n-1}$ that serve as bits in the binary
representation of a number between 0 and $2^{n}-1$, identifying the position
of tape cells (that is, leaves in configuration trees);

  2. 2.

for each $\sigma\in\Gamma$, the concept names $A^{i}_{\sigma}$, $1\leq i\leq
6$;

  3. 3.

for each $\sigma\in\Gamma$ and $q\in Q$, the concept names $A^{i}_{q,\sigma}$,
$1\leq i\leq 6$;

  4. 4.

the concept names $\overline{H}$, $W$, and $\overline{W}$ which stand for
“cell without head”, “cell being written to reach current configuration”, and
“cell not being written to reach current configuration”;

  5. 5.

a concept name $A_{q,\sigma,M}$ for each $q\in Q$, $\sigma\in\Gamma$, and
$M\in\\{L,R\\}$ to describe transitions of $M$;

  6. 6.

a concept name $I$ that marks the initial configuration;

  7. 7.

concept names $L_{0},\dots,L_{n}$ to identify the levels of configuration
trees and concept names $F_{1},F_{2},G_{1},G_{2}$ to identify certain other
nodes;

  8. 8.

the role name $r$ used in the composition $S$.

The concept names $A^{i}_{\sigma}$ are used to represent the symbols on the
tape that are currently not under the head and $A^{i}_{q,\sigma}$ to mark tape
cells under the head, indicating the head position, the current state, and the
symbol under the head.

We start with verifying single configuration trees. Such trees come in three
different types, depending on the set of concept names that we use to
represent the current and previous configuration stored. This is shown in
Figure 5. Type 0 means that the previous configuration is represented by
concept names of the form $A^{1}_{\sigma}$ and $A^{1}_{q,\sigma}$ and the
current configuration by concept names $A^{2}_{\sigma}$ and
$A^{2}_{q,\sigma}$, type 1 uses $A^{3}_{\sigma}$ and $A^{3}_{q,\sigma}$ for
the previous configuration, and so on. We start with verifying configuration
trees of type 0. Intuitively, nodes on levels 0 to $n$ form the configuration
tree proper while nodes on levels $n+1$ and $n+2$ form gadgets appended to the
tree nodes on level $n$, similarly to what is shown in Figure 1. We identify
each node on level $n+1$ with one of the concept names $F_{1}$, $F_{2}$ and
each node on level $n+2$ with one of the concept names $G_{1},G_{2}$. In
contrast to Figure 1, there are only two nodes below each level $n$ node, one
labeled $F_{1}$ and one labeled $F_{2}$. Moreover, every $F_{\ell}$ node must
have a $G_{\ell}$-node successor. Each $G_{\ell}$-node represents a tape cell,
and the position of that cell is encoded in binary by the concept names
$A_{i},\overline{A}_{i}$. The $G_{1}$\- and $G_{2}$-node below the same level
$n$ node must both have the same position and, for similar reasons as in the
previous reduction, the $F_{\ell}$ nodes in between receive a complementary
labeling regarding these concept names and also regarding the concept names
$A^{\ell}_{\sigma},A^{\ell}_{q,\sigma}$. At $G_{1}$-nodes, the concept names
$A^{1}_{\sigma}$ and $A^{1}_{q,\sigma}$ are used to store information and at
$G_{2}$-nodes, we use the concept names $A^{2}_{\sigma}$ and
$A^{2}_{q,\sigma}$. Thus, $G_{1}$-nodes represent the previous configuration
while $G_{2}$-nodes representing the current configutation. The concept names
$\overline{H},W,\overline{W}$ are used for the current configuration, only.

The verification of configuration trees is again bottom-up, starting at level
$n+2$ nodes:

$\begin{array}[]{c}A_{i}\sqsubseteq\mathsf{ok}_{i}\qquad\overline{A}_{i}\sqsubseteq\mathsf{ok}_{i}\qquad
A^{1}_{\sigma}\sqsubseteq\Gamma\mathsf{ok}_{1}\quad
A^{1}_{q,\sigma}\sqsubseteq\Gamma\mathsf{ok}_{1}\\\\[2.84526pt]
\mathsf{ok}_{0}\sqcap\cdots\sqcap\mathsf{ok}_{n-1}\sqcap\Gamma\mathsf{ok}_{1}\sqcap
G_{1}\sqsubseteq G_{1}\mathsf{ok}\\\\[2.84526pt]
A^{2}_{\sigma}\sqcap\overline{H}\sqcap\overline{W}\sqsubseteq\Gamma\mathsf{ok}_{2}\quad
A^{2}_{\sigma}\sqcap\overline{H}\sqcap
W\sqsubseteq\Gamma\mathsf{ok}_{2}\\\\[2.84526pt]
A^{2}_{q,\sigma}\sqcap\overline{W}\sqsubseteq\Gamma\mathsf{ok}_{2}\\\\[2.84526pt]
\mathsf{ok}_{0}\sqcap\cdots\sqcap\mathsf{ok}_{n-1}\sqcap\Gamma\mathsf{ok}_{2}\sqcap
G_{2}\sqsubseteq G_{2}\mathsf{ok}\end{array}$

where $i$ ranges over $0..n-1$, $q$ over the elements of $Q$ and $\sigma$ over
the elements of $\Gamma$. Note that every $G_{\ell}$-node must be labeled with
at least one of $A_{i}$ and $\overline{A}_{i}$ for each $i$ and by at least
one concept name of the form $A^{\ell}_{\sigma}$ or $A^{\ell}_{q,\sigma}$. If
$\ell=2$, then an $A^{\ell}_{\sigma}$-label (as opposed to an
$A^{\ell}_{q,\sigma}$-label) is acceptable only if there is also an
$\overline{H}$-label. For $\ell=2$, there must also be a $W$\- or
$\overline{W}$-label, the former only being acceptable if the head is not on
the current cell. We now verify $F_{\ell}$-nodes:

$\begin{array}[]{r@{\;}c@{\;}l}A_{i}\sqcap\exists
S.(G_{\ell}\mathsf{ok}\sqcap\overline{A}_{i})&\sqsubseteq&\mathsf{ok}_{\ell,i}\\\\[2.84526pt]
\overline{A}_{i}\sqcap\exists S.(G_{\ell}\mathsf{ok}\sqcap
A_{i})&\sqsubseteq&\mathsf{ok}_{\ell,i}\\\\[2.84526pt]
\mathop{\mathop{\mbox{\midmathxx\char
117\relax}}}\limits_{\beta\in(\Gamma\cup(Q\times\Gamma))\setminus\\{\alpha\\}}A^{\ell}_{\beta}\sqcap\exists
S.(G_{\ell}\mathsf{ok}\sqcap
A^{\ell}_{\alpha})&\sqsubseteq&\Gamma\mathsf{ok}^{\prime}_{\ell}\\\\[2.84526pt]
\mathsf{ok}_{\ell,0}\sqcap\cdots\sqcap\mathsf{ok}_{\ell,n-1}\sqcap\Gamma\mathsf{ok}^{\prime}_{\ell}\sqcap
F_{\ell}&\sqsubseteq&F_{\ell}\mathsf{ok}\end{array}$

where $\ell$ ranges over 1,2, $i$ over $0..n-1$, and $\alpha$ over
$\Gamma\cup(Q\times\Gamma)$. We have not yet guaranteed that $G_{\ell}$-nodes
make true at most one of $A_{i}$ and $\overline{A}_{i}$ for each $i$, at most
one concept name of the form $A^{\ell}_{\alpha}$, and not simultaneously $W$
and $\overline{W}$, or $\overline{H}$ and a concept name of the form
$A^{2}_{q,\sigma}$, or $W$ and a concept name $A^{2}_{q,\sigma}$. Moreover,
the first three lines may speak about different $S$-successors. It is thus not
clear that they achieve the intended complementary labeling. We fix these
problems by adding the following inclusions:

$\begin{array}[]{r@{\;}c@{\;}l}\exists S.(G_{\ell}\sqcap A_{i})\sqcap\exists
S.(G_{\ell}\sqcap\overline{A_{i}})&\sqsubseteq&C_{q_{w}}\\\\[2.84526pt]
\exists S.(G_{\ell}\sqcap A^{\ell}_{\alpha})\sqcap\exists S.(G_{\ell}\sqcap
A^{\ell}_{\beta})&\sqsubseteq&C_{q_{w}}\\\\[2.84526pt] \exists
S.(G_{\ell}\sqcap W)\sqcap\exists
S.(G_{\ell}\sqcap\overline{W})&\sqsubseteq&C_{q_{w}}\\\\[2.84526pt] \exists
S.(G_{\ell}\sqcap A^{2}_{q,\sigma})\sqcap\exists
S.(G_{\ell}\sqcap\overline{H})&\sqsubseteq&C_{q_{w}}\\\\[2.84526pt] \exists
S.(G_{\ell}\sqcap A^{2}_{q,\sigma})\sqcap\exists S.(G_{\ell}\sqcap
W)&\sqsubseteq&C_{q_{w}}\end{array}$

where $\ell$ ranges over $1,2$, $i$ over $0..n-1$, $\alpha,\beta$ take
distinct values from $\Gamma\cup(Q\times\Gamma)$, $q$ ranges over $Q$, and
$\sigma$ over $\Gamma$. Moreover, $C_{q_{w}}$ is an
$\mathcal{E\kern-1.00006ptLI}$-concept to be defined later that will satisfy
Point 4 of Lemma 47, that is, make the query $q_{w}$ true.

We now verify the existence of level $n$ of the tree, identified by the
concept name $L_{n}$. Nodes here need to have $S$-successors in $F_{1}$ and
$F_{2}$ that are again labeled complementarily regarding the concept names
$A_{i},\overline{A}_{i}$ (in other words, the $L_{n}$ node agrees with the
labeling of the $G_{1}$\- and $G_{2}$-node leaves below it):

$\displaystyle A_{i}\sqcap\exists
S.(F_{\ell}\mathsf{ok}\sqcap\overline{A}_{i})$
$\displaystyle\sqsubseteq\mathsf{ok}^{\prime}_{\ell,i}$
$\displaystyle\overline{A}_{i}\sqcap\exists S.(F_{\ell}\mathsf{ok}\sqcap
A_{i})$ $\displaystyle\sqsubseteq\mathsf{ok}^{\prime}_{\ell,i}$
$\displaystyle\mathsf{ok}^{\prime}_{1,0}\sqcap\cdots\sqcap\mathsf{ok}^{\prime}_{1,n-1}\sqcap\mathsf{ok}^{\prime}_{2,0}\sqcap\cdots\sqcap\mathsf{ok}^{\prime}_{2,n-1}\sqcap
L_{n}$ $\displaystyle\sqsubseteq L_{n}\mathsf{ok}$ $\displaystyle\exists
S.(F_{\ell}\sqcap A_{i})\sqcap\exists S.(F_{\ell}\sqcap\overline{A}_{i})$
$\displaystyle\sqsubseteq C_{q_{w}}$ $\displaystyle\exists S.(F_{\ell}\sqcap
A^{\ell}_{\alpha})\sqcap\exists S.(F_{\ell}\sqcap A^{\ell}_{\beta})$
$\displaystyle\sqsubseteq C_{q_{w}}$

where $\ell$ ranges over $1..2$, $i$ over $0..n-1$, and $\alpha,\beta$ take
distinct values from $\Gamma\cup(Q\times\Gamma)$.

We next verify the existence of levels $n-1$ to 0 of the configuration tree.
We exploit that we have already stored the position of the leaves in the
concept names $A_{i}$, $\overline{A}_{i}$ at $L_{n}$-nodes. Each node on level
$i$ branches on the concept names $A_{i},\overline{A}_{i}$ and keeps the
choice of $A_{j},\overline{A}_{j}$ for all $j<i$:

$\begin{array}[]{r@{\;}c@{\;}l}\exists S.(L_{i+1}\mathsf{ok}\sqcap
A_{i})\sqcap\exists
S.(L_{i+1}\mathsf{ok}\sqcap\overline{A}_{i})&\sqsubseteq&\mathsf{succ}_{i}\\\\[2.84526pt]
A_{j}\sqcap\exists S.(L_{i+1}\mathsf{ok}\sqcap
A_{j})&\sqsubseteq&\mathsf{ok}^{\prime\prime}_{i,j}\\\\[2.84526pt]
\overline{A}_{j}\sqcap\exists
S.(L_{i+1}\mathsf{ok}\sqcap\overline{A}_{j})&\sqsubseteq&\mathsf{ok}^{\prime\prime}_{i,j}\\\\[2.84526pt]
\mathsf{succ}_{i}\sqcap\mathsf{ok}^{\prime\prime}_{i,0}\sqcap\cdots\sqcap\mathsf{ok}^{\prime\prime}_{i,i-1}\sqcap
L_{i}&\sqsubseteq&L_{i}\mathsf{ok}\\\\[2.84526pt] \exists S.(L_{i+1}\sqcap
A_{j})\sqcap\exists
S.(L_{i+1}\sqcap\overline{A_{j}})&\sqsubseteq&C_{q_{w}}\end{array}$

where $i$ ranges over $0..n-1$ and $j$ over $0..i-1$. We also want that
configuration trees have exactly one leaf labeled with a concept name of the
form $A^{2}_{q,\sigma}$ and exactly one leaf labeled with $W$. We start with
enforcing the “at most one” part of “exactly one”:

$\displaystyle F_{2}\sqcap\exists S.(G_{2}\sqcap A^{2}_{q,\sigma})$
$\displaystyle\sqsubseteq H$ $\displaystyle L_{n}\sqcap\exists S.(F_{2}\sqcap
H)$ $\displaystyle\sqsubseteq H$ $\displaystyle L_{i}\sqcap\exists
S.(L_{i+1}\sqcap H)$ $\displaystyle\sqsubseteq H$ $\displaystyle
L_{i}\sqcap\exists S.(L_{i+1}\sqcap A_{i}\sqcap H)\sqcap\exists
S.(L_{i+1}\sqcap\overline{A}_{i}\sqcap H)$ $\displaystyle\sqsubseteq
C_{q_{w}}$ $\displaystyle F_{2}\sqcap\exists S.(G_{2}\sqcap W)$
$\displaystyle\sqsubseteq W^{\prime}$ $\displaystyle L_{n}\sqcap\exists
S.(F_{2}\sqcap W^{\prime})$ $\displaystyle\sqsubseteq W^{\prime}$
$\displaystyle L_{i}\sqcap\exists S.(L_{i+1}\sqcap W^{\prime})$
$\displaystyle\sqsubseteq W^{\prime}$ $\displaystyle L_{i}\sqcap\exists
S.(L_{i+1}\sqcap A_{i}\sqcap W^{\prime})\sqcap\exists
S.(L_{i+1}\sqcap\overline{A}_{i}\sqcap W^{\prime})$ $\displaystyle\sqsubseteq
C_{q_{w}}$

where $i$ ranges over $0..n-1$ and $q,\sigma$ over $Q\times\Gamma$. Note that
we use $A_{i}$ and $\overline{A}_{i}$ to distinguish left successors and right
successors in the tree: when we see a label $A^{2}_{q,\sigma}$ at a
$G_{2}$-leaf, we propagate the marker $H$ up the tree and additionally make
sure that, at no node of the tree, we have an $H$-marker coming both from the
left successor and from the right successor. We deal with $W$ in a similar
way, propagating the marker $W^{\prime}$.

The “at least one” part of “exactly one” requires some changes to the concept
inclusions already given, which we only sketch. We have not included theses
changes in the original version of the inclusions above to avoid cluttering
the presentation. Essentially, we have to keep track of where we have already
seen a concept name of the form $A^{2}_{q,\sigma}$ in a $G_{2}$-leaf and where
we have already seen a $G_{2}$-leaf labeled $W$. For simplicity, let us
concentrate on the latter. We replace the concept inclusion

$\mathsf{ok}_{2,0}\sqcap\cdots\sqcap\mathsf{ok}_{2,n-1}\sqcap\Gamma\mathsf{ok}^{\prime}_{2}\sqcap
F_{2}\sqsubseteq F_{2}\mathsf{ok}$

above with

$\displaystyle\mathsf{ok}_{2,0}\sqcap\cdots\sqcap\mathsf{ok}_{2,n-1}\sqcap\Gamma\mathsf{ok}^{\prime}_{2}\sqcap
F_{2}\sqcap$ $\displaystyle\exists S.(G_{2}\sqcap W)$
$\displaystyle\sqsubseteq F^{W}_{2}\mathsf{ok}$
$\displaystyle\mathsf{ok}_{2,0}\sqcap\cdots\sqcap\mathsf{ok}_{2,n-1}\sqcap\Gamma\mathsf{ok}^{\prime}_{2}\sqcap
F_{2}\sqcap$ $\displaystyle\exists S.(G_{2}\sqcap\overline{W})$
$\displaystyle\sqsubseteq F^{\overline{W}}_{2}\mathsf{ok}$

Note that we have replaced $F_{2}\mathsf{ok}$ in the conclusion with
$F^{W}_{2}\mathsf{ok}$ and $F^{\overline{W}}_{2}\mathsf{ok}$, recording
whether or not there is a $G_{2}$-node satisfying $W$ below. The information
that we have seen $W$ is then propagated propagated up the tree, which
requires replacing each of $L_{n}\mathsf{ok},\dots,L_{1}\mathsf{ok}$ with two
versions, $L^{W}_{i}\mathsf{ok}$ and $L^{\overline{W}}_{i}\mathsf{ok}$. On
each level, we set $L^{\overline{W}}_{i}\mathsf{ok}$ if both successors are
labeled with $L^{\overline{W}}_{i+1}\mathsf{ok}$ and $L^{W}_{i}\mathsf{ok}$ if
one successor is labeled with $L^{W}_{i+1}\mathsf{ok}$, but not both. In fact,
if both successors are labeled $L^{W}_{i+1}\mathsf{ok}$, then neither
$L^{W}_{i}\mathsf{ok}$ nor $L^{\overline{W}}_{i}\mathsf{ok}$ will be set and
this is exactly how we can ensure that there is at most one $G_{2}$-leaf
labeled $W$. It can be enforced in an analogous way that there is a $G_{2}$
labeled with a concept name of the form $A^{2}_{q,\sigma}$. In fact, we have
to deal with both $W$ and these concept names simultaneously, using concept
names such as $L^{W,H}_{i}\mathsf{ok}$ indicating that we are at a tree node
on level $i$ below which there is a $G_{2}$-leaf satisfying $W$ and a
$G_{2}$-leaf satisfying a concept name $A^{2}_{q,\sigma}$. Details are
omitted.

At this point, we have essentially finished the verification of configuration
trees of type 0 (we will comment on the other types below) and move on to
verify computation trees, also in a bottom-up fashion. To be a proper part of
a computation tree, a configuration must describe an accepting halting
configuration or have successor configuration trees as required by the
transition relation. For type 0 configuration trees, the former case is
covered by

$\begin{array}[]{r@{\;}c@{\;}l}L_{0}\mathsf{ok}\sqcap\exists
S^{n+2}.(G_{2}\sqcap
A^{2}_{q_{a},\sigma})&\sqsubseteq&\mathsf{tree}_{0}\\\\[2.84526pt]
L_{0}\sqcap\exists S^{n+2}.(G_{2}\sqcap A^{2}_{\alpha})\sqcap\exists
S^{n+2}.(G_{2}\sqcap A^{2}_{\beta})&\sqsubseteq&C_{q_{w}}\end{array}$

where $q_{a}$ is the accepting state, $\sigma$ ranges over all elements of
$\Gamma$, and $\alpha$ and $\beta$ are distinct elements of $Q\times\Gamma$.
For the latter case and existential states, we add

$L_{0}\mathsf{ok}\sqcap\exists S^{n+2}.(G_{2}\sqcap
A^{2}_{q_{\exists},\sigma_{0}})\sqcap\exists S.(\mathsf{tree}_{1}\sqcap
A_{q_{1},\sigma_{1},M_{1}})\sqsubseteq\mathsf{tree}_{0}$

for all $q_{\exists}\in Q_{\exists}$, $\sigma_{0}\in\Gamma$, and
$(q_{1},\sigma_{1},M_{1})\in\Delta(q_{\exists},\sigma_{0})$; for universal
states, we add

$\displaystyle L_{0}\mathsf{ok}\sqcap\exists S^{n+2}.(G_{2}\sqcap
A^{2}_{q_{\forall},\sigma_{0}})\,\sqcap\quad$ $\displaystyle\exists
S.(\mathsf{tree}_{1}\sqcap
A_{q_{1},\sigma_{1},M_{1}})\,\sqcap\cdots\sqcap\exists
S.(\mathsf{tree}_{1}\sqcap A_{q_{k},\sigma_{k},M_{k}})\quad$
$\displaystyle\sqsubseteq\;\mathsf{tree}_{0}$

for all $q_{\forall}\in Q_{\forall}$ and $\sigma_{0}\in\Gamma$ when
$\Delta(q_{\forall},\sigma_{0})=\\{(q_{1},\sigma_{1},M_{1}),\dots,(q_{k},\sigma_{k},M_{k})\\}$.
Note that we have used the concept names $A_{q,\sigma,M}$ as markers here. We
still need to enforce that they really represent the transition in the
configuration tree at whose root they are located. We do this as follows. Each
marker state is the actual state in the current configuration:

$A_{q_{1},\sigma_{1},M}\sqcap\exists S^{n+2}.(G_{2}\sqcap
A^{2}_{q_{2},\sigma_{2}})\sqsubseteq C_{q_{w}}$

for all distinct $q_{1},q_{2}\in Q$, all $\sigma_{1},\sigma_{2}\in\Gamma$, and
all $M\in\\{L,R\\}$. Each marker symbol is the actual symbol written in the
current configuration:

$A_{q_{1},\sigma_{1},M}\sqcap\exists S^{n+2}.(G_{2}\sqcap W\sqcap
A^{2}_{\sigma_{2}})\sqsubseteq C_{q_{w}}$

for all distinct $\sigma_{1},\sigma_{2}\in\Gamma$, all $q_{1}\in Q$ and all
$M\in\\{L,R\\}$. Each marker movement is the actual movement in the current
configuration. To achieve this, we first say that the $W$-marker is exactly
where the head was before:

$L_{n}\sqcap\exists S^{2}.(G_{1}\sqcap A^{1}_{q,\sigma})\sqcap\exists
S^{2}.(G_{2}\sqcap\overline{W})\sqsubseteq C_{q_{w}}$

for all $q\in Q$ and $\sigma\in\Sigma$. Now, right moves are ensured in the
following way:

$\displaystyle A_{q,\sigma,R}\sqcap\exists S^{i}.[L_{i}\sqcap\exists
S.(L_{i+1}\sqcap\overline{A}_{i}\sqcap\exists S.(L_{i+2}\sqcap
A_{i}\,\sqcap\qquad$ $\displaystyle\exists S.\cdots\sqcap\exists
S.(L_{n}\sqcap A_{n}\sqcap\exists
S^{2}.(G_{2}\sqcap\overline{W})\cdots)\,\sqcap\qquad$ $\displaystyle\exists
S.(L_{i+1}\sqcap A_{i}\sqcap\exists
S.(L_{i+2}\sqcap\overline{A}_{i}\,\sqcap\qquad$ $\displaystyle\exists
S.\cdots\sqcap\exists S.(L_{n}\sqcap\overline{A}_{n}\sqcap\exists
S^{2}.(G_{2}\sqcap A^{2}_{q,\sigma})\cdots)]\sqsubseteq C_{q_{w}}$

for all $q\in Q$, $\sigma\in\Gamma$, and $0\leq i<n$. Note that this prevents
having a leaf labeled with $\overline{W}$ and a leaf to the immediate right
labeled with $A^{2}_{q,\sigma}$. We ensure that the leaves are immediate
neighbors by going one step to the right and then only to the left for the
first leaf and one step to the left and then only to the right for the second
leaf. We also have to forbid the case where we want to do a right move, but
are already on the right-most tape cell:

$\displaystyle L_{0}\sqcap\exists S^{n+2}.(G_{2}\sqcap
A^{2}_{q_{1},\sigma_{1}}\sqcap A_{0}\sqcap\cdots\sqcap A_{n-1})\;\sqcap$
$\displaystyle\exists S.(L_{0}\sqcap A_{q_{2},\sigma_{2},R})$
$\displaystyle\sqsubseteq C_{q_{w}}$

for all $q_{1},q_{2}\in Q$ and $\sigma_{1},\sigma_{2}\in\Gamma$. Left moves
can be dealt with in a similar way. To implement the transition correctly, it
remains to state that cells which are not written do not change their content.
This is straightforward:

$\begin{array}[]{r@{\;}c@{\;}l}L_{n}\sqcap\exists S^{2}.(G_{1}\sqcap
A^{1}_{\sigma_{1}})\sqcap\exists S^{2}.(G_{2}\sqcap
A^{2}_{\sigma_{2}}\sqcap\overline{W})&\sqsubseteq&C_{q_{w}}\\\\[2.84526pt]
L_{n}\sqcap\exists S^{2}.(G_{1}\sqcap A^{1}_{\sigma_{1}})\sqcap\exists
S^{2}.(G_{2}\sqcap
A^{2}_{q,\sigma_{2}}\sqcap\overline{W})&\sqsubseteq&C_{q_{w}}\\\\[2.84526pt]
\end{array}$

where $q\in Q$ and distinct $\sigma_{1},\sigma_{2}\in\Gamma$.

We need analogous concept inclusions to verify trees of type 1 and 2, setting
concept names $\mathsf{tree}^{1}$ and $\mathsf{tree}^{2}$ instead of
$\mathsf{tree}^{0}$, and to interlink these trees in the computation tree. The
main difference is that we replace the concept names $A^{i}_{a}$ and
$A^{i}_{q,a}$ with $i\in\\{1,2\\}$ with concept names that have different
values for $i$, as described above. Details are omitted.

To complete the verification of (accepting) computation trees, it remains to
set the concept name $A^{*}$ from Lemma 47 when we reach the initial
configuration. We expect that the root of the initial configuration tree is
marked with $I$ and put

$I\sqcap\mathsf{tree}^{j}\sqsubseteq A^{*}$

for all $j\in\\{0,1,2\\}$. Of course, we also need to make sure that the tree
marked by $I$ really represents the initial configuration. In particular, we
expect to see the initial state $q_{0}$, that the first $n$ tape cells are
filled with the input $w$ and that all other tape cells are labeled with the
blank symbol. All this is easy to achieve. As an example, assume that the
first symbol of $w$ is $\sigma$. Then put

$I\sqcap\exists
S^{n+2}.(G_{2}\sqcap\overline{A}_{0}\sqcap\cdots\sqcap\overline{A}_{n-1}\sqcap
A^{2}_{\alpha})\sqsubseteq C_{q_{w}}$

for every $\alpha\in\Gamma\cup(Q\times\Gamma)$ that is different from
$(q_{0},\sigma)$. To prepare for a simpler formulation of the query, we add
the final inclusions

$G_{1}\sqsubseteq G\qquad G_{2}\sqsubseteq G$

which allows us to use $G$ for identifying $G_{\ell}$-nodes, independently of
the value of $\ell$.

This ends the definition of the TBox $\mathcal{T}_{w}$. To finish the
reduction, it remains to ensure that configurations are properly copied
between configuration trees, as initially described. The _$i$ -configuration
of a configuration tree_ is the configuration represented at the leaves of
that tree using the concept names $A^{i}_{\sigma}$ and $A^{i}_{q,\sigma}$,
$i\in\\{1,\dots,6\\}$. Note that configuration trees of type 0 have 1- and
2-configurations, trees of type 1 have 3- and 4-configurations, and trees of
type 2 have 5- and 6-configurations. We say that two configuration trees are
_neighboring_ if their roots are connected by the role composition $S$. We
have to ensure the following:

  1. ($\dagger$)

if $T$ and $T^{\prime}$ are neighboring configuration trees, then the
$i$-configuration of $T$ (if existant) coincides with the $j$-configuration of
$T^{\prime}$ (if existant), for all $(i,j)\in\\{(2,3),(4,5),(6,1)\\}$.

For each of the listed pairs $(i,j)$, condition ($\dagger$) will be ensured
with a UCQ, and the final UCQ $q_{w}$ is the disjunction of these. For
simplicity, we concentrate on the case $(i,j)=(2,3)$. A bit more verbosely,
Condition ($\dagger$) can then be rephrased as follows:

  * ($\ddagger$)

if $a$ and $b$ are leaves in neighboring configuration trees of type 0 and
type 1, respectively, and $a$ and $b$ are labeled identically regarding the
concept names $A_{i},\overline{A}_{i}$, then there are no distinct
$\alpha,\beta\in\Gamma\cup(Q\times\Gamma)$ such that $a$ is labeled with
$A^{2}_{\alpha}$ and $b$ with $A^{3}_{\beta}$.

We use one CQ $q$ for each choice of $\alpha$ and $\beta$ such that $q$ has a
match precisely if there is the undesired labeling described in ($\ddagger$).

$\overline{A}_{i}$$x^{\prime}_{2n+3}$$x_{2n+3}$$x_{2n+4}$$x^{\prime}$$A_{i}$$A_{i}$$x_{2n+3}=x^{\prime}_{2n+4}$$A_{i}$$x^{\prime}=x^{\prime}_{2n+4}$$x_{2n+3}=x^{\prime}_{2n+2}$$x_{0}=x$$A_{i}$$x_{1}=x^{\prime}_{2}$$x=x^{\prime}_{0}$$x_{0}=x^{\prime}_{1}$$A_{i}$$x_{1}=x^{\prime}_{0}$$x_{0}$$x_{1}$$x$$A_{i}$$x^{\prime}_{1}$$\overline{A}_{i}$$x^{\prime}_{2n+4}$$x^{\prime}_{0}$$\overline{A}_{i}$$x_{2n+4}=x^{\prime}_{2n+3}$$x_{2n+4}=x^{\prime}$$\overline{A}_{i}$$\overline{A}_{i}$$\overline{A}_{i}$$G$$G$$A^{2}_{\alpha}$$A^{3}_{\beta}$$G$$A^{2}_{\alpha}$$G$$G$$A^{2}_{\alpha}$$G$$A^{3}_{\beta}$$A^{3}_{\beta}$

Figure 6: Component query and two identifications.

We construct $q$ from component queries $p_{0},\dots,p_{n-1}$, which all take
the form of the query show on the left-hand side of Figure 6. Note that all
edges are $S$-edges and that the only difference between the component queries
is which concept names $A_{i}$ and $\overline{A}_{i}$ are used. All variables
are quantified variables. We assemble $p_{0},\dots,p_{n-1}$ into the desired
query $q$ by taking variable disjoint copies of $p_{0},\dots,p_{n-1}$ and then
identifying (i) the $x$-variables of all components and (ii) the
$x^{\prime}$-variables of all components.

To see why $q$ achieves ($\ddagger$), first note that the variables $x$ and
$x^{\prime}$ must be mapped to leaves of configuration trees because of their
$G$-label. Call these leaves $a$ and $a^{\prime}$. Since $x$ is labeled with
$A^{2}_{\alpha}$ and $x^{\prime}$ with $A^{3}_{\beta}$, $a$ and $a^{\prime}$
must be in different trees. Since they are connected to $x$ in the query, both
$x_{0}$ and $x^{\prime}_{0}$ must then be mapped either to $a$ or to its
predecessor; likewise, $x_{2n+4}$ and $x^{\prime}_{2n+4}$ must be mapped
either to $a^{\prime}$ or to its predecessor. Because of the labeling of $a$
and $a^{\prime}$ and the predecessors in the configuration tree with $A_{i}$
and $\overline{A}_{i}$, we are actually even more constrained: exactly one of
$x_{0}$ and $x^{\prime}_{0}$ must be mapped to $a$, and exactly one of
$x_{2n+4}$ and $x^{\prime}_{2n+4}$ to $a^{\prime}$. Since the paths between
leaves in different configuration trees in the computation tree have length at
least $2n+5$ and $q$ contains paths from $x_{0}$ to $x_{2n+4}$ and from
$x^{\prime}_{0}$ to $x^{\prime}_{2n+4}$ of length $2n+4$, only the following
cases are possible:

  * •

$x_{0}$ is mapped to $a$, $x^{\prime}_{0}$ to the predecessor of $a$,
$x^{\prime}_{2n+4}$ to $a^{\prime}$, and $x_{2n+4}$ to the predecessor of
$a^{\prime}$;

  * •

$x^{\prime}_{0}$ is mapped to $a$, $x_{0}$ to the predecessor of $a$,
$x_{2n+4}$ to $a^{\prime}$, and $x^{\prime}_{2n+4}$ to the predecessor of
$a^{\prime}$.

This gives rise to the two variable identifications in each query $p_{i}$
shown in Figure 6. Note that the first case implies that $a$ and $a^{\prime}$
are both labeled with $A_{i}$ while they are both labeled with
$\overline{A}_{i}$ in the second case. In summary, $a$ and $a^{\prime}$ must
thus agree on all concept names $A_{i}$, $\overline{A}_{i}$. Note that with
the identification $x_{0}=x$ (resp. $x^{\prime}_{0}=x$), there is a path from
$x$ to $x^{\prime}$ in the query of length $2n+5$. Thus, $a$ and $a^{\prime}$
are in neighboring configuration trees. Since $a_{1}$ must satisfy
$A^{2}_{\sigma}$ and $a_{2}$ must satisfy $A^{3}_{\beta}$ due to the labeling
of $x$ and $x^{\prime}$, we have achieved ($\ddagger$).

We now show how to replace the UCQ used in the reduction with a CQ. This
requires the following changes:

  1. 1.

the $F$-nodes in configuration trees receive additional labels: when a
$G$-node is labeled with $A^{i}_{\alpha}$, then its predecessor $F$-node is
labeled with $A^{i}_{\beta}$ for all
$\beta\in(\Gamma\cup(Q\times\Gamma))\setminus\\{\alpha\\}$ and with
$A^{j}_{\beta}$ for all $j\in\\{1,\dots,6\\}\setminus\\{i\\}$ and all
$\beta\in\Gamma\cup(Q\times\Gamma)$;

  2. 2.

the roots of configuration trees receive an additional label $R_{0}$ or
$R_{1}$, alternating with neighboring trees;

  3. 3.

the query construction is modified.

Points 1 and 2 are important for the CQ to be constructed to work correctly
and can be achieved in a straightforward way by modifying $\mathcal{T}_{w}$,
details are omitted. We thus concentrate on Point 3. The desired CQ $q$ is
again constructed from component queries. We use $n$ components as shown in
Figure 6, except that the $A^{2}_{\alpha}$ and $A^{3}_{\beta}$-labels are
dropped. We further add the component (partially) shown in Figure 7 where
again $x$ and $x^{\prime}$ are the variables shared with the other components,
and where we assume that $C_{0},\dots,C_{m-1}$ are all concept names of the
form $A^{i}_{\alpha}$, $i\in\\{1,\dots,6\\}$ and
$\alpha\in\Gamma\cup(Q\times\Gamma)$.

$u^{\prime}$$x_{0,2n+4}$$x_{0,0}$$C_{0}$$x^{\prime}_{1,0}$$x$$x^{\prime}$$G$$G$$x_{m-1,2n+4}$$x_{m-2,2n+4}$$x_{2,2n+4}$$x_{1,2n+4}$$x_{m-1,0}$$x_{m-2,0}$$x_{3,0}$$x_{2,0}$$x_{1,0}$$C_{m-2}$$C_{m-1}$$C_{1}$$C_{3}$$C_{2}$$C_{m-1}$$\cdots$$\cdots$certain
targets
omitted$R_{1}$$R_{0}$$C_{m-2}$$C_{3}$$C_{2}$$C_{1}$$C_{0}$$\cdots$$x_{3,2n+4}$$u$

Figure 7: Additional component for CQ.

The dotted edges denote $S$-paths of length $2n+4$. There is an $S$-path from
every variable $x_{i,0}$ to every variable $x_{j,2n+4}$ except when $x_{i,0}$
is labeled with a concept name $C_{i}=A^{\ell}_{\sigma}$ and $x_{j,2n+4}$ with
$C_{j}=A^{k}_{\sigma^{\prime}}$ such that $(\ell,k)\in\\{(2,3),(4,5),(6,1)\\}$
and $\sigma\neq\sigma^{\prime}$. The variables $u$ and $u^{\prime}$ are
connected with the middle point of each $S$-path, that is, with the variable
on the path which has distance $n+2$ to the $x_{\ell,0}$ variable where the
path starts and also distance $n+2$ to the $x_{k,2n+4}$ variable where it
ends.

We have to argue that the CQ $q$ just constructed achieves ($\ddagger$). As
before, $x$ and $x^{\prime}$ must be mapped to leaves of configuration trees
because of their $G$-label. Call these leaves $a$ and $a^{\prime}$. All
$x_{i,0}$ must then be mapped to $a$ or its predecessor, and all $x_{i,2n+4}$
must be mapped to $a^{\prime}$ or its predecessor. In fact, due to the
labeling of $a$ and $a^{\prime}$ and their predecessors in the configuration
tree (see Point 1 above), exactly one variable $x_{i,0}$ from
$x_{0,0},\dots,x_{m-1,0}$ is mapped to $a$ while all others are mapped to the
predecessor of $a$; likewise, exactly one variable $x_{j,2n+4}$ from
$x_{0,2n+4},\dots,x_{m-1,2n+4}$ is mapped to $a^{\prime}$ while all others are
mapped to the predecessor of $a^{\prime}$. To achieve ($\ddagger$), we have to
argue that $x_{i,0}$ and $x_{j,2n+4}$ are labeled with concept names
$C_{i}=A^{\ell}_{\sigma}$ and $C_{j}=A^{k}_{\sigma^{\prime}}$ where
$(\ell,k)\in\\{(2,3),(4,5),(6,1)\\}$ and $\sigma\neq\sigma^{\prime}$, and that
$a$ and $a^{\prime}$ are in neighboring computation trees.

We start with the former. Assume to the contrary that $x_{i,0}$ and
$x_{j,2n+4}$ are not labeled with concept names in the described way. Then
they are connected in $q$ by a path of length $2n+4$ whose middle point $y$ is
connected to the variables $u$ and $u^{\prime}$. In a match to a computation
tree, there are four possible targets for $u$ and $u^{\prime}$ and for the
predecessor $y_{-1}$ of $y$ on the connecting path and the successor $y_{+1}$
of $y$ on that path:

  1. 1.

$u,y_{-1}$ map to the same target, and so do $u^{\prime}$ and $y$;

  2. 2.

$u,y$ map to the same target, and so do $u^{\prime}$ and $y_{+1}$;

  3. 3.

$u^{\prime},y_{-1}$ map to the same target, and so do $u$ and $y$;

  4. 4.

$u^{\prime},y$ map to the same target, and so do $u$ and $y_{+1}$.

However, options 1 and 3 are impossible because there would have to be a path
of length $n+1$ from a node labeled $R_{0}$ or $R_{1}$ to the leaf $a$.
Similarly, options 2 and 4 are impossible because there would have to be a
path of length $n+1$ from a node labeled $R_{0}$ or $R_{1}$ to the leaf
$a^{\prime}$. Thus, we have shown that $x_{i,0}$ and $x_{j,2n+4}$ are labeled
with concept names as described.

The labeling of $x_{i,0}$ and $x_{j,2n+4}$ with concept names
$C_{i}=A^{\ell}_{\sigma}$ and $C_{j}=A^{k}_{\sigma^{\prime}}$ where
$(\ell,k)\in\\{(2,3),(4,5),(6,1)\\}$ together with the labeling scheme of
Figure 5 also means that $a$ and $a^{\prime}$ (to which $x_{i,0}$ and
$x_{j,2n+4}$ are mapped) are not in the same configuration tree. Moreover,
they cannot be in configurations trees that are further apart than one step
because under the assumption that $x=x_{i,0}$ and $x^{\prime}=x_{j,2n+4}$,
there is a path of length $2n+5$ in the query from $x$ to $x^{\prime}$. Note
that we can identify $u$ with the $2n+2$nd variable on any such path and
$u^{\prime}$ with the $2n+3$rd variable (or vice versa) to admit a match in
neighboring configuration trees.

######  Lemma 50.

$\mathcal{T}_{w}$, $q_{w}$, $\Sigma_{w}$, and $A^{*}$ satisfy Points 1 to 4
from Lemma 47.

###### Proof.

(sketch) We have to show the following:

  1. 1.

If $M$ accepts $w$, then there is a $\Sigma_{w}$-ABox $\mathcal{A}$ and
$a\in\mathsf{Ind}(\mathcal{A})$ such that $\mathcal{A},\mathcal{T}_{w}\models
A^{*}(a)$ and $\mathcal{A},\mathcal{T}_{w}\not\models q_{w}$.

  2. 2.

If $M$ does not accept $w$, then for any $\Sigma_{w}$-ABox $\mathcal{A}$,
$\mathcal{A},\mathcal{T}_{w}\models\exists x\,A^{*}(x)$ implies
$\mathcal{A},\mathcal{T}_{w}\models q_{w}$.

  3. 3.

$q_{w}$ is FO-rewritable relative to $\mathcal{T}_{w}$ and $\Sigma_{w}$.

  4. 4.

There is an $\mathcal{E\kern-1.00006ptLI}$-concept $C_{q_{w}}$ such that $d\in
C^{\mathcal{I}}$ implies $\mathcal{I}\models q_{w}$.

(1) Take as $\mathcal{A}$ the computation tree of $M$ on $w$ viewed as an
ABox, including correct copying of configurations between neighboring
configuration trees. Let $a$ be the root of $\mathcal{A}$, marked with the
concept $I$. The verification of computation trees by $\mathcal{T}_{w}$ yields
$\mathcal{A},\mathcal{T}_{w}\models A^{*}(a)$. Since the copying of
configurations is as intended, we have $\mathcal{A},\mathcal{T}_{w}\not\models
q_{w}$.

(2) Since the verification of (homomorphic images of) computation trees by
$\mathcal{T}_{w}$ is sound, $\mathcal{A},\mathcal{T}_{w}\models\exists
x\,A^{*}(x)$ implies that $\mathcal{A}$ contains a homomorphic image of a
computation tree. Note that this tree has the initial configuration of $M$ on
$w$ as the root, locally (within configuration trees) respects the transition
relation of $M$, and has only accepting configurations as leaves. Since $M$
does not accept $w$, the tree must fail to correctly copy configurations
between neighboring configuration trees. Consequently,
$\mathcal{A},\mathcal{T}_{w}\models q_{w}$.

(3) The query $q_{w}$ contains only concept and role names that do not occur
on the right-hand side of concept inclusions except those of the form
$D\sqsubseteq C_{q_{w}}$. In fact, the FO-rewriting of $q_{w}$ relative to
$\mathcal{T}_{w}$ and $\Sigma_{w}$ is the UCQ $\widehat{q}_{w}$ that consists
of the CQ $q_{w}$ and (essentially) one CQ $q_{D}$ for each inclusion
$D\sqsubseteq C_{q_{w}}$, where $q_{D}$ is the CQ-representation of the
formula $\exists x\,D(x)$. This is a slight oversimplification, e.g. due to
our use of the markers $H$ and $W^{\prime}$ used for enforcing that each
configuration tree has at most one leaf labeled with a concept name of the
form $A^{2}_{q,\sigma}$. However, it is not hard to see that we can “expand
away” these marker concepts, which results in a UCQ to be included in
$\widehat{q}_{w}$. In particular, the markers are propagated only along the
boundedly many levels of configuration trees, so the resulting UCQ is finite.

(4) Select distinct $a,b\in\Gamma$ and set

$\begin{array}[]{r@{\,}c@{\,}l}G_{1}&=&G\sqcap\overline{A}_{0}\sqcap\cdots\sqcap\overline{A}_{n}\sqcap
A^{2}_{a}\\\\[2.84526pt]
G_{2}&=&G\sqcap\overline{A}_{0}\sqcap\cdots\sqcap\overline{A}_{n}\sqcap
A^{3}_{b}\\\\[2.84526pt] F_{1}&=&A_{0}\sqcap\cdots\sqcap
A_{n}\sqcap\mathop{\mathop{\mbox{\midmathxx\char
117\relax}}}\limits_{c\in(\Gamma\cup(Q\times\Gamma))\setminus\\{a\\}}A^{2}_{c}\,\sqcap\\\\[2.84526pt]
&&\mathop{\mathop{\mbox{\midmathxx\char
117\relax}}}\limits_{\alpha\in\Gamma\cup(Q\times\Gamma),\
j\in\\{1,3,4,5,6\\}}A^{j}_{\alpha}\\\\[2.84526pt]
F_{2}&=&A_{0}\sqcap\cdots\sqcap
A_{n}\sqcap\mathop{\mathop{\mbox{\midmathxx\char
117\relax}}}\limits_{c\in(\Gamma\cup(Q\times\Gamma))\setminus\\{b\\}}A^{3}_{c}\,\sqcap\\\\[2.84526pt]
&&\mathop{\mathop{\mbox{\midmathxx\char
117\relax}}}\limits_{\alpha\in\Gamma\cup(Q\times\Gamma),\
j\in\\{1,2,4,5,6\\}}A^{j}_{\alpha}\\\\[2.84526pt]
C_{q_{w}}&=&R_{0}\sqcap\exists S^{2n+1}.(F_{1}\sqcap\exists
S.G_{1})\,\sqcap\\\\[2.84526pt] &&\exists S.(R_{1}\sqcap\exists
S^{2n+1}.(F_{2}\sqcap\exists S.G_{2}))\end{array}$

It can be verified that $C_{q_{w}}$ has the stated property. ∎

###  E.5 Adaptation to Datalog

Our aim is to prove Theorem 17. We first introduce the relevant notions. A
_Datalog rule_ takes the form

$R_{1}(\mathbf{x}_{1})\wedge\cdots\wedge R_{n}(\mathbf{x}_{n})\rightarrow
R_{0}(\mathbf{x}_{0})$

where $R_{0},\dots,R_{n}$ are relation names and
$\mathbf{x}_{0},\dots,\mathbf{x}_{n}$ are tuples of variables such that the
length of each $\mathbf{x}_{i}$ matches the arity of $R_{i}$ and
$\mathbf{x}_{0}\subseteq\mathbf{x}_{1}\cup\cdots\cup\mathbf{x}_{n}$. For
brevity, we shall speak of relations rather than of relation names. We call
$R_{0}(\mathbf{x}_{0})$ the _head_ of the rule and
$R_{1}(\mathbf{x}_{1})\wedge\cdots\wedge R_{n}(\mathbf{x}_{n})$ the _body_. A
_Datalog program_ is a set of Datalog rules with a distinguished relation
$\mathsf{goal}$ that occurs only in rule heads. A relation is called
_extensional_ or _EDB_ if it occurs only in rule bodies; it is called
_intensional_ or _IDB_ if it occurs in at least one rule head. The _EDB
schema_ of a program is the set of all EDB relations in it. A Datalog program
is _monadic_ if all IDB relations with the possivel exception of
$\mathsf{goal}$ are unary; it is _Boolean_ if $\mathsf{goal}$ has arity zero.
We will concentrate on Boolean monadic Datalog programs. Moreover, we will
only use unary and binary EDB relations which correspond to concept and role
names from the ABox signature, respectively. IDB relations then correspond to
concept names that are not in the ABox signature. For the semantics of Datalog
and the definition of boundedness of a Datalog program, we refer to Abiteboul
et al. [1995]. We evaluate Datalog programs over $\Sigma$-ABoxes where
$\Sigma$ is the EDB schema of the program. Note that the rule body of a
Datalog program is a CQ. Tree-shapedness of a CQ $q$ is defined in the same
way as for an ABox in Section 4, that is, $q$ viewed as an undirected graph
must be a tree without multi-edges.

For convenience, we repeat the theorem to be proved.

See 17

We start with Point 1, first establishing it for rooted UCQs (a disjunction of
rooted CQs) and then strengthening to CQs. Recall the reduction of the
exponential torus tiling problem presented in Section E.1. Let $P$ be the
tiling problem that is NExpTime-complete and $c$ an input for $P$. We have
shown how to construct in polynomial time an $\mathcal{E\kern-1.00006ptLI}$
TBox $\mathcal{T}_{c}$, a rooted CQ $q_{c}(x)$, and an ABox signature
$\Sigma_{c}$ such that, for a selected concept name $A^{*}\notin\Sigma_{c}$,
$P$ has a solution given $c$ iff
$(\mathcal{T}_{c},\Sigma_{c},A^{*})\not\subseteq(\mathcal{T}_{c},\Sigma_{c},q_{c})$
over $\Sigma_{c}$-ABoxes.We show how to convert $\mathcal{T}_{c}$ and $q_{c}$
into a Boolean monadic Datalog program $\Pi_{c}$ and a rooted UCQ $p_{c}$,
both over EDB schema $\Sigma_{c}$, such that $P$ has a solution given $c$ iff
$\Pi_{c}\not\subseteq p_{c}$.

It is standard to convert an $\mathcal{E\kern-1.00006ptLI}$-concept $C$ into a
CQ $q_{C}(x)$ that is equivalent in the sense that for all interpretations
$\mathcal{I}$ and $d\in\Delta^{\mathcal{I}}$, we have $d\in C^{\mathcal{I}}$
iff $\mathcal{I}\models q_{C}[d]$. We omit the details and only mention as an
example that

$C=\exists r.\exists s.A\sqcap\exists s.B$

is converted into

$r(x,y)\wedge s(y,z)\wedge A(z)\wedge s(x,u)\wedge B(u).$

Thus, a CI of the form $C\sqsubseteq A$ can be viewed as the monadic Datalog
rule $C_{q}(x)\rightarrow A(x)$.

The monadic Datalog program $\Pi_{c}$ contains the following rules:

  1. 1.

$A(x)\rightarrow\widehat{A}(x)$ for each $A\in\Sigma_{c}$;

  2. 2.

for each CI $D\sqsubseteq A$ in $\mathcal{T}_{c}$ with $A$ a concept name
different from $A^{*}$: $q_{D^{\prime}}(x)\rightarrow A(x)$;

  3. 3.

for each CI $D\sqsubseteq A^{*}$:
$q_{D^{\prime}}(x)\rightarrow\mathsf{goal}(x)$.

where $D^{\prime}$ is obtained from $D$ by replacing each concept name
$A\in\Sigma_{c}$ with $\widehat{A}$. This renaming, as well as the rules in
Point 1 above, achieve the separation between EDB and IDB relations required
in Datalog. The rooted UCQ $p_{c}$ is the disjunction of

  1. 1.

the CQ $q_{c}$;

  2. 2.

the CQ $q_{D}$ for each $D\sqsubseteq C_{q_{c}}$ in $\mathcal{T}_{c}$.

It can be verified that $p_{c}$ is indeed formulated over EDB schema
$\Sigma_{c}$. To show that $\Pi_{c}$ and $p_{c}$ are as desired, it remains to
establish the following.

######  Lemma 51.

A $\Sigma_{c}$-ABox $\mathcal{A}$ and individual name $a$ witness
$(\mathcal{T}_{c},\Sigma_{c},A^{*})\not\subseteq(\mathcal{T}_{c},\Sigma_{c},q_{c})$
iff they witness $\Pi_{c}\not\subseteq p_{c}$.

###### Proof.

First, let $\mathcal{A}$ and $a$ be a witness of
$(\mathcal{T}_{c},\Sigma_{c},A^{*})\not\subseteq(\mathcal{T}_{c},\Sigma_{c},q_{c})$.
Then $\mathcal{A},\mathcal{T}_{c}\models A^{*}[a]$ and
$\mathcal{A},\mathcal{T}_{c}\not\models q_{c}[a]$. By the latter,

  * $(*)$

CIs from $\mathcal{T}_{c}$ that are of the form $D\sqsubseteq C_{q_{c}}$ never
apply.

Consequently and by definition of $\Pi_{c}$, from
$\mathcal{A},\mathcal{T}_{c}\models A^{*}[a]$ we obtain
$\mathcal{A}\models\Pi_{c}[a]$. By ($*$), the only CQ $q$ from $p_{c}$ that
could satisfy $\mathcal{A}\models q[a]$ is $q_{c}$. However, this is not the
case since $\mathcal{A},\mathcal{T}_{c}\not\models q_{c}[a]$.

Now let $\mathcal{A}$ and $a$ witness $\Pi_{c}\not\subseteq p_{c}$. Then
$\mathcal{A}\models\Pi_{c}[a]$ and $\mathcal{A}\not\models p_{c}[a]$. From the
latter, we get $\mathcal{A}\not\models q_{c}[a]$ and $\mathcal{A}\not\models
D[a]$ whenever $D\sqsubseteq C_{q_{c}}$ is in $\mathcal{T}_{c}$. Consequently
and since both $q_{c}$ and all such concepts $D$ contain only symbols that
never occur on the right-hand side of a CI in $\mathcal{T}_{c}$ (except when
they are of the form $D\sqsubseteq C_{q_{c}}$), we must have
$\mathcal{A},\mathcal{T}_{c}\not\models q_{c}[a]$. It thus remains to show
$\mathcal{A},\mathcal{T}_{c}\models A^{*}[a]$. However, this is immediate from
$\mathcal{A}\models\Pi_{c}[a]$ and the construction of $\Pi_{c}$. ∎

As the next step, we show how to replace the rooted UCQ $p_{c}$ with a rooted
CQ $p^{\prime}_{c}$. The general idea is to replace disjunction with
conjunction. Let the CQs in $p_{c}$ be $q_{1}(x),\dots,q_{k}(x)$ and let
$q_{i}(x_{i})$ be $q_{i}(x)$ with the answer variable $x$ renamed to $x_{i}$.
Introduce additional role names $g_{0},\dots,g_{k}$ that are included in
$\Sigma_{c}$. Then set

$\begin{array}[]{rcl}p^{\prime}_{c}(x)&=&g_{0}(x,x_{0})\wedge
g_{1}(x_{0},x_{1})\wedge\cdots\wedge g_{k}(x_{0},x_{k})\,\wedge\\\\[2.84526pt]
&&q_{1}(x_{1})\wedge\cdots\wedge q_{k}(x_{k}).\end{array}$

To make the new query work, we need to install additional gadgets in the toris
tree. Recall that every element of the

In particular, we want that for each $i\in\\{1,\dots,k\\}$, the root of the
torus tree has a $g_{i}$-predecessor $a_{i}$ which in turn has, for each
$j\in\\{1,\dots,i-1,i+1,\dots,k\\}$, a $g_{j}$-successor that is the root of
an ABox which has exactly the shape of $q_{j}$. Further, the torus tree gets a
new root $a_{0}$ that has a $g_{0}$-edge to each of the individuals
$a_{1},\dots,a_{k}$; note that the torus “tree” is actually no longer a tree.
Then a query $q_{i}$ matches at the root of the original torus tree iff
$p^{\prime}_{c}$ matches at the new root $a_{0}$. The additional parts of the
torus “tree” need to be verified in the derivation of $\mathsf{goal}$ in
$\Pi_{c}$ (which is essentially identical to the derivation of
$L_{0}\mathsf{ok}$ in $\mathcal{T}_{c}$). Given that $\Pi_{c}$ is a Datalog
program and that the rule bodies need not be tree-shaped, it is
straightforward to modify $\Pi_{c}$ to achieve this.

For Point 2 of Theorem 17, we again start with a UCQ in the first step and
improve to a CQ in a second step. The first step is exactly analogous to the
construction of $\Pi_{c}$ and $p_{c}$ above. Recall the reduction of the word
problem of exponentially space-bounded ATMs in Section E.2. Let $M$ be the ATM
whose word problem is 2ExpTime-hard and let $w$ be an input to $M$. We have
shown how to construct in polynomial time an $\mathcal{E\kern-1.00006ptLI}$
TBox $\mathcal{T}_{w}$, a Boolean CQ $q_{w}$, and an ABox signature
$\Sigma_{w}$ such that, for a selected concept name $A^{*}\notin\Sigma_{w}$,
$M$ accepts $w$ iff $(\mathcal{T}_{w},\Sigma_{w},\exists
x\,A^{*}(x))\not\subseteq(\mathcal{T}_{w},\Sigma_{w},q_{w})$ over
$\Sigma_{w}$-ABoxes. We can convert $\mathcal{T}_{w}$ and $q_{w}$ into a
monadic Datalog program $\Pi_{w}$ and a UCQ $p_{w}$ in exactly the same way in
which we had constructed $\Pi_{c}$ and $p_{c}$ above. Note in particular that
all CIs in $\mathcal{T}_{w}$ of the form $D\sqsubseteq C_{q_{w}}$ are such
that $D$ contains only symbols from $\Sigma_{w}$, and that also $q_{w}$
contains only symbols from $\Sigma_{w}$. Thus, $\Pi_{w}$ and $p_{w}$ are both
over EDB schema $\Sigma_{w}$, as required. It is straightforward to establish
the following lemma.

######  Lemma 52.

A $\Sigma_{w}$-ABox $\mathcal{A}$ witnesses
$(\mathcal{T}_{w},\Sigma_{w},A^{*})\not\subseteq(\mathcal{T}_{w},\Sigma_{w},q_{w})$
iff it witnesses $\Pi_{w}\not\subseteq p_{w}$.

It remains to replace the UCQ $p_{w}$ with a CQ $p^{\prime}_{w}$. The idea is
again similar to the proof of Point 1. However, we now want to avoid
introducing rules into $\Pi_{w}$ whose bodies are not tree-shaped. This is
possible since we work with Boolean queries here.

Apart from the original Boolean CQ $q_{w}$, let the CQs in $p_{w}$ be
$q_{1}(x),\dots,q_{k}(x)$ and let $q_{i}(x_{i})$ be $q_{i}(x)$ with the answer
variable $x$ renamed to $x_{i}$. Moreover, let $q_{k+1}(u)$ be $q_{w}()$ with
$u$ made an answer variable and let $q_{k+2}(u^{\prime})$ be $q_{w}()$ with
$u$ made an answer variable, see Figure 7 for details. Introduce additional
role names $g_{1},\dots,g_{k+2}$ that are included in $\Sigma_{w}$. Then set

$\begin{array}[]{rcl}p^{\prime}_{w}()&=&g_{1}(x_{0},x_{1})\wedge\cdots\wedge
g_{k}(x_{0},x_{k+2})\,\wedge\\\\[2.84526pt] &&q_{1}(x_{1})\wedge\cdots\wedge
q_{k+2}(x_{k+2}).\end{array}$

To make the new query work, we need to install additional gadgets in the
computation tree. In particular, we want that for each
$i\in\\{1,\dots,k+1\\}$, each node of the computation tree has a
$g^{-}_{i}$-successor which in turn has, for each
$j\in\\{1,\dots,i-1,i+1,\dots,k+1\\}$, a $g_{j}$-successor that is the root of
a tree-shaped ABox in which $q_{j}$ has a match. Then a query $q_{i}$ matches
in the computation tree iff $p^{\prime}_{w}$ matches in it. The additional
parts of the computation tree need to be verified in the derivation of
$\mathsf{goal}$ in $\Pi_{w}$ (which is essentially identical to the derivation
of $A^{*}$ in $\mathcal{T}_{w}$). This is easy to achieve, but we still have
to say what exactly the tree shape ABoxes look like in which
$q_{1},\dots,q_{k+2}$ have a match. The queries $q_{1},\dots,q_{k}$ are tree-
shaped by definition (and use only symbols from $\Sigma_{c}$) and thus we can
simply use these queries used as an ABox. For $q_{k+1}=q_{w}(u)$, we use the
concept $C_{q_{w}}$ viewed as an ABox. And finally, for
$q_{k+2}=q_{w}(u^{\prime})$, we use the ABox obtained from $C_{q_{w}}$ by
swapping the concept names $R_{0}$ and $R_{1}$.

named

## References of Appendix

  * Abiteboul et al. [1995] Serge Abiteboul, Richard Hull, and Victor Vianu  Foundations of Databases: The Logical Level  Addison-Wesley, 1995.
  * Baader et al. [2010] Franz Baader, Meghyn Bienvenu, Carsten Lutz, and Frank Wolter.  Query and predicate emptiness in description logics.  In Proc. of KR, pages 192–202, 2010.
  * Chandra et al. [1981] Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer.  Alternation.  J. ACM, 28(1):114–133, 1981.
  * Hustadt et al. [2007] Ullrich Hustadt, Boris Motik, and Ulrike Sattler.  Reasoning in description logics by a reduction to disjunctive datalog.  J. Autom. Reasoning, 39(3):351–384, 2007.
  * Kazakov [2009] Yevgeny Kazakov.  Consequence-driven reasoning for Horn SHIQ ontologies.  In Proc. of IJCAI, pages 2040–2045, 2009.
  * Lutz [2007] Carsten Lutz.  Inverse roles make conjunctive queries hard.  In Proc. of DL, volume 250 of CEUR-WS, 2007.