\subsection{\ensuremath{\ALCQ^\smallplus}\xspace, single role, UCQ}
As usual, we will show that existence of a counter-example is equivalent to existence of a special tree.

\subsubsection{From finite counter-example to tree} Lets start with finite interpretation \I.
We  will proceed with a variant of a standard unravelling. We will assume that every vertex in partially constructed tree \T is labelled by a path of elements of \I. Moreover each vertex will have exactly the same concepts as the last element of its path. Two vertices are connected if path of the source is the path of the target without the last element.

Consider a vertex $v\in \T$ such that $v$ does not have all required witnesses in \T . From the path $p_v$ labelling $v$ we extract the last element $a_v\in \I$. We will construct witnesses for $v$ from witnesses for $a_v$. Let $b$ be a witness for $a_v$. It is reachable form $a_v$ by some path $p_b$ (possibly just element $b$). For every nonempty prefix $p'\preceq p_b$ we add a new vertex to the tree \T labelled by path $p_v\cdot p'$ with the same concepts as the last element in $p'$.

The construction above obviously guarantees that all at-least requirements are satisfied. We have to check whether the at most restrictions are satisfied. Consider a vertex $v\in \T$ and let $a_v$ be the last element in the label of $v$. By construction $v$ has the same concepts as $a_v$ and successors of $v$ map injectivelly into successors of $a_v$. Therefore any at-most restriction for $v$ cannot be violated, since any such restriction was not violated for $a_v$.

There is a natural homomorphism from \T into \I , so no query not satisfied it \I can be satisfied in \T .

\subsubsection{From trees to finite couter-exaples}

Folding tree into finite structure will be a bit more complicated than in the case \ensuremath{\ALCI^\smallplus}\xspace due to long at-least restrictions.
For each concept $A$ we will introduce finite number of {\em shades} such that
\begin{itemize}
 \item every vertex with concept $A$ will get exactly one shade of $A$ as a new concept
 \item if a vertex has a restriction $\geq ^nr^+.A$ then among its descendants there are $n$ different shades of $A$
\end{itemize}
This will be done inductively in a greedy fashion. We will keep the following invariant: In the tree rooted in an unprocessed vertex each shade of each concept $A$ is used at most once. In a tree without any concept shades the invariant is trivially satisfied.

Take a n unprocessed vertex $v$ closest to the root. Suppose $v$ has a restriction of the form $\geq ^nr^+.A$. If at least $n$ of its descendants have assigned shades of $A$, then we proceed. Otherwise use some unused shades to color descendants of $v$. Notice, that we will never have to use more shades that the highest number used in the T-box.

For each concept (including shades) $C$ add a new concept $C_{\exists r\trans. C}$  axiomatizated by two inclusions: $C_{\exists r\trans. C} \sqsubseteq \exists r\trans. C$ and $\overline{C_{\exists r\trans. C}} \sqsubseteq \forall r\trans. \bar C$. Finally, we add colours  for coloured blocking principle.

Now consider a level $l$ in this tree such that all neighborings large enough for coloured blocking principle   realized in the model are present above this level.
For all nodes above level $l$ and each applicable concept choose any witness.
Preserve this witnesses and paths to them; fold the rest of the tree, redirecting the edges above level $l$.

The only nontrivial thing to check at this point is whether long at-least restrictions are satisfied. But that follows from the observations that each element satisfies its long existential restrictions for shades of concepts.

\subsubsection{Complexity}
Existence of appropriate tree will be checked by automaton. The information needed for automaton contains:
\begin{itemize}
 \item unary type of a vertex
 \item for each $A\in CN(\ensuremath{{\cal{K}}}\xspace)$, the minimum number of elements with concept $A$ in a given subtree
 \item for each $A\in CN(\ensuremath{{\cal{K}}}\xspace)$, an indicator whether we made progress looking for
elements in concept $A$.
 \end{itemize}

All together the size of automaton is equal to $(2\cdot 2 \cdot t)^{|CN(\ensuremath{{\cal{K}}}\xspace)|}$. As usual, we take the product of above automaton with automaton recognizing the query.

\subsubsection{Concepts for the query}
Assume that there are no inverse roles in the atoms of $Q$; that is, replace each $r^-(x, y)$ with $r(y, x)$ and each $(r^-)\refltrans(x, y)$ with $r\refltrans(y, x)$.\nb{In this section I use reflexive transitive closure.}

Consider an \ensuremath{\ALCOI^\smallplus}\xspace-tree.
The idea is to enrich the interpretation with concepts $C_{P, W}$ for $P$ being a \ensuremath{\CQ^\smallplus}\xspace from some class of queries and $W$ being a nonempty subset of $\textit{var}(P)$.
Such a concept will be present in all elements $x$ for which there exists a match for $P$ such that all variables from $W$ are mapped to $x$ and the whole match is contained in the subtree of $\mn{Bag}(x)$ (that is, all variables are mapped to elements in this subtree and all witnessing paths are in this subtree).
Then we will also introduce a concept $C_P$ present in the elements in which any $C_{P, W}$ is true.

We want to do it in a way possible to verify by the procedure above: that is, the new concepts will be axiomatized by concept inclusions and by forbidding some patterns in a bag (by a \ensuremath{\UCQ^\smallplus}\xspace).

\begin{definition}
We say that a \ensuremath{\CQ^\smallplus}\xspace $Q$ is \emph{connected} if for any two variables $x, y \in \textit{var}(Q)$ there is a sequence of variables $a_1, a_2, \dots, a_n$ such that $a_1 = x$, $a_n = y$ and for each pair of subsequent variables $a_i, a_{i+1}$ there is a role name $r$ such that one of the following atoms is in $Q$: $r(a_i, a_{i+1})$, $r(a_{i+1}, a_i)$, $r\refltrans(a_i, a_{i+1})$ or $r\refltrans(a_{i+1}, a_i)$.
\end{definition}

Reduce the entailment problem for arbitrary \ensuremath{\UCQ^\smallplus}\xspace to the problem for a single, connected \ensuremath{\CQ^\smallplus}\xspace.
Assume that $Q$ is a \ensuremath{\UCQ^\smallplus}\xspace and $Q = Q_1 \lor Q_2 \lor \dots \lor Q_n$, where each $Q_i$ is a \ensuremath{\CQ^\smallplus}\xspace.
First, we will show that we can assume that each $Q_i$ is connected.
Take any $Q_i$ and let $P_1, P_2, \dots, P_m$ be its connected components.
Choose one connected component for each $Q_i$ and ask for the query entailment of the disjunction of the chosen connected components; if for any choice of connected components the query is not entailed, then the whole query $Q$ is not entailed (with the same counter-model).
On the other hand, if $Q$ is not entailed, there exists a counter-model, and there is a choice of the connected components of each $Q_i$ which do not have a match in this counter-model.

Now, the reduction from a disjunction of connected queries to a single \ensuremath{\CQ^\smallplus}\xspace: assume we have already defined concepts $C_{Q_i}$ for each $Q_i$.
We can forbid some patterns inside a bag.
Thus, we can forbid a CQ $C_{Q_i}(x) \land \overline{C_Q}(x)$ for each $Q_i$ (and a fresh variable $x$) in every bag, thus assuring that if any element of the interpretation has concept $C_{Q_i}$ for any $i$, it also has concept $C_Q$.

Now we can assume that $Q$ is a single, connected \ensuremath{\CQ^\smallplus}\xspace.
We will define a class $C$ of queries (\ensuremath{\CQ^\smallplus}\xspace) for which the above concepts will be defined.

The description of the class $C$ is quite simple: first, replace each transitive atom $r\refltrans(x, y)$ in $Q$ with $r\refltrans(x, z) \land r\refltrans(z, y)$ for a fresh variable $z$ (we distinguish one node on each witnessing path; the intended meaning is that the distinguished node is some element of the highest bag through which the witnessing path passes).
We will call each such variable $z$ a \emph{distinguished variable}.
Note that each transitive atom has exactly one endpoint being a distinguished variable.
The class $C$ consists of all subqueries of $Q$ (including itself).

Now we want to axiomatize concepts for a query $P \in C$ and $W \subseteq \textit{var}(P)$.
Recall that the concept $C_{P, W}$ is supposed to be satisfied in an element $x$ if that there is a match of $P$ contained in the subtree of $\mn{Bag}(x)$, mapping all variables from $W$ to $x$.
We will define the axiomatization and prove this implication at the same time.

The left column of the table below corresponds to the proof, and the right one to the axiomatization of $C_{P, W}$.

We will look at a match for the query as a graph consisting of all witnessing paths and edges required by the query.

\begin{center}
\begin{tabular}{ m{2in} | m{1.3in} }
Assume there is a match $M$ for $P$.
Let $v$ be the highest (closest to the root) bag with nonempty intersection with the match.
Note that any witnessing path has the image of a distinguished variable as one of its endpoints.
For all witnessing paths passing through $v$, if the distinguished endpoint is not mapped to an element of $v$, let us remap it to some element of $v$ on the path (as each distinguished variable occurs only in two atoms, it is easy to see that the match is still correct).
Let $V$ be the set of elements of $v$ to which any variable is mapped. & Consider all possible subsets of variables $V' \subseteq \textit{var}(P)$. \\
\hline
For any witnessing path with one endpoint inside $V$ and the other outside $V$ (thus, outside of the bag $v$), mark the last element of $v$ on this path (that is, for a witnessing path beginning in $x \in V$, consider its longest prefix that is contained in the bag $v$ and mark the last element of this prefix).
Add all marked elements to $V$. &
For any transitive atom $r\trans(x, y)$ with one endpoint inside $V'$ and the other outside, take a fresh variable $z$ and replace the atom with $r\trans(x, z) \land r\trans(z, y)$.
Add $z$ to $V'$. \\
\hline
 & Guess which variables are mapped to the same element (i.e. consider all possible contractions; we will discard some of them).
 Let $R$ be such a ``contracted'' query.\\
\hline
Let $M_{in}$ be the match $M$ restricted to $V$ (viewed as graphs, $M_{in}$ is the subgraph induced by $V$).
Note that $M_{in}$ is connected.
Let $M_{out}$ be $M$ without the edges from $M_{in}$. &
Consider $R$ restricted to $V'$ (call it $R_{in}$) and the rest of the query $R_{out}$.
If $R_{in}$ is not connected, discard the query $R$. \comment{(maybe we don't need this?)} \\
\hline
Let $M_x$ denote a connected component of $x$ in $M_{out}$.
Consider any two different elements $x, y \in V$.
Note that $M_x$ and $M_y$ are disjoint (their elements, apart from $x$ and $y$, are in different subtrees and there are no witnessing paths between them, as they would pass through $v$, and we made sure that all such paths are split by the distinguished variables). &
For each variable $x \in V'$, let $R_x$ be the query $R_{out}$ restricted to the connected component of $x$.
If for any distinct $x, y \in V'$, $R_x$ and $R_y$ are not disjoint, discard the query R. \\
\hline
Now consider $M'_x$ as $M_x$ with $x$ removed.
$M'_x$ might consist of several connected components.
Each component is contained in the subtree of some child of $v$, connected directly to $x$.
Thus, all witnessing paths from $x$ to this connected component must pass through the entrance node of this child. &
Let $R'_x$ be $R_x$ with $x$ (and all atoms involving it) removed.
$R'_x$ might consist of several connected components.
Let $X$ be one such component.
All atoms in $R_x$ involving $x$ and one of the variables from $X$ must concern the same role; if this is not the case, discard $R$.
\end{tabular}
\end{center}
It should be clear that each match $M$ has a corresponding ``contracted'' query $R$ which captures the structure of $M$ in the bag $v$.
For each query $R$ that was not discarded, we will create auxiliary concepts $C_{R,x}$ for $x \in \textit{var}(R)$, intended to capture the corresponding matches $M$.
Now we will describe these concepts.

Recall that $R = R_{in} \land R_{out}$, as described above.
The match for the part $R_{in}$ has to be contained inside one bag.
As for $R_{out}$, for each variable $x$ from $\textit{var}(R)$, consider each connected component $X$ of $R'_x$.
Let $N(x)$ be the set of all variables $y \in \textit{var}(X)$ such that there is a non-transitive role atom in $R_x$ involving $x$ and $y$.
Furthermore, for each transitive atom involving $x$ and a variable from $X$, let $z$ be the distinguished variable corresponding to that atom \todo{describe the correspondence; the atom was probably created by splitting some transitive atom from $P$, and it had a distinguished variable as one endpoint} (think of $z$ as a fresh variable); add this atom to $X$, but with $z$ instead of $x$.
Let $D(x)$ be the set of all such distinguished variables.
Then the query for the connected component $X$ is $C_{X, N(x) \cup D(x)}$ (and it is intended to be present in the entrance node of the appropriate child bag of $v$).
It is easy to see that $X$ constructed this way is in the class $C$.
\comment{The distinguished variables magic probably requires some comment; we do it just to assure that the resulting query is in our class (we could introduce a fresh variable for the entrance node and then show that the resulting query is isomorphic to some query from the class, but it is exactly the query above).}

Thus, to deal with $R_{out}$ we just need to assure that if an element is connected to children bags with appropriate $C_{X, N(x) \cup D(x)}$ concepts in the entrance node, it has a concept denoting it.
This can be done by introducing some auxiliary concepts and simple universal CIs speaking about the complementary concepts (or just hardcoded into the local correctness conditions in the procedure above, specifically into legal children types).
This allows us to rewrite $R$ as $R_{in}$ with some additional concept atoms.
To deal with the whole query $R$, for each $x \in \textit{var}(R)$, we forbid the pattern $R \land \overline{C_{R, x}}(x)$ (note that this is an auxiliary concept, used only inside one bag; it does not need to belong to the class $C$; we also do not consider sets of variables mapped to $x$, as in $R$ the variables are already contracted).

Finally, if $R_1, R_2, \dots, R_k$ are the contracted queries which were not discarded, the target concept $C_{P, W}$ is a disjunction of all $C_{R_i, x}$ such that the variable $x$ in $R_i$ was constructed by gluing the set $W$, possibly along with some fresh variables not present in $R$.
And, again, this disjuntion is realized as a forbidden pattern: $C_{R_i, x}(y) \land \overline{C_{P, W}}(y)$ for a fresh variable $y$.

We need to also show that if there is any counter-model, there exists its conservative extension with an empty interpretation of $C_Q$.
This is straightforward: just let $C_{P, W}$ be true in an element $x$ iff there is a match of $P$ with all variables from $W$ being matched to $x$ (and $C_P$ be true if any of $C_{P, W}$ is true).
As it was a counter-model, $C_Q$ will not be satisfied, and if some part of axiomatization of $C_{P, W}$ is violated in some element $x$ (i.e. some of the forbidden patterns are violated -- note that without them all concepts $C_{P, W}$ might as well be interpreted as the whole domain), it is straightforward to construct a match for $P$ with all variables from $W$ being matched to $x$.

\subsection{Folding back the model}
\begin{definition}
An interpretation is \emph{$\ell$-bounded} if each simple directed path has length at most $\ell$.
\end{definition}
Having the concept $C_Q$, we can add to all considered KBs a CI $C_Q \sqsubseteq \bot$.
Then the procedure decides whether there exists a strong counter-example.
If it exists, there is a regular witness $(\Imc, T)$ with $T$ having bounded degree $d$ and a bound $m$ on the length of a simple directed path.
Because the tree $T$ is regular, $\Imc$ also has bounded degree and is $\ell$-bounded for some $\ell$ (there are finitely many non-isomorphic subinterpretations in the tree partition $T$ and all of them are finite).
Assume that $\Imc$ is infinite (otherwise there is no need to fold back).
Let $Q\refltrans$ be obtained from $Q$ by replacing each transitive atom $r\refltrans(x, y)$ with a disjunction:
\[ \bigvee_{i\leq \ell} r^i(x, y), \]
where $r^i(x, y)$ expresses existence of an $r$-path of length $i$ from $x$ to $y$ (i.e. for $i=0$ it states that $x = y$; for $i = 1$ it is $r(x, y)$, and for $i > 1$ it is $r(x, z_1) \land r(z_1, z_2) \land \dots \land r(z_{i-1}, y)$ for fresh variables $z_1, \dots, z_{i-1}$). Rewrite $Q\refltrans$ as a UCQ (in the disjunct for $i = 0$, all occurences of the variable $y$ are replaced with $x$). Let $k$ be a bound on the number of binary atoms in one CQ in $Q\refltrans$.

\begin{lemma}
For all $\ell$-bounded interpretations $\Jmc$, $\Jmc \models Q$ iff $\Jmc \models Q\refltrans$.
\end{lemma}

For any $n$, let $\Imc_n$ be any $n$-proper colouring of $\Imc$. \todo{write the definition of $n$-proper colourings}
Fix $n = \max(\ell^2, k^2)$. \todo{verify the bounds}
On each infinite branch $\pi$ of $T$, consider the set of nodes (bags) $V_\pi$ on $\pi$ such that $v \in V_\pi$ if the role of $v$ if $r$, but the role of its parent is $r^-$ (there are infinitely many such bags, because lengths of simple directed paths in $T$ are bounded and $\pi$ is infinite).
Let $D_\pi \in V_\pi$ be the first node for which there exists an earlier node $E_\pi \in V_\pi$ such that $N^{{\cal{I}}_n}_n(d_\pi)\simeq N^{{\cal{I}}_n}_n(e_\pi)$, where $d_\pi \in D_\pi$ and $e_\pi\in E_\pi$ are entrance nodes.
An interpretation ${\cal{F}}_n$ is obtained by including the branch $\pi$ up to the predecessor of $D_\pi$ and the edge originally leading to $d_\pi$ is redirected to $e_\pi$.

\begin{lemma}
After any number of redirections, there are no paths of lengths greater than $\ell$.
\end{lemma}
\begin{proof}
There can be no directed path passing through more than one redirected edge -- each edge is redirected to a bag over role $r$, and at all times all edges leaving this bag are by $r^-$.
For a single redirect, for any path passing through the redirected edge, a corresponding path of the same length can be easily found in the model before the redirection.
\end{proof}

\begin{lemma}
${\cal{F}}_n \models {\cal{K}}$.
\end{lemma}
\begin{proof}
We need to be sure that there is no $r$-path from $e_\pi$ to $d_\pi$ (otherwise the KB could be violated, as $e_\pi$ might require some witness below $d_\pi$).
This is guaranteed by taking neighbourhoods of size larger than $l$ (bound on the length of a simple directed path).
\end{proof}

By the coloured blocking principle, ${\cal{F}}_n \not\models Q\refltrans$, and as it is $\ell$-bounded, ${\cal{F}}_n \not\models Q$.
Thus, there exists a finite counter-model.

\subsection{Finding a strong counter-example}
First we will assume some additional properties of the strong counter-example that we will look for.
\begin{lemma}
If there is any strong counter-example, there is also one with the following property: for every element $x$, in the subtree of $\mn{Bag}(x)$ there are all witnesses required for $x$ by existential CIs in the TBox of ${\cal{K}}$.
\end{lemma}
\begin{proof}
(sketch) For any element $x$ we can duplicate the subtree of $\mn{Bag}(x)$ (there is an obvious homomorphism, so nothing changes wrt. KB and query).
We can also root the tree in another bag, duplicate some subtree and restore the original root.
Thus, if the required witnesses are not in the subtree, we can just duplicate whole interpretation apart from the subtree and add the copy as a fresh child.
\end{proof}

\begin{definition}
A \emph{bag type} of a non-root bag $v$ of an SCC-partition is the following triple:
\begin{itemize}
  \item the role $r_v$ on the label of the incoming edge in the tree (this is either $r$ or $r^-$, where $r$ is the unique role used by ${\cal{K}}$);
  \item the unary type $\tau_v$ of its entrance node $e_v$;
  \item the set $\mn{Reach}$ of concept names reachable from $e_v$ by $r_v$ (in the subtree of $v$ -- this is implicit, because the only edge pointing upwards the tree is by role $r_v^-$).
\end{itemize}
\end{definition}
\begin{lemma}
If there is any strong counter-example $(\Imc, T)$, there is also one with the following property: for any element $x \in \Delta^\Imc$, bag types of children of $\mn{Bag}(x)$ such that there is an edge from $x$ to the entrance node of this bag are distinct. \todo{state it more clearly}
\end{lemma}
\begin{proof}
If there are two children of $\mn{Bag}(x)$ with the same bag type and with edges from $x$ to the entrance nodes of both of them, one of these edges (and one of the children, along with its whole subtree) can be removed.
Removing some elements cannot make the query satisfied; and as the bag type contains information about the unary type of the entrance node and all concepts reachable from it by the role of the incoming edge, all the witnesses required by CIs in subtree of one of the children can be found also in the subtree of the other one.
\end{proof}

Consider some strong counter-example $(\Imc, T)$ and any bag $v$ from $T$.
One can look at the subtree rooted in $v$ (and the corresponding subinterpretation of $\Imc$, along with the nominals) as a strong counter-example for the same query and different KB, with ABox containing only one individual with fully specified unary type (corresponding to the entrance node of $v$) and the same TBox as ${\cal{K}}$.
The intermediate goal is to develop a procedure calculating the set of bag types for which such a strong counter-example exists.
At the end we want to reduce this problem to the existence of an interpretation corresponding to a single bag, assuring some simple local conditions between the bag and its children.

We will describe the procedure determining existence of a strong counter-example by describing simpler procedures and gradually getting nearer the goal.
Begin with assuming that the query is trivial; thus, we want to find any safe model of ${\cal{K}}$.
The strategy is to search for an appropriate \ensuremath{\ALCOI^\smallplus}\xspace-tree (we will still call it a strong counter-example, even though the query is trivial).

Let $\tau = (r, \sigma, R)$\vic{THis notation needs to be introduced} be a bag type and $T$ be a set of bag types.
The situation we consider is a bag of type $\tau$ with children of types from the set $T$ (the types of children can repeat and not all types from $T$ has to be used).
We want to define some \emph{local correctness conditions} that must be satisfied in such a situation (essentially: existence of a model of a single bag; but as some witnesses required by the TBox might be present in the subtrees of its children, it depends on the bag types of children).
Namely, we will construct an \ensuremath{\ALCOI^\smallplus}\xspace-knowledge base ${\cal{K}}_{\tau, T}$ and a non-transitive UCQ $Q_\tau$ such that if ${\cal{K}}_{\tau, T} \models_{\mathsf{fin}} Q_\tau$, there is no strong counter-example in which the considered situation occurs (i.e. there is a bag of type $\tau$ with children of types from $T$).

We will first construct an auxiliary knowledge base ${\cal{K}}_\tau$, independent of $T$.
Begin with the copy of the TBox of ${\cal{K}}$ restricted to the role $r$.
For every concept $B$ add fresh concepts $B_{in}, B_{out}, B_{exit}, B_{any}$ and the following CIs:
\begin{itemize}
  \item $B_{in} \sqsubseteq \exists r\trans. B$,
  \item $B_{out} \sqsubseteq \exists r\trans. B_{exit}$,
  \item $B_{any} \sqsubseteq B_{in} \sqcup B_{out} \sqcup B_{exit}$,
\end{itemize}
and replace every CI of the form $A \sqsubseteq \exists r\trans. B$ by a CI $A \sqsubseteq B_{any}$.
The concepts $B_{in}$ are supposed to be satisfied in the elements that can reach concept $B$ inside the bag;
$B_{exit}$ -- in the elements from which there exists an $r$-edge going to some child bag with reachable concept $B$;
$B_{out}$ -- the ones that can reach $B$ outside the bag through $B_{exit}$;
$B_{any}$ -- any of the above.
Finally, set the ABox of ${\cal{K}}_\tau$ to $\{A(b) \mid A \in \sigma\} \cup \{A_{any}(b) \mid A \in R \}$ (recall that $R$ is the third component of the bag type $\tau$ -- the set of concepts reachable from the entrance node by $r$).

Now construct ${\cal{K}}_{\tau, T}$.
Begin with a copy of the ABox and all non-existential CIs of ${\cal{K}}_\tau$.
We need to know which existential CIs need to be satisfied inside the bag, and which ones will have witnesses in the children (or their subtrees).
To deal with this, we will assume that each element $x$ of the resulting model has edges to all possible bag types from $T$, as long as this does not invalidate the knowledge base.
Checking whether adding an edge to the model invalidates the knowledge base requires just looking at the unary types of its endpoints.
As a result, for each unary type $\sigma$ in ${\cal{K}}_\tau$ we can easily calculate the set of its \emph{legal children types}: the bag types for which the edge from an element with unary type $\sigma$ to the entrance node of such a bag type does not invalidate the knowledge base.
Add to ${\cal{K}}_{\tau, T}$ a fresh concept $A_\sigma$ for each unary type $\sigma$ in ${\cal{K}}_\tau$, with the natural axiomatization.
For each such unary type $\sigma$ and each existential CI $C$ of the form $A \sqsubseteq \exists r. B$ from ${\cal{K}}_{\tau}$ (where $A \in \sigma$), check whether $C$ is witnessed in any of its legal children types (i.e. if the unary type of its entrance node contains $B$).
If not, add to ${\cal{K}}_{\tau, T}$ a new CI $A_\sigma \sqsubseteq \exists r. B$.
Similarly add all transitive existential CIs not witnessed in the legal children types (i.e. if no legal children bag type has an appropriate concept in the set $\mn{Reach}$ of reachable concepts).
Additionally, there are two cases in which the unary type $\sigma$ becomes forbidden.
If $\sigma$ contains a concept $B_{exit}$ for some $B$, check whether any of its legal children types by role $r$ has $B$ in the set of reachable nodes; if not, this unary type is forbidden.
Also, for the existential CIs involving roles other than $r$, if there is at least one of them which is not witnessed by the legal children types, $\sigma$ is forbidden.
Forbidding a type means that we add to $Q_\tau$ a simple CQ $\bigwedge_{A \in \sigma} A(x)$ for a fresh variable $x$.\nb{This can be either in the query or we can use the finite entailment modulo types; I'm not sure how it influences the complexity.}

\subsubsection{The procedure}\vic{What are the realizability/compatibility conditions to decide when to eliminate a type}
The algorithm will be a variant of type elimination \cite{Pratt79,abs-1202-0914}.\textcolor{green}{(?)}
Begin with the set of all possible bag types $T_0 = \mn{rol}({\cal{K}}) \times \mn{Tp}({\cal{K}}) \times {\cal{P}}(\mn{Tp}({\cal{K}}))$.
For $T \subseteq T_0$ let $F(T)$ be the set of types $\tau \in T$ such that there exists a finite model of ${\cal{K}}_{\tau, T}$.
Note that $F$ is a monotone operator on subsets of $T_0$.
Consequently, $F$ has the greatest fixed point and it can be obtained by iterating $F$ on $T_0$:
\[T_0 \supseteq F(T_0) \supseteq F^2(T_0) \supseteq \dots \supseteq F^i (T_0) = F^{i+1} (T_0) \] for some $i\leq |T_0|$.
Let $T = F^{i}(T_0)$.
Removal of some bag type $\tau$ during this procedure witnesses that if an \ensuremath{\ALCOI^\smallplus}\xspace-tree contains a bag $v$ of such type, if we consider the subtree of $v$ as an \ensuremath{\ALCOI^\smallplus}\xspace-tree of bag type $\tau$, it has to violate some local correctness conditions and therefore the whole \ensuremath{\ALCOI^\smallplus}\xspace-tree cannot model ${\cal{K}}$.
Now we want to check whether there exists an interpretation corresponding to the root bag, realizing the ABox of ${\cal{K}}$ with children bag types from $T$.
For this, simply check the local conditions as in the case of ${\cal{K}}_{\tau, T}$, but this time copy the ABox from ${\cal{K}}$.

If the above procedure is successful, there is an \ensuremath{\ALCOI^\smallplus}\xspace-tree with root bag realizing the ABox of ${\cal{K}}$.
However, it might not be safe, and therefore might not even model ${\cal{K}}$ (the transitive existential CIs might not be satisfied -- each bag type on some infinite path may have some concept in its set of reachable concepts, but it might never be actually reached).

Assuring safety requires the following modification of the above procedure.
Instead of adding each bag separately, we will add whole (finite) connected components by one role at once and assure that we add such components for alternating roles.
By a connected component by role $r$ we mean all bags reachable by role $r$ (\emph{not} by role $r^-$) from a given bag $v$, where the role of $v$ is $r$ and the role of parent of $v$ is different than $r$.

Once again, we are interested in local correctness conditions for such a connected component.
More precisely, now we are given a role $r$ and a set of bag types $S$ by roles different than $r$ (possibly $r^-$) and we consider a finite connected component of bags by role $r$ such that all edges leaving this component lead to bags of types from $S$.
This component, of course, is a tree.
We want to first calculate the set of bag types that could be the leaves of such a tree (without violating the local correctness conditions), and then, inductively, other realizable bags.
Begin with an empty set of bag types $T_0 = \emptyset$ -- allowed types of children by role $r$.
For
\[ T \subseteq \{r\} \times \mn{Tp}({\cal{K}}) \times {\cal{P}}(\mn{Tp}({\cal{K}})) \]
and
\[ S \subseteq (\mn{rol}({\cal{K}})\setminus\{r\}) \times \mn{Tp}({\cal{K}}) \times {\cal{P}}(\mn{Tp}({\cal{K}})) \]
let $F_S(T)$ be the set of bag types $\tau \in T$ such that there exists a finite model of ${\cal{K}}_{\tau, T\cup S}$.
As $F$ is a monotone operator on sets of bag types with role $r$, it has the lowest fixed point and it can be obtained by iterating $F_S$ on an empty set.

The whole procedure for deciding existence of a strong counter-example (for a trivial query) works as follows.
Begin with the set $T_0$ of all bag types.
Let $T[r]$ denote the set of all elements of $T$ (bag types) with the first coordinate (role) equal to $r$.
Let $F_r(T)$ be the set of types $\tau \in T[r]$ realizable by a finite connected component by role $r$ in ${\cal{K}}_{\tau, T \setminus T[r]}$.
Take any order of the roles and apply each $F_r$ to the set under construction $T$.
Repeat this procedure until $T$ stabilizes (it must happen, as each $F_r$ is monotone).
Take the resulting set of types $T$ and check, as before, whether the root bag realizing ABox of ${\cal{K}}$ has a model satisfying the local correctness conditions with children bag types from $T$.

\subsubsection{Correctness and regularity}
It is easy to see that, if there exists any strong counter-example, its tree of bag types is a witness that the procedure will be successful.
Assuming the contrary, if $S$ is the set of all bag types occuring in this tree, consider the first moment when any $\tau \in S$ would be removed from the set $T$ of the types considered by the procedure.
It must mean that for some set $T \supseteq S$, the type $\tau$ is not realizable by any finite connected component by role $r$ in ${\cal{K}}_{\tau, T \setminus T[r]}$, where $r$ is the role of $\tau$.
However, $\tau$ is a part of some finite connected component in the strong counter-example.
By considering all bag types in this connected component, bottom-up, one can easily check that the procedure will not remove $\tau$ from the set of considered bag types.

For the other direction: if the above procedure is successful, it essentially calculates a regular infinite tree of bag types, such that there exists an interpretation for each of these bags which is locally correct.
For each bag type $\tau$ and each set of bag types $T$ such that in this tree there is a bag type $\tau$ with children of types $T$, fix some model $\Imc_{\tau, T}$ of ${\cal{K}}_{\tau, T}$.
Fix also any model of the KB for the root bag. \todo{Define it earlier properly and name it somehow?}
Let $\Imc$ be the interpretation consisting of all chosen interpretations for single bags (with all instances of nominals merged), along with the edges between elements of parent bags and entrance nodes of their children (according to the assumptions inside the procedure: if an edge from $x$ to some bag type does not invalidate the knowledge base, add an edge from $x$ to one of the children with this bag type).
$\Imc$ is a model of ${\cal{K}}$: all universal CIs are satisfied inside the bags and, by the construction of the edges between the bags, cannot be violated by them.
The existential CIs are either satisfied inside bags, or are guaranteed to be satisfied in a subtree of one of the children; for the transitive ones it can be proved by a simple induction in one connected component.

\subsubsection{Bounded degree}
There are finitely many interpretations $\Imc_{\tau, T}$ of single bags that we used to construct $\Imc$.
If $k$ is the size of the biggest of them and $l$ is the number of possible bag types, the degree of the tree is bounded by $kl$ (and $l \leq |{\cal{K}}|\cdot 2^{|{\cal{K}}|} \cdot 2^{|{\cal{K}}|}$).

\subsubsection{Non-trivial queries}
For non-trivial queries only some details of the procedure change.
We will extend the knowledge base with some concepts related to the query; in particular, we will add a concept $C_Q$ such that, if there is any match for concept $Q$, the interpretation of $C_Q$ will not be empty.
To assure this, apart from the standard CIs, we will need to forbid some patterns inside the bags.
This will be handled by adding these patterns to all the queries $Q_\tau$ used when verifying local correctness conditions for a single bag and its children bag types.

\section{Eliminating multiple roles}~\label{sec:app:mulroles}

\subsection{Unravelling}
Let $\Imc$ be a finite counter-model.
Let $\Imc_r$ for $r \in \mn{rol}({\cal{K}})$ be a projection of $\Imc$ to the signature containing only one role name $r$.

We construct a tree-like model $\Jmc$.
We will maintain a homomorphism $h: \Delta^\Jmc \to \Delta^\Imc$ -- each element will be added to $\Jmc$ as a copy of some element of $\Imc$.
Choose any role $r \in \mn{rol}({\cal{K}})$; the root bag is a copy of $\Imc_r$, identifying the individual with its copy.

Then, recursively, for each added element $x$ proceed as follows:
let $r$ be the role name of the bag in which $x$ was created; for each role name $s \in \mn{rol}({\cal{K}})\setminus \{r\}$, add a fresh copy of $\Imc_s$ as a child bag, identifying $x$ with its fresh copy in $\Imc_s$.
Repeat the procedure for each created element.

$\Jmc \models {\cal{K}}$, as the ABox is satisfied by the root bag and each CI from the TBox concerns only one role.
The homomorphism $h$ from $\Jmc$ to $\Imc$ witnesses that \Jmc does not satisfy $Q$.

\subsection{Proof of Lemma~\ref{lem:multirolesconsistent}}
\subsubsection{The correct $Q$-labelling is consistent.}
Assume the contrary: that a labelling ${\cal{I}}'$ is correct and inconsistent.
Inconsistency means that for some bag there exists a subquery $p'$ of $Q$, its partition $p, p_1, p_2, \dots, p_k$ with $\textit{var}(p_i)\cap\textit{var}(p_j) = \emptyset$ for all $i \neq j$, $V_i = \textit{var}(p_i)\cap\textit{var}(p)$, $\emptyset \neq V \subseteq \textit{var}(p)$, and a match $\eta$ for $p$ in the bag, such that $\eta(V_i) = \{e_i\} \subseteq A_{p_i, V_i}^{{\cal{I}}'}$ for all $i$, but $\eta(V) \subseteq \{e\} \not\subseteq A_{p', V}^{{\cal{I}}'}$.
As each $e_i \in A_{p_i, V_i}^{{\cal{I}}'}$, there is a match $\eta_i$ witnessing this, with $\eta_i(V_i) = \{e_i\}$.
The matchings $\eta, \eta_1, \eta_2, \dots, \eta_k$ are consistent with each other (i.e. each variable of $p'$ is mapped to the same element in all matchings in which it occurs), so they can be combined into a match $\eta'$ for $p'$ in ${\cal{I}}'$ (i.e. $\eta' = \eta \cup \bigcup_{i=1}^k \eta_i$) such that $\eta'(V) = \eta(V) \subseteq \{e\}$, thus contradicting the correctness of ${\cal{I}}'$.

\subsubsection{If ${\cal{I}}$ admits a consistent $Q$-refutation, then the correct $Q$-labelling of ${\cal{I}}$ is a $Q$-refutation.}
We will show that if a $Q$-labelling ${\cal{I}}'$ is consistent and $e \notin A_{p, V}^{{\cal{I}}'}$, then in the correct $Q$-labelling ${\cal{I}}''$ also $e \notin A_{p, V}^{{\cal{I}}''}$.
Assume the contrary: that ${\cal{I}}'$ is a consistent $Q$-labelling, but for some connected fragment $p'$ of $Q$, some $\emptyset \neq V \subseteq \textit{var}(p')$, there exists an element $e$ of ${\cal{I}}'$ such that $e \notin A_{p', V}^{{\cal{I}}'}$, even though there exists a match $\eta$ for $p'$ in ${\cal{I}}'$ such that $\eta(V) \subseteq \{e\}$.
From all values of $p', V$ and $e$ for which this happens, choose ones where $p'$ is minimal.
Fix a corresponding match $\eta$ for $p'$.

The image of $\eta$ is not contained inside one bag: assuming it is, for a trivial partition of $p'$ into one part $p$, the consistency condition is clearly violated in this bag -- there exists a match for $p$ in the bag, but $\eta(V) \subseteq \{e\} \not\subseteq A_{p',V}^{{\cal{I}}'}$.

Notice that for any binary atom from $p'$, $r(x, y), r^*(x, y)$ or $x = y$, there is a bag to which both $\eta(x)$ and $\eta(y)$ belong; for $r(x, y)$ and $x = y$ this is trivial, and for $r^*(x, y)$ this is true because any two neighbouring bags (i.e. sharing an element) have edges over different roles.
Take any atom from $p'$ mentioning any element of $V$.
Take a bag containing the image of variables mentioned by this atom under $\eta$ (i.e. if it mentions just one variable $x$, take any bag containing $\eta(x)$; if it mentions two variables $x, y$, take any bag containing $\eta(x)$ and $\eta(y)$).
We claim that the compatibility condition in this bag is violated.
Let $p$ be a maximal connected subquery of $p'$ such that $e \in \eta(\textit{var}(p))$ and $\eta(\textit{var}(p))$ is contained in the chosen bag.
It is easy to see that $p' \setminus p$ seen as a set of connected components $p_1, \dots, p_k$ satisfies the required conditions: the components have disjoint variables by definition; by the definition of the tree structure of the bags (specifically, by condition (1): two bags share a single element if they are neighbours and are disjoint if they are not neighbours), $\eta(\textit{var}(p_i)\cap\textit{var}(p)) = \{e_i\}$ for some $e_i$; and by minimality of $p'$, $e_i \subseteq A_{p_i,V_i}^{{\cal{I}}'}$.

\subsection{Proof of Fact~\ref{fact:emptiness}}

Let $\mathsf{step}_{\cal{B}}(X) = \left \{ q \in S \bigm | (X,q) \in
\mathsf{step}_{\cal{B}}\right\}$. Consider the mapping $G(X) = X \cup
\mathsf{step}_{\cal{B}}(X) $. Because $G$ is monotone and inflationary, for
each $P$ it has the least fixed point $\mathsf{step}^*_{\cal{B}}(P) $ that
contains $P$, and the fixed point can be computed by iterating $G$
over $P$.  It is straightforward to see that $\mathsf{step}^*_{\cal{B}}(P)$
is the set of states $q$ such that there exists a \emph{finite}
partial run of $A$, whose leaves are labelled with elements of $P$ and
the root is labelled with $q$.  Consider now the mapping $H(X) =
\mathsf{step}^*_{\cal{B}}(X \cap F)$. It is monotone and its greatest fixed
point $R$ can be computed by iterating it on $S$. Again, it is not
difficult to see that ${\cal{B}}$ accepts some tree iff $I \cap R \neq
\emptyset$. As all the sets and functions above are computable in
polynomial time using the available oracle for $\mathsf{step}_{\cal{B}}$,
this gives a polynomial algorithm for non-emptiness.

\section{Eliminating Nominals, Trivializing ABoxes}~\label{sec:ABoxesNom}
We prove three results: for the logic $\ensuremath{\ALCOI^\smallplus}\xspace$, for a restricted variant of $\ensuremath{\ALCOQ^\smallplus}\xspace$ logic (without at-most restrictions over transitive closures of roles), and for the full $\ensuremath{\ALCOQ^\smallplus}\xspace$ logic.
We start with the simplest proof, and then describe additional components needed in the subsequent proofs.

\subsection{$\ensuremath{\ALCOI^\smallplus}\xspace$}
As there is no counting in the logic, for a role $r$ and a concept name $A$, we will use the standard notation
\[ \forall r. A\,, \quad \forall r^*. A\,, \quad \exists r. A\,, \quad \exists r^*. A\,, \]
instead of
\[ \qnrleq 0 r {\overline{A}}\,, \quad \qnrleq 0 {r^*} {\overline{A}}\,, \quad \qnrgeq 1 r A\,, \quad \qnrgeq 1 {r^*} A\,, \]
respectively.
Note that restrictions of the form $\qnrleq n {r^*} A$ for $n = 0$ can be eliminated using stickiness, and for $r$ being an inverse role they are not present in the normal forms that we assume throughout the paper.
In this section we will use them for the sake of brevity, highlighting the places where it might create confusion.

Let ${\cal{K}} = ({\cal{T}}, {\cal{A}})$ be an $\ensuremath{\ALCOI^\smallplus}\xspace$ knowledge base, $Q \in \ensuremath{\UCQ^\smallplus}\xspace$ with $\ensuremath{\CQ^\smallplus}\xspace$s of size at most $m$.
One can decide if ${\cal{K}} \models_{\mathsf{fin}} Q$ in time
$\mathrm{poly}(\|{\cal{K}}\|, (2m)^{|Q|\cdot\|{\cal{K}}\|^{O(m)}})$
using oracle calls to finite entailment over $\ensuremath{\ALCI^\smallplus}\xspace$ KBs of size at most
$\mathrm{poly}(\|{\cal{K}}\|)$,
with trivial ABoxes and unions of at most
$|Q| \cdot \|{\cal{K}}\|^{O(m)}$
$\ensuremath{\CQ^\smallplus}\xspace$s of size $O(m)$.

We present the result as an oracle reduction; however, it is worth noting that it can be seen as a \emph{truth-table reduction}~\cite{post1944,LADNER1975103}; that is, the calls to the oracle are not adaptive.

\subsubsection{Modifying the KB}
\begin{itemize}
 \item Replace each transitive role atom $r^*(a, b)$ in the ABox with a CI in the TBox: $\{a\} \sqsubseteq \exists r^*. \{b\}$.
 \item For each nominal $\{a\}$ and role $r$ introduce fresh concept names $A_a \equiv \{a\}$, $A_{r,a} \equiv \exists r. \{a\}$ and $A_{r^*, a} \equiv \exists r^*. \{a\}$.
 \item Normalize the knowledge base. We will denote all concept names present in the KB after the normalization as \emph{original} concept names.
 \item Introduce \emph{auxiliary} concept names: for each original concept name $A$ and each role $r$ introduce concept names $C_{\exists r. A}$ and $C_{\exists r^*. A}$, with the following axiomatization:
       \[ C_{\exists r. A} \sqsubseteq \exists r. A\,,\quad \overline{C_{\exists r. A}} \sqsubseteq \forall r. \overline{A}\,, \]
       \[ C_{\exists r^*. A} \sqsubseteq \exists r^*. A\,,\quad \overline{C_{\exists r^*. A}} \sqsubseteq \forall r^*. \overline{A}\,. \]
       To preserve the normal form, the last CI is split into two:
       $\overline{C_{\exists r^*. A}} \sqsubseteq \overline{A}$ and
       $\overline{C_{\exists r^*. A}} \sqsubseteq \forall r. \overline{C_{\exists r^*. A}}$.
\end{itemize}
From now on, let ${\cal{K}}$ denote the KB after above modifications.

\subsubsection{Unravelling}
\begin{definition}
Let ${\cal{I}}$ be a model of ${\cal{K}}$ and $x \in \Delta^{\cal{I}}$.
A \emph{witnessing set} for $x$ is a set $S$ of pairs $(y, r)$, where $y \in \Delta^{\cal{I}}$ and $r$ is a role, such that:
\begin{itemize}
 \item for every $(y, r) \in S$, $y$ is a direct $r$-successor of $x$;
 \item for each CI of the form $A \sqsubseteq \exists r. B$ such that $A \in \mn{tp}^{{\cal{I}}}(x)$, there exists $(y, r) \in S$ such that $y$ is in concept $B$;
 \item for each CI of the form $A \sqsubseteq \exists r^*. B$ such that $A \in \mn{tp}^{{\cal{I}}}(x)$, either $B \in \mn{tp}^{{\cal{I}}}(x)$ or there exists $(y, r)\in S$ such that $y$ is in concept $C_{\exists r^*. B}$.
\end{itemize}
\end{definition}
Observe that in any minimal witnessing set there are at most as many elements as there are CIs in the TBox.
We will call an element $y$ a \emph{required witness} for $x$ if $y$ is present in every witnessing set for $x$.

\begin{lemma}
If ${\cal{K}} \not\models_{\mathsf{fin}} Q$, there exists a counter model $\Imc$ which can be decomposed into domain-disjoint intepretations ${\cal{I}}\upharpoonright \mn{ind}({\cal{K}})$ and ${\cal{I}}_1, \dots, {\cal{I}}_n$ for some $n \leq \|{\cal{K}}\| \cdot |\mn{ind}({\cal{K}})|$ with two kinds of additional edges:
arbitrary edges connecting elements from $\bigcup_i\Delta^{{\cal{I}}_i}$ with elements from $\mn{nom}({\cal{K}})$, and a single edge connecting a distinguished element $d_i\in\Delta^{{\cal{I}}_i}$ with a corresponding element $e_i \in \mn{ind}({\cal{K}})$ for each $i\leq n$.
Moreover, one can assume that:
\begin{itemize}
 \item if $e_i$ is not a nominal, $e_i$ is not a required witness for $d_i$,
 \item for any nominal $a$,
 $\{(b, r): b \in \mn{ind}({\cal{K}}), (a, b) \in r^{\cal{I}}\} \cup \{(d_i, r_i): e_i = a\}$ is a witnessing set for $a$.

\end{itemize}
\end{lemma}
\begin{proof}
This can be achieved by routine one-step unravelling from the individuals.
Let ${\cal{J}}$ be any counter-model.
${\cal{I}}$ is constructed as follows.
Take a copy of ${\cal{J}} \upharpoonright \mn{ind}({\cal{K}})$.
For every individual $x \in \mn{ind}({\cal{K}})$, take any minimal witnessing set $S$ for $x$ in ${\cal{J}}$.
For each $(y, r) \in S$, add a fresh copy of the whole interpretation ${\cal{J}}$ to ${\cal{I}}$, identifying the nominals, and add an $r$-edge from $x$ to the newly created copy of $y$.
As each element and each edge in ${\cal{I}}$ was created as a copy of some element or edge in ${\cal{J}}$, there is a homomorphism from ${\cal{I}}$ to ${\cal{J}}$ witnessing that ${\cal{I}} \not\models Q$.
\end{proof}

\subsubsection{Constructing KBs for ${\cal{I}}_i$.}
We search for a counter-model admitting the described decomposition.
We will refer to ${{\cal{I}}\upharpoonright \mn{ind}({\cal{K}})}$ as $\ensuremath{{\cal{I}}_0}$.
Iterate through all possible interpretations $\ensuremath{{\cal{I}}_0}$ \comment{($4^{|\mn{ind}({\cal{K}})|^2\cdot|\mn{rol}({\cal{K}})|}\cdot 2^{|\mn{ind}({\cal{K}})|\cdot|\mn{CN}({\cal{K}})|}$ options)} and perform the rest of the procedure for a fixed $\ensuremath{{\cal{I}}_0}$; a counter-model exists iff it exists for some of these choices.

We will construct KBs representing abstractly ${\cal{I}}_i$ for $1 \leq i \leq n$; these KBs will have some additional concept names: $D_{\exists r. A} \equiv \exists r. A$ and $D_{\exists r^*. A} \equiv \exists r^*. A$, for each role $r$ and original concept name $A$.
Their meaning is similar to the auxiliary concept names, but they are supposed to represent having appropriate (direct) $r$-successor \emph{inside one interpretation ${\cal{I}}_i$}, while the auxiliary concept names speak about the whole interpretation ${\cal{I}}$.
We will call them \emph{local auxiliary concept names}.
For any choice of a unary type $\tau$ containing both concept names from ${\cal{K}}$ and the local auxiliary concept names (or their complements), let ${\cal{K}}_\tau$ be the KB ${\cal{K}}$ with the following modifications:
\begin{itemize}
 \item the ABox is $\left\{A(b) \bigm | A \in \tau\right\}$ for a fresh individual $b$;
 \item remove the axiomatization of concept names $A_{r, a}$;
 \item replace the axiomatization of the auxiliary concept names:
       \[ C_{\exists r. A} \equiv \exists r. A \sqcup \bigsqcup_{\substack{a \in \Nom({\cal{K}})\\A(a) \in {\cal{A}}}} A_{r, a}\,, \]
       \[ C_{\exists r^*. A} \equiv \exists r^*. A \sqcup \bigsqcup_{\substack{a \in \Nom({\cal{K}})\\ C_{\exists r^*. A}(a) \in {\cal{A}}}} \exists r^*. A_{r, a}\,, \]
 \item for each nominal $\{a\}$, each $A$ such that $A(a) \in {\cal{A}}$ and each role $r$:
 \begin{itemize}
  \item for each CI of the form $A \sqsubseteq \forall r. B$ add a new CI $A_{r^-, a} \sqsubseteq B$ to the TBox;
  \item for each CI of the form $A \sqsubseteq \forall r^*. B$ add a new CI $A_{r^-, a} \sqsubseteq \forall r^*. B$ to the TBox;
 \end{itemize}
 \item remove all CIs with a nominal on the left-hand side;
 \item replace CIs by the following rules, for any original concept names $A$, $B$ and any role $r$ (by the previous point, $A$ is not a nominal):
 \begin{itemize}
  \item $A \sqsubseteq \exists r. B \longrightarrow A \sqsubseteq C_{\exists r. B}$;
  \item $A \sqsubseteq \forall r. B \longrightarrow A \sqsubseteq \overline{C_{\exists r. \overline{B}}}$;
  \item $A \sqsubseteq \exists r^*. B \longrightarrow A \sqsubseteq C_{\exists r^*. B}$;
  \item $A \sqsubseteq \forall r^*. B \longrightarrow A \sqsubseteq \overline{C_{\exists r^*. \overline{B}}}$;
 \end{itemize}
 \item for any CI of the form $\bigsqcap_i A_i \sqsubseteq \bigsqcup_j B_j$, remove all nominals from the right-hand side (i.e. if $B_j$ is a nominal, remove $B_j$ from the disjunction);
 \item add the axiomatization of concept names $D_{\exists r. A}$ and $D_{\exists r^*. A}$.
\end{itemize}

Iterate through all possible choices of a number ${n \leq \|{\cal{K}}\| \cdot |\mn{ind}({\cal{K}})|}$, and sequences of: unary types $\tau_i$ (containing concept names from ${\cal{K}}$ and the local auxiliary concept names), individuals $e_i$ and roles $r_i$ for $i = 1, \dots, n$.
\comment{($\|{\cal{K}}\|\cdot |\mn{ind}({\cal{K}})| \cdot 4^{|\mn{CN}({\cal{K}})|\cdot \|{\cal{K}}\| \cdot |\mn{ind}({\cal{K}})|} \cdot (|\mn{ind}({\cal{K}})| \cdot 2|\mn{rol}({\cal{K}})|)^{\|{\cal{K}}\| \cdot |\mn{ind}({\cal{K}})|}$ options)}
We will consider an interpretation obtained by taking a union of $\ensuremath{{\cal{I}}_0}$ and all ${\cal{I}}_i$ for $i = 1, \dots, n$, where ${\cal{I}}_i$ is any model of ${\cal{K}}_{\tau_i}$, and adding two kinds of additional edges: between $e_i$ and $d_i$ (the only individual of ${\cal{K}}_{\tau_i}$) by role $r_i$ and from all elements in concept $A_{r, a}$ to $a$ by role $r$.
Perform the rest of the procedure for a fixed choice of $n$ and all $\tau_i$, $e_i$ and $r_i$ for $i = 1, \dots, n$; there is a counter-model iff there is a counter-model consistent with one of such choices.

We will see that the following procedure verifying that the resulting interpretation is a model of ${\cal{K}}$ does not depend on the choices of models ${\cal{I}}_i$.
Regardless of the exact shape of ${\cal{I}}_i$, the local auxiliary concept names $D_{\exists r^*. A_{r^-, a}}$ present in $\tau_i$ determine the set of nominals $r$-reachable from $d_i$ through ${\cal{I}}_i$.

Knowing also ${\cal{I}}_0$, we can calculate for each individual the set of $r$-reachable nominals and verify that it corresponds to the auxiliary concept names $C_{\exists r^*. A_{a}}$ present in the unary type of this individual.
This reachability information is the crucial part that needs to be verified; the rest is a number of straightforward conditions. Namely, one needs to check that:
\begin{itemize}
 \item for each individual, each auxiliary concept name $C_{\exists r^*. A}$ present in its unary type is witnessed, either by an $r$-reachable element of ${\cal{I}}_0$ in concept $A$ or by the local auxiliary concept name $D_{\exists r^*. A}$ present in some $\tau_i$ for an $r$-reachable $d_i$;
 \item for each individual, verify that it belongs to each auxiliary concept of the form $C_{\exists r. A}$ and $\overline{C_{\exists r. A}}$ present in its unary type; each of its direct successors is either inside ${\cal{I}}_0$ or is some $d_i$ (with unary types $\tau_i$) for $1 \leq i \leq n$, so this can be done by simply checking direct successors one by one;

 \item CIs of the form $\bigsqcap_i A_i \sqsubseteq \bigsqcup_j B_j$ are satisfied in all elements of ${\cal{I}}_0$;
 \item no universal CIs are violated in ${\cal{I}}_0$ and by the edges between $e_i$ and $d_i$; in particular, for any element being subject to restriction $\forall {r^*}. A$ (i.e. in concept $\overline{C_{\exists {r^*}. \overline{A}}}$), all its direct $r$-successors must be subject to the same restriction (stickiness).

\end{itemize}

Every counter-model admitting the described decomposition can be constructed this way.
If the verification procedure fails, there is no counter-model consistent with the choices made.
If it succeeds, the only thing left to do is to check if there are models of ${\cal{K}}_{\tau_i}$ for which $Q$ does not have a match in the resulting interpretation ${\cal{I}}$.

\subsubsection{Adjusting the query.}
We want to reduce reasoning about matches of $Q$ in the whole interpretation ${\cal{I}}$ to reasoning about matches of some query in the interpretations ${\cal{I}}_i$.
To achieve this, for each $q \in Q$ we will construct a $\ensuremath{\UCQ^\smallplus}\xspace$ $Q'$ mentioning $d_i$ for $i = 1, \dots, n$ as individuals such that, for any interpretation ${\cal{I}}$ admitting the described decomposition, ${\cal{I}} \models q$ iff there is some $q' \in Q'$ such that each connected component of $q'$ has a match in some ${\cal{I}}_i$ for some $i = 1, \dots, n$.
Each disjunct $q' \in Q'$ will correspond to some way in which a match of $q$ can be distributed among interpretations ${\cal{I}}_i$ for $i = 0, 1, \dots, n$.

Existence of an $r$-path between any two individuals $a, b$ can be deduced from $\ensuremath{{\cal{I}}_0}$ alone: any $r$-path from $a$ to $b$ is either contained entirely in $\ensuremath{{\cal{I}}_0}$ (which can be easily verified), or it passes through at least one nominal, so its existence can be checked by comparing the sets of nominals $r$-reachable from $a$ and $r^-$-reachable from $b$ (these sets in turn can be deduced from the unary types of $a$ and $b$).

\begin{definition}
Let $\Imc$ be an interpretation and $q \in \ensuremath{\CQ^\smallplus}\xspace$.
An \emph{enhanced match} for $q$ in $\Imc$ is a match $\eta:\textit{var}(q)\to\Delta^\Imc$ along with \emph{witnessing paths}: for each transitive atom $r^*(x, y)$ in $q$ there is one chosen $r$-path in $\Imc$ from $\eta(x)$ to $\eta(y)$.
\end{definition}

The crucial observation is that any path witnessing a transitive atom $r^*(x, y)$ is either contained entirely in one of the interpretations ${\cal{I}}_i$ for $0 \leq i \leq n$, or can be split into three parts: $r^*(x, a) \land r^*(a, b) \land r^*(b, y)$, where $a$ and $b$ are individuals and the paths witnessing the first and the third atom do not pass through individuals (i.e. each of them is contained inside one interpretation ${\cal{I}}_i$ for $1 \leq i \leq n$).
Thus, a $\ensuremath{\UCQ^\smallplus}\xspace$ $Q'$ capturing all possible distributions of an enhanced match of some $q \in Q$ is a disjunction of all possible results of the following procedure:
\begin{itemize}
 \item for each transitive atom $r^*(x, y)$ in $q$, either leave it unmodified or choose two individuals $a, b \in \mn{ind}({\cal{K}})$ and replace it with $r^*(x, a) \land r^*(a, b) \land r^*(b, y)$;
 \item choose a subset of variables, a mapping from this subset to $\mn{ind}({\cal{K}})$ and replace the chosen variables with individuals in the whole query (we assume that no other variable will be mapped to an individual);
 \item evaluate all atoms involving only individuals (this can be done, as ${\cal{I}}_0$ is already fixed, and the reachability between the individuals is known);
 \item replace atoms involving one individual from $\mn{ind}({\cal{K}})$ with equivalent ones mentioning either some $d_i$ or no individual at all; this requires considering several simple cases, which we will omit here, such as: for each atom $r(x, a)$ where $a$ is an individual, choose to replace it either with $A_{r, a}(x)$ (only if $a$ is a nominal) or with $x = d_i$ for some $i$ such that $e_i = a$.
\end{itemize}

Thus, if $m$ is the number of transitive atoms in $q$, we can replace $q$ with a disjunction of $\ensuremath{\CQ^\smallplus}\xspace$s $q_1, \dots, q_k$ for $k \leq (|\mn{ind}({\cal{K}})|^2+1)^m \cdot (|\mn{ind}({\cal{K}})|+n+1)^{|\textit{var}(q)|}$, and assume that each connected component of each $q_j$ is contained entirely inside one interpretation ${\cal{I}}_i$ for $1 \leq i \leq n$.

Let $Q'$ be the $\ensuremath{\UCQ^\smallplus}\xspace$ being a disjunction of all resulting $\ensuremath{\CQ^\smallplus}\xspace$s for all $q \in Q$.

Now we just need a standard reduction of finite entailment to the case where one assumes that each $\ensuremath{\CQ^\smallplus}\xspace$ is connected.
In any counter-model, for each of $q \in Q'$, for at least one connected component of $q$ there must be no match (contained entirely in ${\cal{I}}_i$ for some $1 \leq i \leq n$).
For each possible choices of one connected component from each $q \in Q'$, check the entailment of their disjunction in each ${\cal{K}}_{\tau_i}$ for $1 \leq i \leq n$.
There is a counter-model for $Q$ and ${\cal{K}}$ iff for some choice of the connected components there are counter-models for the resulting $\ensuremath{\UCQ^\smallplus}\xspace$ and each ${\cal{K}}_{\tau_i}$ for $1 \leq i \leq n$; there are at most $(2m)^{k\cdot |Q|}$ such choices, where $k$ is the bound on the number of $\ensuremath{\CQ^\smallplus}\xspace$s $q_1, \dots, q_k$ above.

\subsection{$\ensuremath{\ALCOQ^\smallplus}\xspace$ without at-most restrictions over transitive closures}
We present only the modifications needed to be done in the proof for $\ensuremath{\ALCOI^\smallplus}\xspace$.

Let ${\cal{K}} = ({\cal{T}}, {\cal{A}})$ be an $\ensuremath{\ALCOQ^\smallplus}\xspace$ knowledge base without at-most restrictions over transitive closures of roles, with counting threshold $N$, and $Q \in \ensuremath{\UCQ^\smallplus}\xspace$ with $\ensuremath{\CQ^\smallplus}\xspace$s of size at most $m$.

One can decide if ${\cal{K}} \models_{\mathsf{fin}} Q$ in time
$\mathrm{poly}(\|{\cal{K}}\|, (2m)^{|Q|\cdot (N \cdot \|{\cal{K}}\|)^{O(m)}})$
using oracle calls to finite entailment modulo types over $\ensuremath{\ALCQ^\smallplus}\xspace$ KBs of size at most
$\mathrm{poly}(N, \|{\cal{K}}\|)$,
with trivial ABoxes and unions of at most
$|Q| \cdot (N \cdot \|{\cal{K}}\|)^{O(m)}$
$\ensuremath{\CQ^\smallplus}\xspace$s of size
$O(m)$.

\subsubsection{Auxiliary concepts.}
Introduce new auxiliary concept names $C_{\qnrleq k r A}$, $C_{\qnrgeq k r A}$ and $C_{\qnrgeq k {r^*} A}$ for each $k < N$, role name $r$ and original concept name $A$; they are supposed to denote that, if an element $x$ is in such a concept, it belongs to the concept in the subscript (in the whole interpretation ${\cal{I}}$).
That is, their axiomatization is simply $C_{\qnrleq k r A} \sqsubseteq {\qnrleq k r A}$, $C_{\qnrgeq k r A} \sqsubseteq {\qnrgeq k r A}$, $C_{\qnrgeq k {r^*} A} \sqsubseteq {\qnrgeq k {r^*} A}$.

\subsubsection{Unravelling.}
The unravelling procedure lifts easily to the case with counting, without inverses.
Assume that the auxiliary concept names have the intended meaning in the original counter-model; for example, an element is in concept $C_{\qnrgeq k {r^*} A}$ iff it has at least $k$ $r$-successors in concept $A$.
The definition of a witnessing set for $x$ is modified to be $S$ such that:
\begin{itemize}
 \item for every $(y, r) \in S$, $y$ is a direct $r$-successor of $x$;
 \item for each CI of the form $A \sqsubseteq \qnrgeq k r B$ such that $A \in \mn{tp}^{{\cal{I}}}(x)$, there exist at least $k$ distinct $(y, r) \in S$ such that $y$ is in concept $B$;
 \item for each CI of the form $A \sqsubseteq \qnrgeq k {r^*} B$ such that $A \in \mn{tp}^{{\cal{I}}}(x)$:
 \begin{itemize}
  \item if $B \in \mn{tp}^{{\cal{I}}}(x)$, at least $k-1$ distinct $r$-successors of $x$ in concept $B$ are $r$-reachable from the elements $\{y: (y, r) \in S\}$,
  \item if $B \not\in \mn{tp}^{{\cal{I}}}(x)$, at least $k$ distinct $r$-successors of $x$ in concept $B$ are $r$-reachable from the elements ${\{y: (y, r) \in S\}}$.
 \end{itemize}
\end{itemize}
\comment{(any minimal witnessing set has size at most $N \cdot \|{\cal{K}}\|$)}

Let ${\cal{J}}$ be any counter-model.
A counter-model ${\cal{I}}$ admitting the desired decomposition is constructed as follows.
Take a copy of ${\cal{J}} \upharpoonright \mn{ind}({\cal{K}})$.
For every individual $x \in \mn{ind}({\cal{K}})$, take any minimal witnessing set $S$ for $x$ in ${\cal{J}}$.
For each $(y, r) \in S$, add a fresh copy of the whole interpretation ${\cal{J}}$ to ${\cal{I}}$, identifying the nominals and \emph{removing all outgoing edges from the nominals} and add an $r$-edge from $x$ to the newly created copy of $y$.
As each element and each edge in ${\cal{I}}$ was created as a copy of some element or edge in ${\cal{J}}$, there is a homomorphism from ${\cal{I}}$ to ${\cal{J}}$ witnessing that ${\cal{I}} \not\models Q$.

To argue that ${\cal{I}} \models {\cal{K}}$, we will show that the satisfaction of all the required restrictions is preserved.
Recall that there are no inverses and no at-most restrictions over transitive closures.
For any element $x$ in ${\cal{I}}$ created as a copy of some $x'$ in ${\cal{J}}$, and for any role name $r$, all direct $r$-successors of $x$ were created as copies of distinct direct $r$-successors of $x'$, which preserves all at-most restrictions.
All required restrictions of the form $\qnrgeq k r A$ are clearly satisfied in ${\cal{I}}$, as the copies of appropriate elements and edges are added explicitly during the procedure.
As for restrictions of the form $\qnrgeq k {r^*} A$, consider an individual that has $m$ $r$-reachable elements in concept $A$ in ${\cal{J}}$:
\begin{itemize}
 \item if $m < N$, at least one copy of each of them is $r$-reachable in ${\cal{I}}$ from this individual (recall the assumption that the concepts $C_{\qnrgeq k {r^*} A}$ have the intended meaning in ${\cal{J}}$ and the definition of the witnessing set);
 \item if $m \geq N$, then copies of at least $N-1$ of them are reachable (by the argument above), which is enough to satisfy any counting restriction.
\end{itemize}
Therefore, for any element $x$ in ${\cal{I}}$ created as a copy of $x'$ from ${\cal{J}}$, any role name $r$ and any concept name $A$, it can be easily seen that either:
\begin{itemize}
 \item there is a nominal in concept $C_{\qnrgeq {N-1} {r^*} A}$ $r$-reachable from $x$;
 \item at least one copy of every element in concept $A$ $r$-reachable from $x'$ (in ${\cal{J}}$) is $r$-reachable from $x$ (in ${\cal{I}}$).
\end{itemize}
This is enough for all required restrictions to be satisfied in ${\cal{I}}$.

Note that, as there are no inverse roles, the edges between $e_i$ and $d_i$ are always directed towards $d_i$.

\subsubsection{Local auxiliary concepts.}
For $\ensuremath{\ALCOI^\smallplus}\xspace$, when describing KBs ${\cal{K}}_{\tau_i}$, we defined local auxiliary concepts $D_{\exists r. A}$ and $D_{\exists r^*. A}$.
Here we will define analogous concepts $D_{\qnrleq k r A}$, $D_{\qnrgeq k r A}$ and $D_{\qnrgeq k {r^*} A}$, although this time we additionally need to be prepared to distinguish elements $r_i$-reachable from $d_i$ to avoid counting them twice later in the process.

For each role name $r$ we introduce a concept name $R_r$; if an element $x$ in ${\cal{I}}_i$ is $r$-reachable from $d_i$, it is supposed to be in this concept.
The axiomatization is simple: $R_r(d_i)$ is present in the ABox, and $R_r \sqsubseteq \forall r. R_r$ is present in the TBox.
Then, for each original concept name $A$, introduce a concept name $C_{A\sqcap \overline{R_r}} \equiv A \sqcap \overline{R_r}$.

Introduce local auxiliary concept names $D_{\qnrleq k r A}$, $D_{\qnrgeq k r A}$ and $D_{\qnrgeq k {r^*} A}$ for each $k < N$, role name $r$ and $A$ being either an original concept name or $C_{B\sqcap \overline{R_r}}$ for an original concept name $B$; if an element $x \in \Delta^{{\cal{I}}_i}$ is in such concept, it belongs to the concept in the subscript in ${\cal{I}}_i$.

When constructing KBs ${\cal{K}}_\tau$, rewrite CIs to use the auxiliary concept names; that is, replace:
\begin{itemize}
 \item $A \sqsubseteq \qnrleq k r A$ with $A \sqsubseteq C_{\qnrleq k r A}$;
 \item $A \sqsubseteq \qnrgeq k r A$ with $A \sqsubseteq C_{\qnrgeq k r A}$;
 \item $A \sqsubseteq \qnrgeq k {r^*} A$ with $A \sqsubseteq C_{\qnrgeq k {r^*} A}$.
\end{itemize}
Also, remove the axiomatization of the auxiliary concepts altogether.

\subsubsection{Verifying being a model of ${\cal{K}}$.}
For each choice of ${\cal{I}}_0$, $n$, $e_i$, $r_i$, $\tau_i$ for $i = 1, \dots, n$, we need to verify whether there exists a counter-model admitting a decomposition consistent with their values.
For $\ensuremath{\ALCOI^\smallplus}\xspace$, to perform this verification, we solved multiple instances of finite entailment problem for ${\cal{K}}_{\tau_i}$ for each $i = 1, \dots, n$ and the modified query $Q'$.
Now we will need to solve instances of finite entailment modulo types; we will define sets $\Theta_i$ (which will depend on ${\cal{I}}_0$, $n$, $e_i$, $r_i$ and $\tau_i$) of unary types allowed for ${\cal{K}}_{\tau_i}$ to make sure that whenever an element of a model ${\cal{I}}_i$ of ${\cal{K}}_{\tau_i}$ is in concept $C_{\qnrgeq k {r^*} A}$, it is also in concept $\qnrgeq k {R^*} A$ in the whole interpretation ${\cal{I}}$.

For a given element $x$ of some ${\cal{I}}_i$, we will be talking about \emph{local successors}: successors reachable from $x$ without leaving the model ${\cal{I}}_i$ (without passing through any nominal) and \emph{global successors}: ones that are reachable by paths passing through some nominal.
Note that the sets of local successors and global successors are not necessarily disjoint.

For a nominal $a$, define $\mathsf{globsuc}_{a,r,A}$ to be the set of $r$-successors of $a$ in concept $A$.
Note that, even though this exact set depends on choices of models ${\cal{I}}_i$, the local auxiliary concepts $D_{\qnrgeq k {r^*} A}$ present in $\tau_i$ for $i = 1, \dots, n$ along with ${\cal{I}}_0$ give a lower bound on its cardinality.
Moreover, assuming that they have the intended meaning in the interpretations ${\cal{I}}_i$, one can deduce from them (and from ${\cal{I}}_0$) the exact cardinality of $\mathsf{globsuc}_{a,r,A}$ up to $N$.
For a set of nominals $S$, let $\mathsf{globsuc}_{S,r,A} = \bigcup_{a \in S} \mathsf{globsuc}_{a,r,A}$.

For each $i = 1, \dots, n$ define the set $\Theta_i$ of allowed unary types $\tau$ such that, for every $k < N$, role name $r$ and original concept name $A$:
\begin{itemize}
 \item if $C_{\qnrgeq k r A} \in \tau$, then $\max\{\ell: D_{\qnrgeq \ell r A} \in \tau\} + |\{a \in \mn{nom}({\cal{K}}): A_{r,a} \in \tau \land A(a) \in {\cal{A}}\}| \geq k$;
 \item if $C_{\qnrleq k r A} \in \tau$, then $\min\{\ell: D_{\qnrleq \ell r A} \in \tau\} + |\{a \in \mn{nom}({\cal{K}}): A_{r,a} \in \tau \land A(a) \in {\cal{A}}\}| \leq k$;
 \item if $C_{\qnrgeq k {r^*} A} \in \tau$, then:
 \begin{itemize}
  \item if $d_i$ is not $r$-reachable from an element of type $\tau$ through any nominal (this depends only on ${\cal{I}}_0$, $r_i$ and the set of nominals $r$-reachable from an element of type $\tau$), then the sets of local and global $r$-successors in concept $A$ are disjoint, so the condition is:
  $\max\{\ell: D_{\qnrgeq \ell {r^*} A} \in \tau\} + |\mathsf{globsuc}_S| \geq k$, where $S = \{a \in \mn{nom}({\cal{K}}): C_{\qnrgeq 1 {r^*} {A_a}} \in \tau\}$;
  \item if $d_i$ is $r$-reachable from an element of type $\tau$ through any nominal, then these sets are intersecting, but we can avoid double counting thanks to the concept names $C_{A \sqcap \overline{R_r}}$ introduced in ${\cal{K}}_{\tau_i}$:
  $\max\{\ell: D_{\qnrgeq \ell {r^*} {C_{A \sqcap \overline{R_r}}}} \in \tau\} + |\mathsf{globsuc}_S| \geq k$, where $S = \{a \in \mn{nom}({\cal{K}}): C_{\qnrgeq 1 {r^*} {A_{r,a}}} \in \tau\}$.
 \end{itemize}
\end{itemize}
We cannot calculate the exact cardinality of $|\mathsf{globsuc}_S|$ used above, but we can use the described lower bound instead.
If the local auxiliary concept names have the intended interpretations in all ${\cal{I}}_i$, the conditions will be correctly verified.
If not, they will be lower bounds, so $\Theta_i$ might contain less unary types, which only reduces the space of considered models and does not affect the resulting model of ${\cal{K}}$; notice that the local auxiliary concept names are introduced by the procedure and are not present in the original KB ${\cal{K}}$.

As in the $\ensuremath{\ALCOI^\smallplus}\xspace$ case, calculate for each individual the set of $r$-reachable nominals for each role name $r$.
For each element of ${\cal{I}}_0$, all its direct successors are either inside ${\cal{I}}_0$ or are $d_i$ (with unary types $\tau_i$), so verifying whether an element of ${\cal{I}}_0$ is in a concept of the form $\qnrleq k r A$ or $\qnrgeq k r A$ can be done by simply counting the appropriate successors.
Concepts of the form $\qnrgeq k {r^*} A$ can be easily verified using the information about the nominals reachable from individuals and the local auxiliary concept names.

\subsubsection{Adjusting the query.}
The only change with respect to the $\ensuremath{\ALCOI^\smallplus}\xspace$ case regarding the query is the method of calculating whether a path between two individuals exist.
Before we used the sets of nominals $r$-reachable and $r^-$-reachable from the individuals; now we need to use the fact that there are no inverses and the edges between $e_i$ and $d_i$ are always directed towards $d_i$.
Therefore, any (forward) path between individuals is either contained entirely in ${\cal{I}}_0$, or it passes through some nominal and can be decomposed into two parts: the beginning up to the last nominal on the path and the rest (possibly empty), contained entirely in ${\cal{I}}_0$.
Existence of such parts is easy to verify; the first part relies on the set of nominals $r$-reachable from an individual, which can be deduced from the auxiliary concept names of the form $C_{\qnrgeq 1 {r^*} A_a}$.

\subsection{$\ensuremath{\ALCOQ^\smallplus}\xspace$}
Let ${\cal{K}} = ({\cal{T}}, {\cal{A}})$ be an $\ensuremath{\ALCOQ^\smallplus}\xspace$ knowledge base with counting threshold $N$, and $Q \in \ensuremath{\UCQ^\smallplus}\xspace$ with $\ensuremath{\CQ^\smallplus}\xspace$s of size at most $m$.

One can decide if ${\cal{K}} \models_{\mathsf{fin}} Q$ in time
$\mathrm{poly}(\|{\cal{K}}\|, (2m)^{|Q|\cdot (\|{\cal{K}}\| \cdot N^{|\mn{RCN}({\cal{K}})|})^{O(m)}})$
using oracle calls to finite entailment modulo types over $\ensuremath{\ALCQ^\smallplus}\xspace$ KBs of size at most
$\mathrm{poly}(\|{\cal{K}}\|, N^{1+|\mn{RCN}({\cal{K}})|})$,
with trivial ABoxes and unions of at most
$|Q| \cdot (\|{\cal{K}}\| \cdot N^{|\mn{RCN}({\cal{K}})|})^{O(m)}$
$\ensuremath{\CQ^\smallplus}\xspace$s of size
$O(m)$.

Without loss of generality, assume that ${\cal{K}}$ is sticky.

In this case, $\ensuremath{{\cal{I}}_0}$ becomes ${\cal{I}}$ restricted not just to the individuals, but to individuals and all their relevant successors.
For this reason, at the very beginning of the reduction, we do the following.
Iterate through all possible sizes of the set of relevant successors of all individuals (by Fact~\ref{fact:relevant}, it is of size at most $|\mn{ind}({\cal{K}})|\cdot |\mn{rol}({\cal{K}})|\cdot N^{|\mn{RCN}({\cal{K}})|}$).
As usual, there is a counter-model iff there is one consistent with one of these choices.
For a fixed choice $t$ of this number, add $t$ fresh individuals to the ABox.
For each role name $r$ and each pair of individuals $(a, b)$, choose whether there exists an $r$-path from $a$ to $b$; if so, add a CI $\{a\} \sqsubseteq \exists r^*. \{b\}$ to the TBox.
Note that this might introduce new nominals, which are treated as such throughout the whole procedure; in particular, appropriate concept names of the form $A_{r, a}$ are introduced.

The construction extends the one from the case without at-most restrictions over transitive closures; below we describe only the newly introduced concepts and verification steps.

\subsubsection{Auxiliary concepts.}
Add auxiliary concept names $C_{\qnrleq k {r^*} A}$ for all $k < N$, role names $r$ and relevant concept names $A$.
Additionally, for each role name $r$ and relevant concept name $A$, choose a subset $\mathsf{full}_{r, A} \subseteq \Delta^{\ensuremath{{\cal{I}}_0}}$; it is supposed to denote the set of elements having at least $N$ $r$-successors in concept $A$ (one could express it using the concept $C_{\qnrgeq N {r^*} A}$, but we want to avoid increasing the counting threshold in the produced KBs).

\subsubsection{Unravelling.}
Unravelling works the same as in the case of $\ensuremath{\ALCOQ^\smallplus}\xspace$ without at-most restrictions over transitive closures.
Correctness follows easily from the fact that all relevant successors of individuals are inside ${\cal{I}}_0$ and that the at-most restrictions are sticky, therefore no additional interaction between the interpretations ${\cal{I}}_i$ is introduced.

\subsubsection{Local auxiliary concepts.}
Introduce concept names $D_{\qnrleq k {r^*} A}$ for $k < N$, any role name $r$ and any relevant concept name $A$.

\subsubsection{Verifying being a model of ${\cal{K}}$.}
By the assumption that $\ensuremath{{\cal{I}}_0}$ is closed under taking relevant successors, if any element of $\ensuremath{{\cal{I}}_0}$ is in the interpretation of a concept name $C_{\qnrleq k {r^*} A}$ for $k > 0$, all appropriate witnesses (i.e. its $r$-successors in concept $A$) need to also be in $\ensuremath{{\cal{I}}_0}$.
For any fixed role name $r$ and relevant concept name $A$, we verify that if an element of $\ensuremath{{\cal{I}}_0}$ is not in such concept for any $k$, then it is in the set $\mathsf{full}_{r, A}$.

For all $r$-edges from $e_i$ to $d_i$, if $e_i$ has an at-most restriction over transitive closure of $r$, $d_i$ needs to have the same restriction with number $0$.

 We will again construct the sets $\Theta_i$ of unary types allowed in models of ${\cal{K}}_{\tau_i}$: the allowed types $\tau$ need to satisfy all the conditions listed in the case without at-most restrictions over transitive closures. Additionally, if $C_{\qnrleq k {r^*} A} \in \tau$, then: if any nominal \emph{without} the same type of restriction ($C_{\qnrleq \ell {r^*} A}$ for any $\ell$) is $r$-reachable, the restriction is violated (this nominal is in $\mathsf{full}_{r, A}$ and has at least $N$ $r$-successors in concept $A$), so then $\tau$ is forbidden; otherwise, all reachable nominals have the same type of restriction, so all relevant successors reachable through nominals are also nominals and can be counted explicitly.
The upper bound on the number of local witnesses is $\min\{k: D_{\qnrleq k {r^*} A} \in \tau\}$, and, if the local auxiliary concept names have the intended meaning, these numbers are equal.

\section{Eliminating transitive atoms}

\subsection{Proof of Lemma~\ref{lem:unravelling}}

Let us check that the decomposition is well formed for ${\cal{K}}$. We start
the unravelling from the individual mentioned in the ABox, so
${\cal{I}}_\varepsilon \models {\cal{A}}$. Item \ref{item:types} of
Definition~\ref{def:well-formed} is satisfied because elements in each
bag inherit their unary types from their originals in ${\cal{J}}$.  For item
\ref{item:roots}, note that each neighbour of $\mn{cmp}_{\cal{J}}(d)$ outside of
$\mn{rel}_{\cal{J}}(d) \cup \mn{cmp}_{\cal{J}}(d)$ can have either only outgoing edges to
$\mn{cmp}_{\cal{J}}(d)$ or only incoming edges from $\mn{cmp}_{\cal{J}}(d)$: if it had
both, it would belong to $\mn{cmp}_{\cal{J}}(d)$.  Items \ref{item:external}
follow directly from the construction.  For item
\ref{item:rel-consistent}, note that $\Gamma_u$ and $\Gamma_w$ are
copies of $\mn{rel}_{\cal{J}}(e_u)$ and $\mn{rel}_{\cal{J}}(e_w)$ for the originals $e_u$
and $e_w$ of $f_u$ and $f_w$, which implies that $e_u \in
\mn{rel}_{\cal{J}}(e_w)$, and this gives $\mn{rel}_{\cal{J}}(e_u) \subseteq \mn{rel}_{\cal{J}}(e_w)$
by the definition of relevant successors. It follows by construction
that $\Gamma_u \subseteq \Gamma_w$.  It remains to prove item
\ref{item:rel-contained}. By construction, local elements in bag $u$
are exactly those in the copy of $\mn{cmp}_{\cal{J}}(e_u)$. By stickyness, all
local elements have the same relevant concept names. Hence, the
concept name $A$ mentioned in item \ref{item:rel-contained} is
relevant for $f_u$. Because $d$ mentioned in item
\ref{item:rel-contained} is local, it is reachable from
$f_u$. Hence, if $d\in A^{{\cal{I}}_u}$, then $d$ is a relevant successor
of $f_u$, which means it belongs to $\Gamma_u$. (The only case when
this can happen is when $d=f_u$, but this is irrelevant here.)
Consider $v\in T$ such that $f_v$ is a sink in ${\cal{I}}_u$ or
$f_u$ is a non-isolated source in ${\cal{I}}_v$. In either case,
the original $e_v$ of $f_v$ is reachable from the original $e_u$ of
$f_u$ in ${\cal{J}}$. Consider an element $e' \in \Gamma_v$. Then, the original $e$
of $e'$ is a (relevant) successor of the original $e_v$ of $f_v$,
which implies that it is also reachable from the original $e_u$ of
$f_u$. If $e' \in A^{{\cal{I}}_v}$, then $e \in A^{{\cal{J}}}$ and $e \in
\mn{rel}_{\cal{J}}(e_u)$. From the construction of the unravelling it follows
that $e' \in \Gamma_u$, and we are done.
If ${\cal{K}}$ does not use inverse roles, we add only direct successors of
$f_v$, rather than all neighbours, so items \ref{item:roots} and
\ref{item:external} hold with ``sink or source'' replaced with
``sink''.  Because we remove all edges outgoing from
$\Gamma_u\setminus \{f_u\}$, these elements are indeed sinks.
If ${\cal{K}}$ does not use counting restrictions, $\mn{rel}_{\cal{J}}(e) = \emptyset$
for each $e \in \Delta^{{\cal{J}}}$, so $\Gamma_u = \emptyset$ for each
$u\in T$.

To see that the decomposition is well connected, observe that each
${\cal{I}}_u$ consists of a strongly connected component, a set of elements
attached to it, and possibly a set of isolated elements. This is
precisely how a well-connected interpretation looks.

Safety is proved by contradiction. Consider an infinite path of nodes
$u_0, u_1, \dots, $ such that for all $i$, either $f_{u_{i+1}}$ is a
sink in ${\cal{I}}_{u_{i}}$ or $f_{u_i} $ is a non-isolated source in
${\cal{I}}_{u_{i+1}}$. By construction, in this case, the original
$e_{u_{i+1}}$ of $f_{u_{i+1}}$ is a successor of the original
$e_{u_{i}}$ of $f_{u_{i}}$ in ${\cal{J}}$ for all $i$.  Once a simple
directed path in ${\cal{J}}$ leaves some strongly connected
component (SCC) of ${\cal{J}}$ it never goes back. Because the number of
SCCs in ${\cal{J}}$ is finite, there exists $i_0$ such that for $i\geq i_0$,
all $e_{u_{i}}$ belong to the same strongly connected component $Z$ in
${\cal{J}}$. By stickiness, the sets $\mn{rel}_{\cal{J}}(e_{u_{i}})$ coincide for all
$i\geq i_0$; let $\mn{rel}_{{\cal{J}}}(Z)$ be their common value. From the
construction of $T$ it follows that $\Gamma_{u_i}$ also coincide for
$i\geq i_0$. Because all $f_{u_{i}}$ are different, there exists
$i_1 \geq i_0$ such that $f_{u_{i}} \notin \Gamma_{u_i}$ for all
$i\geq i_1$. This implies that $e_{u_i} \notin \mn{rel}_{{\cal{J}}}(Z)$ for
$i\geq i_1$. By the construction of the unravellng, $e_{u_{i+1}}$ is
reachable from $e_{u_i}$ without passing through $\mn{rel}_{{\cal{J}}}(Z)$, and
$e_{u_{i+1}} \notin \mn{cmp}_{\cal{J}}(e_{u_i})$. It follows that $e_{u_{j}}
\notin \mn{cmp}_{\cal{J}}(e_{u_i})$ for $j>i \geq i_1$, because  $e_{u_{j}} \in
\mn{cmp}_{\cal{J}}(e_{u_i})$ implies that  $e_{u_{j'}} \in \mn{cmp}_{\cal{J}}(e_{u_i})$
for all $ j \geq j' \geq i$, which is in contradiction with
$e_{u_{i+1}} \notin \mn{cmp}_{\cal{J}}(e_{u_i})$. But $e_{u_{j}} \notin
\mn{cmp}_{\cal{J}}(e_{u_i})$ implies $e_{u_{j}} \neq e_{u_i}$ for $j>i \geq
i_1$, which is impossible because ${\cal{J}}$ is finite.

Checking that ${\cal{I}}\models {\cal{K}}$ is entirely routine.

\subsection{Proof of Lemma~\ref{lem:correct}}

By the compostionality of $Q$-types, that the correct $Q$-labelling
$\sigma$ satisfies the condition
\[  \sigma(d) = \bigg(\mn{tp}^{{\cal{I}}_u}_Q\big(\{d\} \cup \Gamma_u \cup
\widetilde\Gamma_u\big) \oplus \bigoplus_{e\in \widetilde\Gamma_u}
\sigma(e)\bigg) \upharpoonright \{d\}\cup\Gamma_u
\]
for each node $u \in T$ and each element $d$ local in $u$.

It remains to show that for each $Q$-labelling $\sigma'$ satisfying
the condition above we have $\sigma(d) \subseteq \sigma'(d)$. Let us
fix such $\sigma'$. We first show an auxiliary fact.

\begin{fact} \label{fact:aux}
  For each descendent $v$ of $u$ and each $d$ local in $u$,
  $\sigma'(f_v) \upharpoonright \{d\} \cup \Gamma_u \subseteq
  \sigma'(d)$.
\end{fact}
\begin{proof}
This is proved by induction on the distance between $u$ and $v$. If
$v$ is a child of $u$ the claim follows directly from the initial
assumption on $\sigma'$.  Otherwise, let $w$ be the unique child of
$u$ that is an acestor of $v$. By the inductive hypothesis,
\[\sigma'(f_v) \upharpoonright \{f_w\} \cup \Gamma_w \subseteq
\sigma'(f_w)\,.\] Like in the base case, we get
\[ \big (\sigma'(f_v) \upharpoonright \{f_w\} \cup \Gamma_w \big)
\upharpoonright \{d\} \cup \Gamma_u \subseteq \sigma'(d)\,. \] The
left-hand side is equal to $ \sigma'(f_v)
\upharpoonright \{d\} \cup \Gamma_u$, beacause \[\Delta_v \cap \big(\{d\} \cup
\Gamma_u\big)\subseteq \Delta_v \cap \Delta_u \subseteq \{f_w\} \cup
\Gamma_w\] holds in each hybrid decomposition.
\end{proof}

We need to show that for each node $u$, element $d \in \Delta_u$ local
in $u$, and $(p, \eta)$ with $ \emptyset \neq \mathsf{img}(\eta) \subseteq
\{d\} \cup \Gamma_u$, if there exists a match for $p$ in
$\widehat{\cal{I}}_u$ that extends $\eta$, then $(p, \eta) \in
\sigma'(d)$. We prove it by induction on the size of a minimal
connected set $V$ of nodes from the subtree rooted at $u$ such that
there exists a match for $p$ in $\bigcup _{v\in V} {\cal{I}}_v$, extending
$\eta$.

The base case is when $V = \{v\}$. If $v=u$, then \[(p, \eta) \in
\mn{tp}^{{\cal{I}}_u}_Q\big(\{d\} \cup \Gamma_u) \subseteq
\sigma'(d)\,.\] If $v \neq u$, using Fact~\ref{fact:aux},
\begin{align*}
(p, \eta) \in \mn{tp}^{{\cal{I}}_v}_Q\big(\{f_v\} \cup \Gamma_v)
\upharpoonright \{d\} \cup \Gamma_u \subseteq &\\
 \subseteq \sigma'(f_v) \upharpoonright \{d\} \cup \Gamma_u
  \subseteq \; & \sigma'(d)\,.
\end{align*}

If $|V| > 1$, let $v$ be the minimal node in $V$. Let us choose a
local element $e$ in $v$ as follows: if $d \in {\cal{I}}_v$ take $e=d$,
otherwise take $e=f_v$. We will prove that $(p, \eta) \in
\sigma'(e)$. This will yield $(p, \eta) \in \sigma'(d)$ either
directly, or by way of Fact~\ref{fact:aux}. Let $v_1, v_2, \dots, v_k$
be the children of $v$ that belong to $V$. Our goal now is to split
$(p, \eta)$ into $\tau, \tau_1, \dots, \tau_k$ such that
\begin{itemize}
\item
  $\textit{var}(p')\setminus \dom(\eta')$ are pairwise disjoint for $(p',
  \eta') \in \tau\cup\tau_1\cup\dots \cup \tau_k$;
\item
  $\mathsf{img}(\eta') \subseteq \{e\}\cup\Gamma_v\cup\widetilde\Gamma_v$ for $(p',
  \eta') \in \tau\cup\tau_1\cup\dots \cup \tau_k$;
\item
  for each $(p',\eta') \in \tau$, an extension of $\eta'$ matches $p'$
  in ${\cal{I}}_v$;
\item
  for each $i$ and each $(p',\eta') \in \tau_i$, an extension of $\eta'$
  matches $p'$ in $\widehat{\cal{I}}_{v_i}$;
\item
  there is a homomorphism $\tilde \eta$, extending $\eta$, from $p$
  into \[\bigcup_{(p',\eta') \in \tau\cup\tau_1\cup\dots \cup \tau_k} \eta'(p')\,;\]
\end{itemize}
and use the inductive hypothesis. An obstacle is that a path
witnessing a transitive atom $r^*(x,y)$ of $p$ for the match $\widehat
\eta$ may visit multiple bags among $v, v_1, \dots, v_k$. Let us
subdivide each transitive atom $r^*(x,y)$ of $p$ into $r^*(x,z_1),
r^*(z_1,z_2), \dots, r^*(z_\ell,y)$ in a minimal way ensuring that in
the induced matching each atom is witnessed by a path within ${\cal{I}}_v$
or within a single $\widehat{\cal{I}}_{v_i}$, with endpoints in
$\{\widehat\eta(x), \widehat\eta(y), f_v\} \cup \Gamma_v \cup
\widetilde\Gamma_v$.  We can now obtain the desired $\tau, \tau_1,
\dots, \tau_k$ by partitioning the resulting query into maximal
fragments matched within ${\cal{I}}_v$ or some $\widehat{\cal{I}}_{v_i}$. For each
such fragment $p'$, the corresponding $\eta'$ is obtained by
restricting the matching to variables matched in $\{f_v\} \cup
\Gamma_v \cup \widetilde\Gamma_v$.

\subsection{Proof of Lemma~\ref{lem:regularity}}

We now know that ${\cal{K}}$ is an $\ensuremath{\ALCI^\smallplus}\xspace$ KB or an $\ensuremath{\ALCQ^\smallplus}\xspace$ KB, but in the
construction of the automaton we shall only assume that in  well-formed
decompositions for each bag $u$, all elements in $\Gamma_u \setminus
\{f_u\}$ are sinks. This is explicitly assumend for $\ensuremath{\ALCQ^\smallplus}\xspace$ KBs in
Definition~\ref{def:well-formed}, and it holds vacuously
for $\ensuremath{\ALCI^\smallplus}\xspace$ KBs, because $\Gamma_u = \emptyset$.

Let $N$ be the counting threshold in ${\cal{K}}$.  Without loss of
generality we can assume that there is an equivalent concept name for
each concept
\begin{align*}
  &\qnrleq n r A \,, &&\qnrgeq n r A \,, \\
  &\qnrleq n {r^*} B\,, &&\qnrgeq n {r^*} B \,,\\
  &\qnrleq 0 {r^-} A \,, &&\qnrgeq 1 {r^-} A \,, \\
  &\qnrleq 0 {(r^-)^*} A\,, &&\qnrgeq 1 {(r^-)^*} A
\end{align*}
where $n \leq N$, $A \in \mn{CN}({\cal{K}})$, and $B \in \mn{RCN}({\cal{K}})$.  If ${\cal{K}}$
does not have this property, we add these concepts and build an
automaton over a richer alphabet. The automaton for the original KB is
obtained by projecting to the smaller alphabet in a natural way.

We first describe the construction of the automaton and then discuss
the additional computability claims. The automaton ${\cal{B}}_{{\cal{K}}, Q,
\Theta}$ consists of three components. The first one verifies that the
input tree encodes a safe ${\cal{K}}$-decomposition of an interpretation
that only uses types from $\Theta$, the second deals with the concept
inclusions of ${\cal{K}}$, and the last checks that the decomposition admits
a $Q$-refutation. In what follows, $M=N^{|\mn{RCN}({\cal{K}})|}$ where $N$ is
the counting threshold in ${\cal{K}}$ and $[i,j] = \{i, i+1, \dots, j\}$.

\subsubsection*{Correctness of decomposition, safety, types}

The first thing to check is that the input tree is an encoding of a
hybrid decomposition. Correctness of the
encoding amounts to checking that $|\tup{g}_u|$ is equal to the length of
the tuple on the edge from $u$ to the parent; the latter is passed
down the tree and compared with $|\tup{g}_u|$. Conditions
\ref{item:hybrid-union}--\ref{item:hybrid-disjoint} of
Definition~\ref{def:hybrid} are ensured by the way the decomposition
is represented.

Ensuring that branching is at most $N^{\mn{CN}({\cal{K}})}$ is
done locally, based on the label of the current node and the edges
connecting it to its children, without relying on any kind of in
formation stored in the states.

Let us see how to verify that the hybrid decomposition is well-formed
for ${\cal{K}}$. Whether ${\cal{I}}_\varepsilon \models {\cal{A}}$ is tested locally
based on the label of the current node and recorded in the state; a
state is initial iff the result of this test is positive. Because
fresh nodes in ${\cal{I}}_u$ are exactly the ones that do not occur in
$f_u$ and $\tup{g}_u$, conditions \ref{item:roots} and
\ref{item:external} can also be checked locally. To check
condition \ref{item:types}, it suffices to pass the unary ${\cal{K}}$-type
of $f_u$ up the tree, and check that it coincides with the unary
${\cal{K}}$-type of the node specified in the label on the edge between $u$
and its parent. To check condition \ref{item:rel-consistent} it is
enough to maintain for each $e \in \Gamma_u$ the information about
which elements of $\Gamma_u$ belong to $\Gamma_v$ where $e=f_v$, and
make sure none of these elements is dropped unless $e$ is
dropped. This involves guessing in each node $w$ if $f_w$ belongs to
$\Gamma_{w'}$, where $w'$ is the parent of $w$: if so, $\tup{g}_w$ must
list all elements of $\Gamma_w$; the guess is passed up the tree to be
verified. It remains to check condition \ref{item:rel-contained}.

The first part of condition \ref{item:rel-contained} states that for
each local element $d$ in ${\cal{I}}_u$ and each concept name $A$ relevant
for $d$, if $d \in A^{{\cal{I}}_u}$ then $d\in\Gamma_u$. This can be be
verified locally by just looking at the label of the current node.
The second part of condition \ref{item:rel-contained} states that for
each local element $d$ in ${\cal{I}}_u$ and each concept name $A$ relevant
for $d$, $\Gamma_v \cap A^{{\cal{I}}_v} \subseteq \Gamma_u$ for all
$v\in T$ such that $f_v$ is a sink in ${\cal{I}}_u$ or $f_u$ is a
non-isolated source in ${\cal{I}}_v$. If $f_v \in \Gamma_{u}$, then by
condition \ref{item:rel-consistent}, the entire $\Gamma_v$ is
contained in $\Gamma_u$. And should $f_u$ belong to $\Gamma_v$, it
would be a sink, so not a non-isolated source in ${\cal{I}}_v$. Combining
these two observations we see that the automaton
only needs to verify the second part of condition
\ref{item:rel-contained} for $v$ such that  $f_v\notin\Gamma_u$ is a
sink in ${\cal{I}}_u$ or $f_u \notin \Gamma_v$ is a non-isolated source in
${\cal{I}}_v$, which implies that $v$ is a neighbour of $u$. Towards this
goal, the automaton passes from parent $w'$ to child $w$ the
information on whether $f_w$ is a sink or a non-isolated source in ${\cal{I}}_{w'}$, and
the information about all concept names relevant for some local
elements in ${\cal{I}}_{w'}$. The information about relevant concept names
is also passed up the tree: it is guessed in $w'$ and the guess is
passed down in the state to $w$, where it is verified. Based on this
information the automaton can ensure the second part of condition
\ref{item:rel-contained} as follows. If $f_v$ is a sink in the parent
of $v$, the automaton checks that for each concept name $A$ passed to
$v$ from the parent, all elements of $\Gamma_v \cap A^{{\cal{I}}_v}$ are
listed in $\tup{g}_v$.  Similarly, for each child $u$ of $v$ reachable via
an edge labelled with a non-isolated source in ${\cal{I}}_v$, and each concept name
passed from $u$ to $v$, all elements from $\Gamma_v \cap A^{{\cal{I}}_v}$
should be listed in the tuple on the edge between $v$ and $u$.

If ${\cal{K}}$ does not use inverse roles, the modified conditions
\ref{item:roots} and \ref{item:external} can be checked locally, too,
as can be the additional requirement that all elements of
$\Gamma_u\setminus \{f_u\}$ are sinks. The condition that $\Gamma_u
= \emptyset$, imposed when ${\cal{K}}$ does not use counting restrictions,
is also local.

To check safety it suffices to ensure that on each infinite branch, after
each node $v$ such that $f_v$ is a sink in the parent of $v$, there
is a node $w$ such that $f_w$ is a non-isolated source in the parent of $w$. The
automaton already has access, in node $v$, to the information on
whether $f_v$ is a sink or a non-isolated source in the parent $v'$ of
$v$. Additionally, we shall maintain the same information about the
parent $v'$ of $v$. With that, it suffices to declare as accepting
those states of the automaton, where $f_v$ is a sink and $f_{v'}$ is a
non-isolated source, or the other way around.

Verifying that only unary types from $\Theta$ are realized is also
done locally; when an element realizing a type not in $\Theta$ is
detected, the automaton rejects immediately.

Including additional information that will be useful later on, we let
the state $q$ at the node $v$ represent the following information:
\begin{enumerate}
\item \label{item:aut:rt}
  a type $\tau_q \in \mn{Tp}({\cal{K}})$, storing the unary ${\cal{K}}$-type of $f_v$;
\item \label{item:aut:Gamma}
  a tuple $(\tau^1_q, \dots, \tau^k_q) \in \mn{Tp}({\cal{K}})^k$ for some $k\leq
  M$, storing the unary ${\cal{K}}$-types of elements of $\Gamma_v$
  (according to some arbitrary fixed order on $\Delta$);
\item\label{item:aut:rt-in-Gamma}
  a value $i_q \in [0, k]$, where $i_q \in [1, k]$
  indicates that $f_v$ is the $i_q$th element in $\Gamma_v$ and
  $i_q=0$ means that $f_v \notin \Gamma_v$;
\item \label{item:aut:map}
  a partial function $\iota_q$ from $[1,k]$ to $[1, M]$, indicating
  which elements of $\Gamma_v$ are listed in $\tup{g}_v$ and their
  positions in the tuple of ${\cal{K}}$-types in the parent (this also
  provides $|\tup{g}_v|$);
\item \label{item:aut:luggage}
  a binary reflexive relation $\leadsto_q$ over $[1,k]$ representing
  for each element in $\Gamma_v$, a subset of $\Gamma_v$ containing
  this element;
\item \label{item:aut:relevant}
  a subset $R_q$ of $\mn{RCN}({\cal{K}})$ indicating concept names relevant for
  local elements in $v$;
\item \label{item:aut:relevant-parent}
  a subset $R'_q$ of $\mn{RCN}({\cal{K}})$ indicating concept names relevant for
  local elements in the parent $v'$ of $v$;
\item \label{item:aut:parent}
  a binary flag $\mathsf{sink}_q$ indicating whether $f_v$ is a sink
  or a source in the parent $v'$ of $v$;
\item \label{item:aut:grandparent}
  a binary flag $\mathsf{sink}'_q$ indicating whether
  $f_{v'}$ is a sink or a source in  the parent $v''$ of $v'$;
\item a binary flag $\mathsf{abox}_q$ indicating whether ${\cal{I}}_v \models {\cal{A}}$.
\end{enumerate}
Moreover, we only allow combinations of these values that satisfy the
following consistency conditions:

\begin{itemize}
\item if $i_q \neq 0$, then $\tau_q = \tau_q^{i_q}$ and $i_q
  \leadsto_q j$ for all $j \in [1,k]$;
\item if $i \in \dom(\iota_q)$ and $i \leadsto_q j$, then $j \in
  \dom(\iota_q)$;
\item if $\mathsf{sink}_q = 1$, then for each $A\in R'_q$ and  $j \in
  [1,k]$  it holds that $A \in \tau_q^j$ implies $j \in \dom(\iota_q)$.
\end{itemize}

\subsubsection{KB automaton}

Concept inclusions that involve only concept names are verified
locally. For the remaining checks, apart from the information stored
in the first component, it suffices to pass some aggregated
information about each element that is shared between nodes; that is,
$f_v$ and $\Gamma_v$ for each $v$. In what follows, by an $A$-successor
we mean a successor that belongs to the extension of the concept
$A$. Similarly for predecessors, direct successors, and direct
predecessors. The second component of state $q$ at node $v$ stores:
\begin{enumerate}
\item  a subset of $\dom(\iota_q)$, representing elements of $\Gamma_v$
  shared with the parent of $v$
  that are \emph{successors} of $f_v$ in the current subtree;
\item  a subset of $\dom(\iota_q)$, representing elements of $\Gamma_v$
  shared with the parent of $v$
  that are \emph{direct successors} of $f_v$ in the current subtree;
\item for each $A\in \mn{CN}({\cal{K}})$, the counts of
\begin{itemize}
\item  $A$-predecessors and direct $A$-predecessors (up to $1$),
\item  $A$-successors and direct $A$-successors (up to $N$)
\end{itemize}
of $f_v$ appearing in the current subtree as local elements;
\item for each $i\in [1,k]$ and $A\in \mn{CN}({\cal{K}})$, the counts of
\begin{itemize}
\item  $A$-successors and direct $A$-successors (up to $N$)
\end{itemize}
of the $i$th element of $\Gamma_v$ appearing as local elements in the
subtree rooted at the node $w$ such that $f_w$ is the $i$th element
of $\Gamma_v$.
\end{enumerate}
If $i_q \neq 0$, then the counts for the $i_q$th element of
$\Gamma_v$ must be consistent with those for $f_v$.

It is not difficult to maintain this information when processing the
tree, detecting violations of ${\cal{K}}$ along the way. The latter is done
when an element is \emph{forgotten}; that is, its record is not passed up
the tree any more. This happens exactly in the node where the said
element is fresh. Assuming that the current node is $v$, this
includes elements internal in ${\cal{I}}_v$ and $f_w$ for each child $w$ of
$v$ (among the latter, all elements of $\Gamma_v$ that are not listed in
$\tup{g}_v$). For each such element we compute the current counts,
based on ${\cal{I}}_v$ and the information passed from the children and the
parent (including the information on elements of $\Gamma_v$ that are
reachable from each $f_v$ and from other elements of $\Gamma_v$):
because all counts refer to local elements in disjoint parts of the
tree, there is no danger of counting anything twice. If the computed
counts violate some restriction imposed by ${\cal{K}}$, the automaton
rejects immediately. The maintanance amounts to updating the records
for those elements $e$ that are not getting forgotten in the current node. Note
that this requires accounting for those elements of $\Gamma_v$ that
are reachable from $e$ and are getting forgotten in $v$.
\todo{Finish maintanance.}

Observe that correctness of this construction relies on the safety condition.
Witnesses for positive counts of $A$-successors or $A$-predecessors
must be found among elements reachable or backwards reachable from the
elements in the current bag. Safety implies that these elements are
contained within a finite fragment of the decomposition.

\subsubsection{Query automaton}

The automaton guesses a $Q$-refutation and verifies that it is
consistent. The consistency condition, as given in
Definition~\ref{def:consistency}, can be easily checked based on the
label of the current node and the labels of the edges connecting it
with its children, provided that we are given the values
$\sigma(f_v)$ for all children $v$ of the current node. In fact,
note that in the condition of Definition~\ref{def:consistency}, one
can replace $\sigma(e)$ with $\sigma(e) \upharpoonright \{e\} \cup
\Gamma_u$. This is precisely the information the automaton will pass
between nodes: states of the query automaton are $Q$-types with
parameters $[0, M]$, where $0$ represents $f_v$ and each $i > 0$
represents $\tup{g}_v^i$. Moreover, we only allow $Q$-types in which no $q
\in Q$ occurs.

\subsubsection{Computability}

The set of states, initial states, and accepting states of the product
automaton ${\cal{B}}_{{\cal{K}}, Q, \Theta}$ can be clearly computed within the
desired complexity bounds. Let us see how to deal with
$\mathsf{step}_{{\cal{B}}_{{\cal{K}}, Q, \Theta}}$. Let $P$ be a set of states of
${\cal{B}}_{{\cal{K}}, Q, \Theta}$ and $q$ a single state of ${\cal{B}}_{{\cal{K}}, Q,
  \Theta}$. As a first step we remove from $P$ all states that are
incompatible with $q$. That is, we only keep states $p$ such that
\begin{itemize}
\item $\tau^i_p  =  \tau^{\iota_p(i)}_q$ for all $i \in \dom(\iota_p)$;
\item $R'_p = R_q$;
\item $\mathsf{sink}'_p = \mathsf{sink}_q$;
\item if $\mathsf{sink}_p = 0$, then $A \notin   \tau^i_q$ for all $A \in
  R_p$, $i \notin   \mathsf{img}(\iota_p)$;
\item $\left \{\iota_p(j) \bigm | i \leadsto_p
    j\right\} = \left \{j' \bigm | \iota_p(i) \leadsto_q
    j'\right\}$ for $i\in \dom(\iota_p)$;
\item for all $i\in \dom(\iota_p)$

  and all $A \in \mn{CN}({\cal{K}})$,

    the counts of $A$-successors and direct $A$-successors for
    $i$ in $p$ are equal to the respective counts for $\iota_p(i)$ in $q$.

\end{itemize}

Now, we shall construct a single-role $\ensuremath{(\ALCOIQfwd)^\smallplus}\xspace$ KB ${\cal{K}}'$ without
at-most restrictions over closures of roles, a query $Q' \in\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$, and
a type set $\Theta'$ such that $(P, q) \in \mathsf{step}_{{\cal{B}}_{{\cal{K}},Q,\Theta}}$
iff ${\cal{K}}' \notmodels_{\!\!\mathsf{fin}}^{\Theta'} Q'$. For ${\cal{K}}$ in $\ensuremath{\ALCI^\smallplus}\xspace$, the
construction almost directly gives ${\cal{K}}'$ in $\ensuremath{\ALCI^\smallplus}\xspace$: nominals are
not needed because the sets $\Gamma_u$ are empty in
${\cal{K}}$-decompositions, and CIs using counting will not be added.
If ${\cal{K}}$ is a $\ensuremath{\ALCQ^\smallplus}\xspace$ KB, ${\cal{K}}'$ will be in $\ensuremath{\ALCOQ^\smallplus}\xspace$. Nominals can
be eliminated as explained in Appendix~\ref{sec:ABoxesNom}, but
because the ABox is already trivial, there is no need of unravelling
and the reduction will give only one instance of $\ensuremath{\ALCQ^\smallplus}\xspace$.

\newcommand{\mathsf{Root}}{\mathsf{Root}}
\newcommand{\mathsf{Sink}}{\mathsf{Sink}}
\newcommand{\mathsf{Source}}{\mathsf{Source}}
\newcommand{\mathsf{Internal}}{\mathsf{Internal}}
\newcommand{\mathsf{Local}}{\mathsf{Local}}
\newcommand{\mathsf{Gamma}}{\mathsf{Gamma}}
\newcommand{\mathsf{External}}{\mathsf{External}}

Let us start with ${\cal{K}}'$. The ABox mentions a single individual $a_0$
and specifies its unary type as $\tau_q$. The TBox uses nominals $a_1,
\dots, a_k$ and specifies the unary type of $a_i$ as $\tau^i_q$. If
$i_q = 0$, then $a_0 \notin \{a_1, \dots, a_k\}$; otherwise, $a_0 =
a_{i_q}$.

We include into ${\cal{K}}'$ the axioms
\begin{align*}
  \mathsf{Root} & \equiv \{a_0\}\,,\\
  \mathsf{Gamma} & \equiv \{a_1,  \dots, a_k\}\,,\\

  \mathsf{Sink} & \equiv \forall r. \bot \,,\\
  \mathsf{Source} & \equiv \forall r^-. \bot  \sqcap \exists r.\top\,,\\
  \mathsf{Internal}  & \equiv \lnot(\mathsf{Sink} \sqcup \mathsf{Source}) \,,\\
  \mathsf{Local}  & \equiv \mathsf{Internal} \sqcup \mathsf{Root} \,,\\
  \mathsf{Gamma} & \sqsubseteq \mathsf{Sink} \sqcup \mathsf{Root}

\end{align*}
for fresh concept names $\mathsf{Root}$, $\mathsf{Gamma}$,
$\mathsf{Sink}$, $\mathsf{Source}$, $\mathsf{Internal}$, and $\mathsf{Local}$.
(If ${\cal{K}}$ does not use inverse roles, let $\mathsf{Source} \equiv \bot$.)
For each CI $A \sqsubseteq \qnrleq n {r^*} B$ in ${\cal{K}}$ with $n>0$, if $B \in R_q$, then add
\begin{align*}
    A  \sqcap B \sqcap \mathsf{Local} & \sqsubseteq  \mathsf{Gamma} \,,
\end{align*}
and
otherwise add
\begin{align*}
  A  \sqcap \mathsf{Local} & \sqsubseteq  \bot \,.
\end{align*}
Using these, we reformulate the CIs of ${\cal{K}}$ taking into account that some
neighbours of non-internal elements are outside of the current bag.
Aiming at reducing the number of cases, we model $\exists s. B$ as
$\qnrgeq 1 s B$ and $\forall s. B$ as $\qnrleq 0 s {\overline B}$ for
$s \in \big\{r^-, (r^-)^*\big\}$.

To model neighbours inside and outside the current bag, for each $B
\in \mn{CN}({\cal{K}}) \cup \{ \{a_i\} \bigm| 0\leq i \leq k\}$  and $n\leq N$ we introduce fresh concept names
\[E_{\qnrleq n r B} \,, \quad  E_{\qnrgeq n r B}\,, \quad E_{\qnrleq n
    {r^*} B} \,, \quad  E_{\qnrgeq n {r^*} B}\,, \]
\[E_{\qnrleq 0 {r^-} B} \,, \;\;  E_{\qnrgeq 1 {r^-} B}\,, \;\; E_{\qnrleq 0 {(r^-)^*} B} \,, \;\;  E_{\qnrgeq 1 {(r^-)^*} B} \,.\]
Let  $s \in\{r, r^-\}$.
For each CI of the form $A \sqsubseteq \qnrgeq n s B$ in ${\cal{K}}$, we add
\begin{align*}

  A &\sqsubseteq \bigsqcup_{i \leq n}   {\qnrgeq i s B} \sqcap
      E_{\qnrgeq {n-i} s B} \,,
\end{align*}
and analogously for CIs of the form $A \sqsubseteq \qnrleq n s B$.
For each CI of the form $A \sqsubseteq \qnrgeq 1 {s^*} B$, we
add
\begin{align*}

  %

  A \sqsubseteq  \qnrgeq 1 {s^*} {E_{\qnrgeq 1 {s^*} B}} \,,
\end{align*}
and for each CI of the form $A \sqsubseteq \qnrleq {0} {s^*} B$, we add
\begin{align*}

  A &
      \sqsubseteq \qnrleq 0 {s^*} {E_{\qnrgeq1 {s^*} {B}}} \,.
\end{align*}
For each CI of the form $A \sqsubseteq \qnrgeq {n} {r^*} B$,
we add
\begin{align*}

  %

  A \sqsubseteq \;
  \bigsqcup_{\alpha_0 + \sum_{i=1}^n \alpha_i\cdot i = n} \;
  F_{\qnrgeq {\alpha_0} {r^*} B} \sqcap
  \bigsqcap_{i=1}^n  F_{\qnrgeq {(\alpha_i, i)} {r^*} B}
  \,,\\
 \hspace{-7ex}   F_{\qnrgeq {\alpha} {r^*} B} \sqsubseteq\;
  \bigsqcup _{I \subseteq [1,k]\colon \alpha \leq \sum_{i\in I}
  \ell^B_i} \;\bigsqcap_{i \in I} F_{\qnrgeq 1 {r^*} {\{a_i\}}}
  \,,\\
  F_{\qnrgeq 1 {r^*} {\{a_i\}}} \sqsubseteq
  \qnrgeq 1 {r^*} {E_{\qnrgeq 1 {r^*} {\{a_i\}}}}
  \,,\\
  F_{\qnrgeq {(\alpha,\beta)} {r^*} B} \sqsubseteq
  \qnrgeq {\alpha} {r^*} {\lnot \mathsf{Gamma} \sqcap E_{\qnreq {\beta}{r^*} B}}
  \,,\\
  E_{\qnreq {\beta} {r^*} B}
  \sqsubseteq   E_{\qnrleq {\beta} {r^*} B} \sqcap E_{\qnrgeq {\beta} {r^*} B}
\end{align*}
for $\alpha,\beta \leq N$, $i\in [1,k]$, where $\ell_i^B$ is the count of
$B$-successors of $a_i$ stored in $q$.
For each CI of the form $A \sqsubseteq
\qnrleq {n} {r^*} B$ where $n>0$ and $B \in R_q$, we add
\begin{align*}
  \mathsf{Local} \sqcap A &\sqsubseteq
  \bigsqcup_{O \subseteq \widehat B \colon |O| \leq  n} \;
  \bigsqcap_{o \in \widehat B \setminus O}
  F_{\qnrleq 0 {r^*} {\{o\}}} \,,\\
  F_{\qnrleq 0 {r^*} {\{a_i\}}} &
                                \sqsubseteq \qnrleq 0 {r^*} { E_{\qnrgeq 1 {r^*} {\{a_i\}}}} \,,
\end{align*}
where $\widehat B = \left\{a_i \bigm | B \in \tau_q^i\right\}$.

We need to ensure that the concepts modelling neighbours are
interpreted in a way consistent with the information in the
states. First, we ensure that internal elements do not have any
external neighbours by adding
\begin{align*}
  \mathsf{Internal} &
                     \sqsubseteq
                     \bigsqcap_{n \geq  0} E_{\qnrleq n s B} \,,\\
  \mathsf{Internal} &
                     \sqsubseteq
                     E_{\qnrgeq 0 s B} \sqcap
                     \bigsqcap_{n > 0} \lnot  E_{\qnrgeq n s B} \,,\\
  \lnot B \sqcap \mathsf{Internal} &
                     \sqsubseteq
                     \bigsqcap_{n \geq  0} E_{\qnrleq n {s^*} B} \,,\\
  \lnot B \sqcap \mathsf{Internal} &
                     \sqsubseteq
                     E_{\qnrgeq 0 {s^*} B} \sqcap
                     \bigsqcap_{n > 0} \lnot  E_{\qnrgeq n {s^*} B} \,,\\
  B \sqcap \mathsf{Internal} &
                     \sqsubseteq
                       \lnot E_{\qnrleq 0 {s^*} B} \sqcap
                       \bigsqcap_{n >  0} E_{\qnrleq n {s^*} B} \,,\\
  B \sqcap \mathsf{Internal} &
                     \sqsubseteq

                       \bigsqcap_{n \leq 1}  E_{\qnrgeq n {s^*} B} \sqcap
                       \bigsqcap_{n > 1} \lnot  E_{\qnrgeq n {s^*} B}
\end{align*}
for all $B \in \mn{CN}({\cal{K}}) \cup \{ \{a_i\} \bigm| 0\leq i \leq k\}$ and $s \in \left\{r, r^-\right\}$.

Next, we take care of sinks. For those not in $\{a_0, a_1\dots, a_k\}$ we let
\begin{align*}
\mathsf{Sink} \sqcap \lnot (\mathsf{Gamma}\sqcup \mathsf{Root})\sqsubseteq \;\bigsqcup_{\substack{p
  \in P \colon i_p \notin \dom(\iota_p)\\ \mathsf{sink}_p=1}} \;\bigsqcap_{A \in \widehat\tau_p}\; A \,,
\end{align*}
where $\widehat \tau_p$ is the extension of $\tau_p$ to concept names
$E_{\qnrleq n t B}$ and $E_{\qnrgeq n t B}$ that reflects the counts
of neighbours in the current subtree stored in $p$.
For $a_i$ with $i \notin \dom(\iota_q)$ the condition is similar:
\begin{align*}
\{a_i\} \sqsubseteq \;\bigsqcup_{p
  \in P \colon \iota_p(i_p) =i} \;\bigsqcap_{A \in \widehat\tau_p}\; A \,.
\end{align*}
\todo{Finish backwards requirements for local nominals. }
For $a_i$ with $i \in \dom(\iota_q)$, different from $a_0$, the
condition is extracted exclusively from the counts stored in $q$; an
appropriate subtree will be provided in the bag where the element
corresponding to $a_i$ is fresh.

For sources different from $a_0$, shared elements might be successors or direct
successors both in the current bag and outside. To handle that, for
each conjunction $C$ choosing either $\qnrleq 0 t {\{ a_i\}}$ or $\qnrgeq
1 t {\{ a_i\}}$ for each $t\in\{r, r^*\}$ and $i\in [1,k]$, we add a
separate conditions
\begin{align*}
C \sqcap \mathsf{Source} \sqcap \lnot \mathsf{Root} \sqsubseteq \;\bigsqcup_{\substack{p
  \in P \colon i_p \notin \dom(\iota_p)\\ \mathsf{sink}_p = 0}} \;\bigsqcap_{A \in \widehat\tau_p^C}\; A \,,
\end{align*}
in which $\widehat \tau_p^C$ accounts for the connections to $a_i$ with
$i \in \mathsf{img}(\iota_p)$ described in $C$.

Finally, we let
\begin{align*}
\{a_0\} \sqsubseteq \bigsqcap_{A \in \widehat\tau_q}\; A \,,
\end{align*}
where $\widehat \tau_q$ extracts information about counts of external
neighbours from the counts in the current subtree stored in $q$ and
the total counts represented in the ${\cal{K}}$-type $\tau_q$.

Note that many disjunctions above have doubly exponential length. To avoid
blowup, instead of actually putting them into ${\cal{K}}'$ we encode them in the
type set $\Theta'$, by filtering out types that do not satisfy
them. Of course, $\Theta'$ also filters out types that are not
extensions of types from $\Theta$.

Let us deal with the query now.

\begin{definition}[unary $Q$-type]
  A unary $Q$-type with parameters $\Gamma$ is a set of triples of the
  form $(p, V, \eta)$ such that $p$ is a fragment of $Q$,
  $V \subseteq \textit{var}(p)$, and $\eta$ is a partial mapping from $\textit{var}(p)
  \setminus V$ to $\Gamma$.
\end{definition}

The definition below captures the condition relating the the $Q$-type
stored in state $q$ with $Q$-types stored in states from $P$. The
function $\Sigma$ it mentions in our case maps each
$\tau \in \mn{Tp}({\cal{K}}')$ to the set $\Sigma(\tau)$ of unary $Q$-types
 with parameters $\{a_1, a_2,
\dots, a_k\}$,
\[\left\{ \big( f, \eta^{-1}(\{0\}),
    a_*\circ \iota_p \circ \eta\upharpoonright [1,k] \setminus \{i_p\}

    \big) \bigm | (f, \eta) \in \tau^Q_p \right\},\]
where $a_*$ is a function mapping $i$ to $a_i$, $\tau^Q_p$ is the
$Q$-type the stored in state $p$, and $p$ ranges over states in $ P$ that are compatible
with $\tau$; that is, satisfy one of the following conditions:
\begin{itemize}
\item $\left\{\mathsf{Sink}, \overline{\mathsf{Gamma}}, \overline{\mathsf{Root}}\right\} \cup \widehat
  \tau_p\subseteq \tau$, $\mathsf{sink}_p \!=\! 1$, $i_p \!\notin\!
  \dom(\iota_p)$,
\item $\left\{\mathsf{Source},  \overline{\mathsf{Root}}\right\} \cup \widehat \tau_p^C
  \cup C \subseteq \tau$, $\mathsf{sink}_p = 0$, $i_p \notin
  \dom(\iota_p)$,
\item  $\left\{\{a_i\}\right\} \cup \tau_p \subseteq \tau$,
  $\iota_p(i_p) =i \notin \dom(\iota_q)$.
\end{itemize}

\begin{definition} [weak realizability modulo]
  Consider a KB ${\cal{K}}'$, a $Q$-type
$\tau$ with parameters $\Gamma \subseteq \mn{ind}({\cal{K}}')$, and a function
$\Sigma$ mapping unary ${\cal{K}}'$-types to sets of unary $Q$-types with
parameters $\Gamma$. The $Q$-type $\tau$ is \emph{weakly realized
modulo $\Sigma$} in a ${\cal{K}}'$-interpretation ${\cal{M}}$ if
  \[\tau \supseteq \bigg(\mn{wtp}^{\cal{M}}_Q\big(\Gamma\cup\dom(\sigma)\big)
    \oplus \bigoplus_{d\in \dom(\sigma)} \sigma(d) \bigg)
    \upharpoonright \Gamma\,.\]
  for some partial function $\sigma$ mapping elements $d\in\Delta^{\cal{M}}$ to $Q$-types
  $\sigma(d)$ with parameters $\{d\} \cup \Gamma$ such that
  $ \left \{ \left(p, \eta^{-1}(d), \eta\upharpoonright \Gamma\right) \bigm |
    (p,\eta)\in\sigma(d) \right\} \in \Sigma\big(\mn{tp}^{{\cal{K}}'}_{\cal{M}}(d)\big)$.
\end{definition}

\begin{lemma}
  Given $Q\in\ensuremath{\UCQ^\smallplus}\xspace$, a KB ${\cal{K}}'$, a set $\Theta' \subseteq \mn{Tp}({\cal{K}}')$,
  a $Q$-type $\tau$ with parameters
  $\Gamma \subseteq \mn{ind}({\cal{K}}')$, and a function $\Sigma$ mapping unary
  ${\cal{K}}'$-types to sets of unary $Q$-types with parameters $\Gamma$,
  one can construct $Q'\in \ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$ and $\Theta''$ such that ${\cal{K}}'
  \models_{\mathsf{fin}}^{\Theta''} Q'$ if $\tau$ is weakly realizable modulo $\Sigma$ in a
  finite model of ${\cal{K}}'$ realizing only types from $\Theta'$.
\end{lemma}

\begin{proof}
For each triple of the form $(p, V, \eta)$ such that $p$ is a
subquery of a query from $Q$, $V \subseteq \textit{var}(p)$, and $\eta$ is a
partial mapping from $\textit{var}(p) \setminus V$ to $\Gamma$, introduce a
concept $A_{p, V, \eta}$. This adds $|Q|\cdot 2^m\cdot (|\Gamma|+1)^n$
concepts, where $m = \max_{q\in Q}|q|$ and $n = \max_{q\in Q}
|\textit{var}(q)|$.

Let $\Theta''$ be the set of all unary types (over the
extended set of concept names) of the form $\theta \cup \theta'$ where
$\theta \in \Theta'$ and there exists a unary $Q$-type $\upsilon \in
\Sigma(\theta)$ such that $\overline{A_{p, V, \eta}} \in \theta'$ for
all $(p, V, \eta) \in \upsilon$. In the model we seek, we shall
allow only unary types from $\Theta''$.

We now define a query $Q' \in \ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$ that will be forbidden in
the model we seek. Choose
\begin{itemize}
\item
  a fragment $p$ of $Q$ and a partial mapping from
  $\textit{var}(p)$ to $\Gamma$ such that $(p, \eta) \notin \tau$;
\item
  a partition of $p$ into fragments $p'$ and $p_1, \dots, p_k$ such that
  $\textit{var}(p_i) \cap \textit{var}(p_j) \subseteq \textit{var}(p') \cup \eta^{-1}(\Gamma)$
  for all $i \neq j$;
\item a localization $p''$ of $p'$.
\end{itemize}
For each choice, add to $Q'$ the query
$\eta(p'' \land \bigwedge_{i=1}^k \widetilde p_i)$, where
\begin{align*}
  \widetilde p_i &= A_{p_i, V_i, \eta_i}(y_i) \land \bigwedge_{x \in
                   V_i} x = y_i\,,\\
  \eta_i &= \eta\upharpoonright \textit{var}(p_i)\,,\\
  V_i &= \textit{var}(p_i) \cap \textit{var}(p') \setminus \eta^{-1}(\Gamma)\,,
\end{align*}
and $y_i$ is a fresh variable. With $m = \max_{q \in Q} |q|$,  we have
\[|Q'| \leq
  \big(|Q|\cdot 2^m \cdot (|\Gamma|+1)^n\big) \cdot m^m \cdot  2^m
\]
and, after eliminating equality atoms in the usual, way
each conjunctive query in $Q'$ has size $O(m)$.
\end{proof}

\subsection{Proof of Lemma~\ref{lem:folding-correct}}

Let us call an interpretion \emph{$\ell$-bounded} if the length of
simple directed paths in this interpretation is at most $\ell$.

\begin{lemma} \label{lem:bounded-transfer}
  ${\cal{F}}$ is $\ell$-bounded.
\end{lemma}

\begin{proof}
  Redirected edges orginate in ${\cal{I}}_u$ such that $f_u$ is a source
  in ${\cal{I}}_{u'}$ for the parent $u'$ of $u$, and lead to $f_{\hat v}$
  that is a sink in ${\cal{I}}_{\hat v'}$ for the parent $\hat v'$ of $\hat
  v$. Consequently, a simple directed path $\pi$ taking an edge
  redirected from $f_v$ to $f_{\hat v}$ (as the first redirected
  edge) cannot reach the origin of another redirected edge. Hence, the
  suffix of $\pi$ starting in $f_{\hat v}$ is a path in ${\cal{I}}'$, and
  its length is bounded by $\ell$. Because $N^{{\cal{I}}_n}_n(f_{v})\simeq
  N^{{\cal{I}}_n}_n(f_{\hat v})$ and $n\geq \ell$, a simple directed path
  originating in $f_{v}$, of the same length as the suffix, can be
  found in ${\cal{I}}'$. Consequently, there exists a simple path in
  ${\cal{I}}'$ of the same length as $\pi$: instead of taking the
  redirected edge, take the original edge to $f_v$ and continue from
  there; because $\pi$ enters $f_v$ from ${\cal{I}}_{v'}$ for the parent
  $v'$ of $v$, and $f_v$ is a sink in ${\cal{I}}_{v'}$, the resulting path
  is indeed simple. It follows that the length of the whole $\pi$ is
  bounded by $\ell$.
\end{proof}

\begin{lemma}
  ${\cal{F}} \models {\cal{K}}$.
\end{lemma}
\begin{proof}
  Because the unary types of $f_v$ and $f_{\hat v}$ coincide,
  redirections of edges do not violate concept inclusions of ${\cal{K}}$
  that do not involve transitive closure. In $\ell$-bounded
  interpretations, each universal restriction is equivalent to not
  satisfying a UCQ with at most $\ell$ binary atoms per
  CQ. Consequently, ${\cal{F}}$ satisfies all universal restrictions by
  Fact~\ref{fact:coloured-blocking}.  It remains to verify
  existential restrictions involving transitive closure. Consider a
  forward  path $\pi$ witnessing an existential restriction in ${\cal{I}}'$
  and suppose that the origin of this path is still in still in
  ${\cal{F}}$. Because ${\cal{I}}'$ is $\ell$-bounded, the path has length at
  most $\ell$. If this path does not pass through a redirected edge, we
  are done. Suppose that it does pass an edge redirected from $f_v$
  to $f_{\hat v}$. Then we can transfer the suffix of the path
  after $f_v$ to $f_{\hat v}$, because  $N^{{\cal{I}}_n}_n(f_{v})\simeq
  N^{{\cal{I}}_n}_n(f_{\hat v})$ and $n\geq \ell$. Like in the proof of
  Lemma~\ref{lem:bounded-transfer}, the transferred suffix cannot take
  another redirected edge, and we are done.
\end{proof}

\section{Outlook}

This paper provides first positive results on finite entailment of
non-local queries over DLs knowledge bases. The main technical
contribution is optimal \ensuremath{\textsc{2ExpTime}}\xspace upper bounds for finite entailment of
$\ensuremath{\UCQ^\smallplus}\xspace\!$s over \ensuremath{\ALCOI^\smallplus}\xspace and \ensuremath{\ALCOQ^\smallplus}\xspace knowledge bases. To obtain these
results, we have shown intermediate reductions that are interesting in
their own, and could be applied to similar settings.

\smallskip
 There are several directions to follow for future work. A first
possibility is to vary the DL language.  One could consider
lightweight DLs from the $\mathcal{EL}$ and \textsl{DL-Lite} families
or extensions of \ensuremath{\ALCOI^\smallplus}\xspace with e.g. role inclusions. For
the latter, a different approach to the one proposed here is needed
because our techniques rely on the lack of interaction between
different roles. Another option is to allow for controlled interaction
of inverses and number restrictions as e.g.\ in \ensuremath{(\ALCIQfwd)^\smallplus}\xspace. A second
possibility is to consider more expressive non-local queries, such as
positive regular path queries. In this case new techniques seem to be
needed, e.g.\ the coloured blocking principle does not
work for PRPQs.

\section{Hardness}
\par \noindent {\bf Theorem~\ref{thm:LoweBound}}
Finite entailment of  $\ensuremath{\CQ^\smallplus}\xspace\!$s over \ALC knowledge bases is \ensuremath{\textsc{2ExpTime}}\xspace-hard.
\newcommand{\ensuremath{\Kmc_{(\Mmc, w)}}}{\ensuremath{\Kmc_{(\Mmc, w)}}}
\newcommand{\ensuremath{q_{\Mmc,w}}}{\ensuremath{q_{\Mmc,w}}}

\begin{proof}
We reduce the word problem of exponentially space bounded alternating Turing machines.
For each input word $w$ to $\Mmc= (Q, \Sigma, q_0, \delta)$, we define an \ALC knowledge base $\ensuremath{\Kmc_{(\Mmc, w)}}$ and a $\ensuremath{\CQ^\smallplus}\xspace\!$ $q$ such that $\Mmc$ accepts $w$ iff there is a counter-model of $\ensuremath{\Kmc_{(\Mmc, w)}}$ and $\ensuremath{q_{\Mmc,w}}$.

Each finite forest counter-model of $\ensuremath{\Kmc_{(\Mmc, w)}}$ and $\ensuremath{q_{\Mmc,w}}$ will represent an accepting computation of $\Mmc$ and $w$.
Our encoding follows closely the one use in~\cite{EiterLOS09} to show that (arbitrary) entailment of CQs
over $\mathcal{SH}$ knowledge bases is \ensuremath{\textsc{2ExpTime}}\xspace-hard. In particular, each tree model of $\ensuremath{\Kmc_{(\Mmc, w)}}$ encodes an accepting \emph{computation tree} in which each node is the root of a \emph{configuration tree} (see Figure~\ref{fig:comp-tree}). Notably, there are two consecutive edges connecting a configuration tree and any of its successor configurations. Further, each configuration tree is a complete binary tree of depth  equal to the length of the input word $|w|$, and whose leaves shall store the tape contents using a \emph{cell gadget} as illustrated in Figure~\ref{fig:conf-tree}. Each \emph{cell gadget}
records the current (right descendants) and the previous (left descendants) configuration of $\Mmc$.  The particular structure of a cell gadget is illustrated in Figure~\ref{fig:cell-gadget}.  The root of each gadget cell is labelled with concepts names $B_1, \dots, B_m$ that encode (in binary) the position of the cell in the tape.  The node labelled with concept name $E_h$ records pairs $(q,a)$ (not) satisfied in the current configuration, whereas $F_h$ records all possible pairs $(q,a)$ with $q \in Q$ and $a \in \Sigma$ using concept names $Z_{q,a}$. The actual content of the cell in the current (previous) configuration is recorded in the node labelled by $G_h$ ($G_p$) using a concept name for each symbol in $\Sigma$;
symmetrically, the node $F_p$ records the pairs  (not) satisfied in the previous configuration and $E_p$ all possible pairs $(q,a)$.

Concept inclusions in $\ensuremath{\Kmc_{(\Mmc, w)}}$ to enforce the structure fo configuration trees are rather standard and use a single role $r$. They ensure locally  that in every gadget the current configuration is indeed a successor of the previous configuration. All the relevant axioms to ensure this from the encoding in ~\cite{EiterLOS09} can be expressed in \ALC.

\medskip
We will use a $\ensuremath{\CQ^\smallplus}\xspace\!$   $q_w$  to ensure that computation trees are \emph{proper}, i.e., that the previous configuration recorded in each configuration tree $T$ coincides with the current configuration recorded in all its successors $T'$. This property can be characterised as follows:

\begin{lemma}[Proposition 4 in~\cite{EiterLOS09}]\label{lemma:ProperLB}
A computation tree is not proper iff  there exists a cell gadget $n$ in some configuration tree $T$ and a cell gadget $n'$ in a successor configuration of $T$ such that for all $A \in \Bbf \cup \Zbf$

\begin{itemize}
\item[$(\dagger)$] $A$ is true at the $E_h$-node of $n$ and the $E_p$-node of $n'$, or
\item[$(\ddagger)$]  $A$ is true at the $F_h$-node of $n$ and the $F_p$-node of $n$.
\end{itemize}
\end{lemma}
where $\Bbf = \{B_1, \dots, B_m\}$ is the set of all concept names used to encode the cell addresses, and $\Zbf = \{ Z_{q,a} \mid q \in  Q, a\in \Sigma \}$
is the set of concept names used as markers in the cell gadgets.
Notably, (the proof of) Lemma~\ref{lemma:ProperLB} does not rely on the use of role inclusions not transitive roles in the encoding.

Thus, the query $q_w$ should be able to test properties $(\dagger)$ and $(\ddagger)$ for each $A \in \Bbf \cup \Zbf$. We achieve this by taking a copy of the query shown in Figure~\ref{fig:BasicQ}, for each $A  \in \Bbf \cup \Zbf$.  Possible matches of one of these copies in a computation tree are illustrated on Figure~\ref{fig:BasicQ}. The required query $q_w$ is the conjunction of all these copies.

\end{proof}

\begin{figure}\caption{ATM computations}\label{fig:comp-tree}
\centerline{%
\begin{tikzpicture}[>=latex,point/.style={circle,draw=black,minimum size=1.4mm,inner sep=0pt}]
\node[point, fill=black] (t1) at (0,2){};
\node[point, fill=black] (t12) at (1.5,1.5){};
\node[point, fill=black] (t22) at (3,1){};
\node[point, fill=black] (t13) at (4.5,0.5){};
\node[point, fill=black] (t23) at (6,0){};
\node[point,fill=black] (t14) at (4.5,2){};
\node[point, fill=black] (t24) at (6,3){};
\draw[thin] (0,2) -- (-1,0) -- (1,0) -- cycle;
\draw[->,out=10,in=130](t1) to node[pos=0.5,sloped, above] {$r$}  (t12);
\draw[->,out=10,in=130](t12) to node[pos=0.5,sloped, above] {$r$}  (t22);
\draw[->,out=10,in=130](t22) to node[pos=0.5,sloped, above] {$r$}  (t13);
\draw[->,out=10,in=130](t13) to node[pos=0.5,sloped, above] {$r$}  (t23);
\draw[->,out=70,in=180](t14) to node[pos=0.5,sloped, above] {$r$} (t24);
\draw[->,out=70,in=180](t22) to node[pos=0.5,sloped, above] {$r$} (t14);
\draw[thin] (3,1) -- (2,-1) -- (4,-1) -- cycle;
\draw[thin] (6,3) -- (5,1) -- (7,1) -- cycle;
\draw[thin] (6,0) -- (5,-2) -- (7,-2) -- cycle;
\end{tikzpicture}%
}
\end{figure}
\begin{figure}\caption{Configuration Tree}\label{fig:conf-tree}
\centerline{
\begin{tikzpicture}[>=latex,thick,point/.style={circle,draw=black,minimum size=1.4mm,inner sep=0pt}]
\coordinate (A) at (0,3);
\coordinate (B) at (-4,0);
\coordinate(C) at (4,0);
\draw[color=gray] (A) -- (B) -- (C) -- cycle;
\foreach \x in  {-4, 0, 4}{
\node[point, fill=black] (cp) at (\x,0) {};
\node[point, fill=black] (lp) at (\x-0.5,-0.7) {};
\node[point, fill=black] (llp) at (\x-0.5,-1.4) {};
\node[point, fill=black] (lllp) at (\x-0.5,-2.1) {};
\node[point, fill=black] (rp) at (\x+0.5,-0.7) {};
\node[point, fill=black] (rrp) at (\x+0.5,-1.4) {};
\node[point, fill=black] (rrrp) at (\x+0.5,-2.1) {};
 %
\draw[->] (cp) to  node[pos=0.5,sloped, above] {$r$} (lp);
\draw[->] (cp) to  node[pos=0.5,sloped, above] {$r$} (rp);
\draw[->] (lp) to  node[pos=0.5, left] {$r$} (llp);
\draw[->] (llp) to  node[pos=0.5, left] {$r$} (lllp);
\draw[->] (rp) to  node[pos=0.5, right] {$r$} (rrp);
\draw[->] (rrp) to  node[pos=0.5, right] {$r$} (rrrp);
}
\node at (-2,-1.4){$\dots$};
\node at (2,-1.4){$\dots$};
\draw[color=gray, zigzag] (A) to node[pos= 0.5, right]{$|w|$} (0,0);
\end{tikzpicture}%
}
\end{figure}
\begin{figure}\caption{Cell gadget}\label{fig:cell-gadget}
\centerline{%
\begin{tikzpicture}[>=latex,thick,point/.style={circle,draw=black,minimum size=1.4mm,inner sep=0pt}]
\node[point, fill=black, label=above:{$L_m$}] (cp) at (0,0) {};
\node[point, fill=black, label=left:{$E_P,X$}] (lp) at (-1,-1) {};
\node[point, fill=black, label=left:{$F_P,X$}] (llp) at (-1,-2.3) {};
\node[point, fill=black, label=left:{$G_P$}] (lllp) at (-1,-3.3) {};
\node[point, fill=black, label=right:{$E_h,X$}] (rp) at (1,-1) {};
\node[point, fill=black, label=right:{$F_h,X$}] (rrp) at (1,-2.3) {};
\node[point, fill=black, label=left:{$G_h$}] (rrrp) at (1,-3.3) {};
\draw[->] (cp) to  node[pos=0.5,sloped, above] {$r$} (lp);
\draw[->] (cp) to  node[pos=0.5,sloped, above] {$r$} (rp);
\draw[->] (lp) to  node[pos=0.5, left] {$r$} (llp);
\draw[->] (llp) to  node[pos=0.5, left] {$r$} (lllp);
\draw[->] (rp) to  node[pos=0.5, right] {$r$} (rrp);
\draw[->] (rrp) to  node[pos=0.5, right] {$r$} (rrrp);
\end{tikzpicture}
}
\end{figure}
\begin{figure*}\caption{Basic Query}\label{fig:BasicQ}
\centerline{
\begin{tikzpicture}[>=latex,thick,point/.style={circle,draw=black,minimum size=1.4mm,inner sep=0pt}]
\node[point, fill=white, label=above:{$x$}] (x) at (0,0) {};
\node[point,  fill=white, label=left:{$y_0$}] (y0) at (-1,-1) {};
\node[point, fill=white, label=left:{$y_1$}] (y1) at (-1,-2.3) {};
\node[point,  fill=white, label=left:{$y_m$}] (ym) at (-1,-3.5) {};
\node[point,  fill=white, label=left:{$y_{m+1}$}, label= right:{$X, A$}] (X) at (-1,-3.5- 1.3) {};
\node[point,  fill=white, label=below:{$u$}, label= right:{$G_h$}] (Gh) at (-1,-3.5 - 2.6) {};
\node[point,  fill=white, label=right:{$z_0$}] (z0) at (1,-1) {};
\node[point, fill=white, label=right:{$z_1$}] (z1) at (1,-2.3) {};
\node[point,  fill=white, label=right:{$z_{m+2}$}] (zm2) at (1,-5) {};
\node[point,  fill=white, label=right:{$z_{m+3}$}, label=left:{$X, A$}] (XR) at (1,-5-1.3) {};
\node[point,  fill=white, label=below:{$v$}, label=left:{$G_p$}] (Gp) at (1,-5-2.6) {};
\draw[->] (x) to  node[pos=0.5,sloped, above] {$r$} (y0);
\draw[->] (x) to  node[pos=0.5,sloped, above] {$r$} (z0);
\draw[->] (y0) to  node[pos=0.5, left] {$r$} (y1);
\draw[->,dotted](y1) to (ym);
\draw[->] (ym) to  node[pos=0.5, left] {$r$} (X);
\draw[->] (zm2) to  node[pos=0.5, right] {$r$} (XR);
\draw[->] (X) to  node[pos=0.5, left] {$r^+$} (Gh);
\draw[->] (XR) to  node[pos=0.5, right] {$r^+$} (Gp);
\draw[->] (z0) to  node[pos=0.5, right] {$r$} (z1);
\draw[->,dotted] (z1) to  (zm2);
\coordinate (A) at (7,0);
\coordinate (B) at (5,-3);
\coordinate(C) at (9,-3);
\draw[color=gray] (A) -- (B) -- (C) -- cycle;
\node[point, fill=black, label=above right:$L_0$] at (A) {};
\node[point, fill=black, label=above right:$L_0$] at (12,-1) {};
\draw[color=gray] (12,-1) -- (10,-4) -- (14,-4) -- cycle;
\node[point, fill=black] (p) at (9.5, -0.5){};
\draw[->] (A) to node[pos=0.5, above]{$r$} (p);
\draw[->] (5,0) to node[pos=0.5, above]{$r$} (A);
\draw[->] (3,0) to node[pos=0.5, above]{$r$} (5,0);
\draw[->](p) to node[pos=0.5, above]{$r$} (12,-1);
\node[shift={(7,-3)}, point, fill=black, label=above:{$L_m$}] (cp) at (0,0) {};
\node[shift={(7,-3)}, point, fill=black, label=left:{$E_P,X$}] (lp) at (-1,-1) {};
\node[shift={(7,-3)}, point, fill=black, label=left:{$F_P,X$}] (llp) at (-1,-2.3) {};
\node[shift={(7,-3)}, point, fill=black, label=left:{$G_P$}] (lllp) at (-1,-3.3) {};
\node[shift={(7,-3)}, point, fill=black, label=right:{$E_h,X$}] (rp) at (1,-1) {};
\node[shift={(7,-3)}, point, fill=black, label=right:{$F_h,X$}] (rrp) at (1,-2.3) {};
\node[shift={(7,-3)}, point, fill=black, label=left:{$G_h$}] (rrrp) at (1,-3.3) {};
\draw[->] (cp) to  node[pos=0.5,sloped, above] {$r$} (lp);
\draw[->] (cp) to  node[pos=0.5,sloped, above] {$r$} (rp);
\draw[->] (lp) to  node[pos=0.5, left] {$r$} (llp);
\draw[->] (llp) to  node[pos=0.5, left] {$r$} (lllp);
\draw[->] (rp) to  node[pos=0.5, right] {$r$} (rrp);
\draw[->] (rrp) to  node[pos=0.5, right] {$r$} (rrrp);
\node[shift={(12,-4)}, point, fill=black, label=above:{$L_m$}] (Lm) at (0,0) {};
\node[shift={(12,-4)}, point, fill=black, label=left:{$E_P,X$}] (EP) at (-1,-1) {};
\node[shift={(12,-4)}, point, fill=black, label=left:{$F_P,X$}] (FP) at (-1,-2.3) {};
\node[shift={(12,-4)}, point, fill=black, label=left:{$G_P$}] (GP) at (-1,-3.3) {};
\node[shift={(12,-4)}, point, fill=black, label=right:{$E_h,X$}] (EH) at (1,-1) {};
\node[shift={(12,-4)}, point, fill=black, label=right:{$F_h,X$}] (FH) at (1,-2.3) {};
\node[shift={(12,-4)}, point, fill=black, label=left:{$G_h$}] (GH) at (1,-3.3) {};
\draw[->] (Lm) to  node[pos=0.5,sloped, above] {$r$} (EP);
\draw[->] (Lm) to  node[pos=0.5,sloped, above] {$r$} (EH);
\draw[->] (EP) to  node[pos=0.5, left] {$r$} (FP);
\draw[->] (FP) to  node[pos=0.5, left] {$r$} (GP);
\draw[->] (EH) to  node[pos=0.5, right] {$r$} (FH);
\draw[->] (FH) to  node[pos=0.5, right] {$r$} (GH);
\draw[dashed,out=-20,in=200,] (Gp) to (GP);
\draw[dashed,out=10,in=170] (Gh) to (rrrp);
\draw[dashed,out=10,in=170, blue] (X) to (rrp);
\draw[dashed,out=20,in=160, orange] (X) to (rp);
\draw[dashed,out=20,in=160, blue] (x) to (A);
\draw[dashed,out=-20,in=200, orange] (x) to (5,0);
\draw[dashed,out=-20,in=200, orange] (z0) to (A);
\draw[dashed,out=-20,in=200, blue] (z0) to (p);
\draw[dashed,out=-20,in=200, blue] (XR) to (FP);
\draw[dashed,out=-20,in=220, orange] (XR) to (EP);
\end{tikzpicture}}
\end{figure*}

\section{Introduction}

The use of ontologies to provide background knowledge for enriching
answers to queries posed to a database is a major research topic
in the fields of knowledge representation and
reasoning. In this data-centric setting, various options for the
formalisms used to express ontologies and queries exist,
but popular choices are
description logics (DLs)
and either unions of conjunctive queries (UCQs) or navigational queries.
The main reasoning problem in this scenario is query
entailment, which has been extensively investigated for different
combinations of DLs and query languages.  An important assumption in
data-centric applications is that both database instances and the
models they represent are finite.  The study of \emph{finite}
query entailment, where one is interested in reasoning over finite
models only, is thus paramount. Even so, the finite model semantics
has received far less attention than the unrestricted one.

Prior work on finite query entailment in description logics has
concentrated on \emph{local} queries, UCQs in
particular~\cite{Rosati08,GarciaLS14,AmarilliB15,GogaczIM18,Kieronski18,GogaczGIJM19}.
The single work studying extensions of UCQs \cite{Rudolph16},
brings only undecidability results for navigational queries and
various expressive description logics. In contrast, for unrestricted
entailment a large body of literature is available, providing multiple
positive results for navigational queries and both expressive and lightweight DLs
\cite{CalvaneseEO14,StefanoniMKR14,BienvenuOS15,JungLMS17,GuIbJu-AAAI18,GogaczGIJM19,BednarczykR19}.
The lack of research on finite entailment of non-local queries (e.g.\
variants of regular path queries) comes as a surprise since, as noted
in the above works, they are necessary in data centric applications
dealing with graph databases.

In this paper, we close the distance to the undecidability frontier
for finite entailment delineated by \citeauthor{Rudolph16}~(\citeyear{Rudolph16})
by identifying some decidable classes of non-local ontology-mediated queries.
We focus on UCQs with transitive closure over roles;
from the viewpoint of DL applications, transitive closure is arguably
one of the most useful features of regular expressions over roles. As the
ontology component, we consider extensions of the DL \ALC, allowing for
transitive closure of roles. The study of finite entailment is relevant
for this combination because, unlike for plain CQs,
query entailment of CQs with transitive closure is not
finitely controllable even for \ALC, and thus finite and unrestricted
entailment do not coincide. As a consequence, dedicated algorithmic
methods and lower bounds need to be developed.

Our main finding is that
finite entailment of UCQs with transitive closure over
\ensuremath{\ALCOI^\smallplus}\xspace or \ensuremath{\ALCOQ^\smallplus}\xspace knowledge bases is \ensuremath{\textsc{2ExpTime}}\xspace-complete.
As unrestricted entailment of positive regular path queries is
\ensuremath{\textsc{2ExpTime}}\xspace-complete for both logics~\cite{CalvaneseEO14,BednarczykR19},
and the hardness already holds for CQs and both \ALCI and \ALCO
~\cite{DBLP:conf/cade/Lutz08,DBLP:conf/kr/NgoOS16}, we have that the
complexity of our setting is the same over arbitrary and finite
models.
As finite entailment of two-way regular path queries over
$\mathcal{ALCIOF}$ knowledge bases is undecidable~\cite{Rudolph16},
our results are quite close to the undecidability frontier.

While there exist positive results on finite entailment in
expressive DLs related to \ensuremath{\ALCOI^\smallplus}\xspace or \ensuremath{\ALCOQ^\smallplus}\xspace, they are all about local
queries. For example, the \ensuremath{\textsc{2ExpTime}}\xspace algorithms for finite entailment of
UCQs over \ensuremath{{\cal{S\hspace{-0.2ex}O\hspace{-0.06ex}I}}}\xspace, \ensuremath{{\cal{S\hspace{-0.06ex}I\hspace{-0.1ex}F}}}\xspace, and \SOQ knowledge
bases~\cite{GogaczIM18,GogaczGIJM19} are considerably easier to obtain
due to the relatively simple structure of transitive roles. For the
more expressive \SHOIF, the problem becomes
undecidable~\cite{Rudolph16}.  Indeed, to the best of our knowledge,
this paper offers the first positive results on finite entailment of
non-local queries in description logics.

In order to show our main result, we provide a series of intermediate
reductions allowing us to work with simpler variants of the input
logics and query formalisms. The reductions apply to both logics,
requiring sometimes conceptually different proofs for each of
them. Our proofs encompass different techniques. We use unravelling
operations to establish a tree-like model property, i.e.\ to show that
if a query is not entailed by a knowledge base, then there is a
tree-like counter-model. This in turn serves as the basis for
automata-based approaches to finite entailment. We also use the
coloured blocking principle to construct appropriate finite
counter-models out of infinite tree-like counter-models.

\section*{Acknowledgments}

This work was supported by Poland's National Science Centre
grant 2018/30/E/ST6/00042.

\section{Eliminating Multiple Roles}~\label{sec:mulroles}
Moving on with simplifications, we reduce finite entailment of $\ensuremath{\UCQ^\smallplus}\xspace$s
over $\ensuremath{\ALCI^\smallplus}\xspace$ or $\ensuremath{\ALCQ^\smallplus}\xspace$ KBs to the single-role case. More
precisely, we show how to solve one instance of finite entailment by
solving many instances of finite entailment modulo types with
single-role KBs.

Let ${\cal{K}} = ({\cal{T}},{\cal{A}})$ be an $\ensuremath{\ALCI^\smallplus}\xspace$ or $\ensuremath{\ALCQ^\smallplus}\xspace$ KB, $Q \in \ensuremath{\UCQ^\smallplus}\xspace$
and $ m = \max_{q\in Q} |q|$. One can decide if
${\cal{K}}\models_{\mathsf{fin}} Q$ in time $O\big(\mathrm{poly}\big(\|{\cal{K}}\|, 2^{|\mn{CN}({\cal{K}})|\cdot |Q|
  \cdot 4^{m}}\big)\big)$ using
oracle calls to finite entailment modulo
types with single-role KBs of size at most $\mathrm{poly}(\|{\cal{K}}\|,\|Q\|)$,
unions of at most $|Q| \cdot 2^{\mathrm{poly}(m)}$ $\ensuremath{\CQ^\smallplus}\xspace$s of size ${\cal{O}}(m)$,
and type sets of size at most $2^{|\mn{CN}({\cal{K}})|\cdot |Q| \cdot 4^{m}}$;
the KBs inherit their counting threshold and
set of relevant concept names from ${\cal{K}}$.

The argument again relies on unravelling, which allows focusing on
\emph{tree-like} counter-models; that is, ones that can be decomposed
into multiple finite $\Sigma_r$-subinterpretations with
$\Sigma_r=\{r\}\cup\mn{CN}({\cal{K}})$ and $r \in \mn{rol}({\cal{K}})$, called
\emph{bags}, arranged into a (possibly infinite) tree such that:
(1) two bags share a single element if they are neighbours, and are
disjoint if they are not neighbours; (2) each element $d$ occurs in
exactly one $\Sigma_r$-bag for each $r\in \mn{rol}({\cal{K}})$ and \new{some bag
containing $d$ is the parent of all other bags containing $d$}; (3)~the root bag satisfies
${\cal{A}}$. A tree-like interpretation is a model of ${\cal{K}}$ iff each
$\Sigma_r$-bag is a model of the TBox ${\cal{T}}_r$, collecting all CIs from ${\cal{T}}$ that mention
only role name $r$.

Evaluating $Q$ over a tree-like interpretation ${\cal{I}}$ can be
distributed over bags by means of \emph{$Q$-labellings}, which assign
to each element its \emph{(unary) $Q$-type}, summarizing information
relevant for $Q$ as a set of pairs $(p,V)$ where $p$ is a  fragment of
$Q$ and $\new{\emptyset \neq \,} V
\subseteq \textit{var}(p)$. We shall think of a $Q$-labelling as an extension
${\cal{I}}'$ of ${\cal{I}}$ to fresh concept names $A_{p, V}$.
\new{We are interested in $Q$-labellings ${\cal{I}}'$ such that $A_{q,
    V}^{{\cal{I}}'} = \emptyset$ for all $q \in
  Q$ and $\emptyset \neq V \subseteq \textit{var}(q)$;
  we call them \emph{$Q$-refutations}.}
We call ${\cal{I}}'$ \emph{correct} if $e \in A_{p, V}^{{\cal{I}}'}$ iff $\eta(V)
= \{e\}$ for some match $\eta$ for $p$ in ${\cal{I}}'$. We call ${\cal{I}}'$
\emph{consistent} if each bag satisfies the following: for each
partition of a fragment $p'$ into fragments $p, p_1, p_2, \dots, p_k$
with $\textit{var}(p_i)\cap \textit{var}(p_j) = \emptyset$ for $i\neq j$, $V_i =
\textit{var}(p_i) \cap \textit{var}(p)$, and $\new{\emptyset \neq} \;V\subseteq
\textit{var}(p)$, there is no match $\eta$ for $p$ in the bag such that
$\eta(V_i) = \{e_i\} \subseteq A_{p_i, V_i}^{{\cal{I}}'}$ for all $i$ but
$\eta(V) = \{e\} \not\subseteq A_{p', V}^{{\cal{I}}'}$.

\begin{lemma} \label{lem:multirolesconsistent}
  \new{The correct $Q$-labelling of ${\cal{I}}$ is a
  $Q$-refutation iff ${\cal{I}}$ admits a consistent $Q$-refutation.}
\end{lemma}

It remains to show how to find consistent \new{$Q$-refutations ${\cal{J}}$ such
that ${\cal{J}} \models {\cal{K}}$} and prove that they can be turned into finite
counter-models.

\new{Consistent $Q$-refutations} can be recognized by a tree
automaton but there are two obstacles. First, bags are finite, but arbitrarily
large, so tree-like interpretations do not naturally encode as
finitely-labelled trees. Second, the information that needs to be
passed between bags is the unary type of the shared element, and the
unary type of the element shared with the parent bag needs to be
related with the \emph{set of unary types} of elements shared with
child bags. As the number of such types is $2^{\mn{CN}({\cal{K}}) \cdot |Q|\cdot
4^{m}}$, this suggests a triply exponential construction. Our response
is to generalize automata to trees over infinite alphabets and avoid
representing the transition relation explicitly.

\begin{definition}
A \emph{(B\"uchi) automaton} ${\cal{B}}= (\Sigma, \Gamma,S, I, F, \delta)$
consists of a \emph{node alphabet} $\Sigma$, an \emph{edge alphabet}
$\Gamma$, a finite set $S$ of \emph{states}, sets $I, F\subseteq S$ of
\emph{initial} and \emph{accepting} states, and a \emph{transition
function} $\delta: S \times \Sigma \to 2^{(\Gamma \times S)^*}$
mapping state-letter pairs to sets of words over the alphabet
$\Gamma\times S$.  A \emph{run} $\rho$ of ${\cal{B}}$ on a tree $T$ maps
nodes of $T$ to $S$ such that $\rho(\varepsilon) \in I$ and for each
node $v$ with children $v_1, v_2, \dots, v_n$,
\[ (\gamma_1, \rho(v_1)) (\gamma_2, \rho(v_2)) \dots (\gamma_n,
  \rho(v_n))  \in  \delta (\rho(v), \sigma) \,,\]
where $\gamma_i$ is the label of the edge $(v, v_i)$ and $\sigma$ is
the label of the node $v$. A tree $T$ is \emph{accepted} by ${\cal{B}}$ if
for some run $\rho$, each branch of $T$ contains infinitely many
nodes from $\rho^{-1}(F)$. All trees accepted by
${\cal{B}}$ form the set \emph{recognized} by ${\cal{B}}$.
\end{definition}

Let us build an automaton ${\cal{B}}_{{\cal{K}}, Q}$ recognizing \new{consistent
$Q$-refutations}. Because the state space is finite, the automaton
cannot compute which elements are shared between bags: it must be
given this information. We provide it by marking in each bag the
element shared with the parent bag and displaying the shared element
on the edge to the parent.  With that, the actual elements used in the
bags do not matter any more: the element on the edge between bags
indicates the element of the parent bag that should be identified with
the marked element of the child bag. Let $\Delta$ be a countably infinite
set. The node alphabet is the set of finite
$\Sigma_r$-interpretations for $r\in\mn{rol}({\cal{K}})$ with domains contained
in $\Delta$, and the edge alphabet is $\Delta$. States consist of
$r\in\mn{rol}({\cal{K}})$ and a unary type $\tau$ that includes no $A_{q, V}$
with $q \in Q$.  A state $(r, \tau)$ is initial if $\tau \supseteq \{A
\bigm | A(a) \in {\cal{A}}\}$ where $\{a\} = \mn{ind}({\cal{K}})$.  All states are
accepting. The transition function ensures that the input tree
represents a tree-like interpretation and that each $\Sigma_r$-bag is
a model of ${\cal{T}}_r$ and satisfies the consistency condition.

Our automata are infinite objects, but in the oracle model their
emptiness can be tested in $\ensuremath{\textsc{PTime}}\xspace$ (see Appendix B).

\begin{fact} \label{fact:emptiness}
  There is a polynomial-time algorithm with an oracle that, for each
 automaton ${\cal{B}} = (\Sigma, \Gamma, S, I, F, \delta)$, accepts input
 $(S, I, F)$ with oracle $\mathsf{step}_{\cal{B}}$ iff ${\cal{B}}$ accepts some tree, where
 $\mathsf{step}_{\cal{B}}$ is the set of pairs $(P, q) \in 2^S\times S$ such that
 $\delta(q, \sigma) \cap (P\times \Gamma)^* \neq \emptyset$  for
 some $\sigma \in \Sigma$.
\end{fact}

Deciding if $\big(P, (r, \tau)\big) \in \mathsf{step}_{{\cal{B}}_{{\cal{K}},Q}}$ reduces
to a single instance of finite entailment modulo types, for
${\cal{K}}'=({\cal{T}}_r, {\cal{A}}_\tau)$ where ${\cal{A}}_\tau$ encodes $\tau$ as a set of
assertions on some distinguished individual, $Q'$ obtained, informally
speaking, by taking the union of all matches forbidden in the
consistency condition, and $\Theta'=\big \{ \tau \bigm | \forall \,
r\in\mn{rol}({\cal{K}})\; (r, \tau) \in P \cup (r, \tau)\big\}$. Hence, applied
to ${\cal{B}}_{{\cal{K}}, Q}$, Fact~\ref{fact:emptiness} yields the desired
bounds.

\smallskip
To get finite counter-models we use coloured blocking.
For $d \in\Delta^{\cal{I}}$, the \emph{$n$-neighbourhood $N_n^{{\cal{I}}}(d)$ of
$d$} is the interpretation obtained by restricting ${\cal{I}}$ to elements
$e \in \Delta^{\cal{I}}$ within distance $n$ from $d$ in ${\cal{I}}$, enriched
with a fresh concept interpreted as $\{d\}$.
A \emph{colouring of ${\cal{I}}$ with $k$ colours} is an
extension ${\cal{I}}'$ of ${\cal{I}}$ to $k$ fresh concept names $B_1, \dots, B_k$
such that $B_1^{{\cal{I}}'}, \dots, B_k^{{\cal{I}}'}$ is a partition of
$\Delta^{{\cal{I}}'} = \Delta^{{\cal{I}}}$. We say that
$d \in B_i^{{\cal{I}}'}$ has colour $B_i$. We call ${\cal{I}}'$
\emph{$n$-proper} if for each $d \in \Delta^{{\cal{I}}'}$
all elements of $N_n^{{\cal{I}}'}(d)$ have different colours.

\begin{fact}[\citeauthor{GogaczIM18} \citeyear{GogaczIM18}]
  \label{fact:coloured-blocking}
If ${\cal{I}}$ has bounded degree, then for all $n\geq 0$ there exists an
$n$-proper colouring ${\cal{I}}'$ of ${\cal{I}}$ with finitely many colours.
Consider interpretation ${\cal{J}}$ obtained from ${\cal{I}}'$ by redirecting some
edges such that the old target and the new target have
isomorphic $n$-neighbourhoods in ${\cal{I}}'$. Then, for each $q \in \ensuremath{\mathcal{C\hspace{-0.25ex}Q}}\xspace$
with at most $\sqrt{n}$ binary atoms, if ${\cal{I}}\centernot\models q$, then
${\cal{J}}\centernot\models q$.
\end{fact}

From the proof of Fact~\ref{fact:emptiness} it also follows that if
${\cal{B}}$ accepts some tree, then it also accepts a \emph{regular} tree;
that is, a tree that has only finitely many non-isomorphic
subtrees. Each regular tree has bounded branching and uses only
finitely many different labels.  Consequently, the tree-like
counter-model ${\cal{I}}$ corresponding to a regular tree accepted by
${\cal{B}}_{{\cal{K}}, Q}$ uses finitely many different bags (up to isomorphism),
which means that their size is bounded by some $k$. Therefore,
${\cal{I}}$ has bounded degree and, because $\Sigma_r$-bags are disjoint,
the length of simple directed $r$-paths in ${\cal{I}}$ is also bounded by
$k$.

For $\ell = 2k$, let  $Q^{(\ell)}$ be obtained from $Q$ by replacing
each transitive atom $r^*(x, y)$ with the disjunction
\[ x=y \lor r(x,y) \lor \bigvee_{1<i\leq \ell} r^i(x, y)\, , \] where
$r^i(x, y)$ expresses the existence of an $r$-path of length $i$ from
$x$ to $y$ as $r(x, z_1) \land r(z_1, z_2) \land \dots \land
r(z_{i-1}, y)$ for fresh variables $z_1, \dots, z_{i-1}$. Rewrite
$Q^{(\ell)}$ as a $\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$ and let $t$ be the maximal number of binary
atoms in one $\ensuremath{\mathcal{C\hspace{-0.25ex}Q}}\xspace$ in $Q^{(\ell)}$.

\begin{fact} \label{fact:bounded}
If each simple directed $r$-path in an interpretation ${\cal{J}}$ has length
at most $\ell$, then $\Jmc \models Q$ iff $\Jmc \models Q^{(\ell)}$.
\end{fact}

Fix $n = t^2$ and let ${\cal{I}}'$ be an $n$-proper colouring of ${\cal{I}}$. On
each infinite branch, select the first $\Sigma_r$-bag ${\cal{M}}$ such that
for some $\Sigma_r$-bag ${\cal{M}}'$ higher on this branch, the
$n$-neighbourhood of the element $e$, shared by ${\cal{M}}$ and its parent, is
isomorphic to the $n$-neighbourhood of the element $e'$, shared by
${\cal{M}}'$ and its parent. The set of selected bags forms a maximal
antichain, and by K\"onig's Lemma, it is finite. Let ${\cal{F}}$ be the
interpretation obtained by taking the union of all strict ancestors of
the selected bags, and for each element $e$ shared by a selected
$\Sigma_r$-bag and its parent, redirect each $r$-edge incident with
$e$: instead of pointing at an $r$-neighbour of $e$, it should point
at the corresponding $r$-neighbour of $e'$. If ${\cal{K}}$ is an $\ensuremath{\ALCQ^\smallplus}\xspace$
KB, redirect only outgoing $r$-edges, and drop the incoming
ones. Multiple nodes $e$ may be attached to the same bag ${\cal{M}}'$ in
this way, but they are only $r$-reachable from each other via elements
of ${\cal{M}}'$, so any simple $r$-path in ${\cal{F}}$ has length bounded by $2k =
\ell$.  It is routine to check that ${\cal{F}}\models {\cal{K}}$. By
Fact~\ref{fact:coloured-blocking}, ${\cal{F}} \not\models Q^{(\ell)}$;
by Fact~\ref{fact:bounded}, ${\cal{F}} \not\models Q$. Thus, ${\cal{F}}$ is
a finite counter-model.

\section{Eliminating Nominals, Trivializing ABoxes}
\label{sec:ABoxesNomMain}

Finite entailment of a $\ensuremath{\UCQ^\smallplus}\xspace$ over an $\ensuremath{\ALCOI^\smallplus}\xspace$ or $\ensuremath{\ALCOQ^\smallplus}\xspace$ KB can
be reduced to multiple instances of finite entailment of $\ensuremath{\UCQ^\smallplus}\xspace$s over
$\ensuremath{\ALCI^\smallplus}\xspace$ or $\ensuremath{\ALCQ^\smallplus}\xspace$ KBs, respectively, with \emph{trivial} ABoxes;
the latter means that ABoxes mention only one individual (with a
fully specified unary type) and contain no binary assertions.
Concluding complexity bounds for $\ensuremath{\ALCOI^\smallplus}\xspace$ or $\ensuremath{\ALCOQ^\smallplus}\xspace$ from bounds
for $\ensuremath{\ALCI^\smallplus}\xspace$ or $\ensuremath{\ALCQ^\smallplus}\xspace$ requires precise estimations of the number of
these instances and their parameters. The key parameters are the size
of the KB, the number of $\ensuremath{\CQ^\smallplus}\xspace$s in the query, and their size.

Consider an $\ensuremath{\ALCOI^\smallplus}\xspace$ or $\ensuremath{\ALCOQ^\smallplus}\xspace$ KB ${\cal{K}}$ and $Q \in \ensuremath{\UCQ^\smallplus}\xspace$ with
$\ensuremath{\CQ^\smallplus}\xspace$s of size at most $m$. Then, the reduction gives an at
most doubly exponential number of instances, with KBs of size at most
$\mathrm{poly}(\|{\cal{K}}\|, N^{1+|\mn{RCN}({\cal{K}})|})$ and queries with at most
$|Q| \cdot \big(\|{\cal{K}}\|\cdot N^{|\mn{RCN}({\cal{K}})|}\big)^{O(m)}$
$\ensuremath{\CQ^\smallplus}\xspace$s of size $O(m)$. Importantly, the reduction preserves the counting
threshold $N$ and the set $\mn{RCN}({\cal{K}})$ of relevant concept names.

Let us sketch the argument. Using routine one-step unravelling one can
show that for $\ensuremath{\ALCOI^\smallplus}\xspace$ it suffices to search for counter-models ${\cal{I}}$
that can be decomposed into domain-disjoint interpretations
${\cal{I}}\upharpoonright \mn{ind}({\cal{K}})$ and ${\cal{I}}_1, \dots, {\cal{I}}_n$ for some $n
\leq |{\cal{K}}| \cdot |\mn{ind}({\cal{K}})|$ with two kinds of additional edges:
arbitrary edges connecting elements from $\bigcup_i\Delta^{{\cal{I}}_i}$
with elements from $\mn{nom}({\cal{K}})$, and a single edge connecting a
distinguished element $d_i\in\Delta^{{\cal{I}}_i}$ with a corresponding
element $e_i \in \mn{ind}({\cal{K}})$ for each $i\leq n$. Iterating over
possible ${\cal{I}}\upharpoonright \mn{ind}({\cal{K}})$, we check if there exist
${\cal{I}}_i$ that \new{are compatible with}
${\cal{K}}$, provide witnesses for elements from
$\mn{ind}({\cal{K}})$, and avoid satisfying the query. The properties required
for a single ${\cal{I}}_i$ can be encoded as a finite entailment problem for
a modified KB whose ABox describes the unary type of $d_i$, and a
union of selected fragments of $Q$ with some variables
substituted by elements of $\{d_i\} \cup \mn{nom}({\cal{K}})$. By representing
the existence of an $r$-edge to $a\in \mn{nom}({\cal{K}})$ with a fresh concept
name $A_{\exists r.\{a\}}$, suitably axiomatized, we can eliminate
nominals from the KB and from the query.

For $\ensuremath{\ALCOQ^\smallplus}\xspace$, unravelling is made harder by at-most restrictions over
closures of roles. We shall treat in a special way all successors of
elements from $\mn{ind}({\cal{K}})$ that are affected by such at-most
restrictions. Let us call an $r$-successor $e$ of $d \in \Delta^{\cal{I}}$
\emph{directly $r$-relevant} if $e\in A^{\cal{I}}$ for some $A$ relevant for
$d$ with respect to $r$, and let $\mn{rel}_r^{\cal{I}}(d)$ be the set of all \emph{$r$-relevant
successors} of $d$; that is, the least set containing all directly
$r$-relevant successors of $d$ and closed under directly $r$-relevant
successors. The key insight is that this set has bounded size.

\begin{fact}[\citeauthor{GuIbJu-AAAI18} \citeyear{GuIbJu-AAAI18}]  \label{fact:relevant}
  If $N$ is the counting threshold in ${\cal{K}}$ and
  ${\cal{I}} \models {\cal{K}}$, then   $|\mn{rel}_r^{\cal{I}}(d)|\leq
  N^{|\mn{RCN}({\cal{K}})|}$ for all $d\in\Delta^{\cal{I}}$ and  $r \in \mn{rol}({\cal{K}})$.
\end{fact}

\noindent In the argument for $\ensuremath{\ALCOI^\smallplus}\xspace$, we replace $\mn{ind}({\cal{K}})$ with
\[\mn{ind}({\cal{K}}) \cup \bigcup \big \{ \mn{rel}^{\cal{I}}_r(a) \bigm| {r \in
      \mn{rol}({\cal{K}})}, {a \in \mn{ind}({\cal{K}})}\big\}\,,\]
and similarly for $\mn{nom}({\cal{K}})$.
Appendix A has full details.

In the following sections we shall focus on the decision
procedures for $\ensuremath{\ALCI^\smallplus}\xspace$ and $\ensuremath{\ALCQ^\smallplus}\xspace$, but to ensure that they give
$\ensuremath{\textsc{2ExpTime}}\xspace$ upper bounds for $\ensuremath{\ALCOI^\smallplus}\xspace$ and $\ensuremath{\ALCOQ^\smallplus}\xspace$ when combined
with the reductions above, we will need more careful complexity analysis.

\section{Eliminating nominals and complex ABoxes [draft]}~\label{sec:ABoxesNomMain}
Finite entailment of a \ensuremath{\UCQ^\smallplus}\xspace $Q$ by an $\ensuremath{\ALCOI^\smallplus}\xspace$ (resp. $\ensuremath{\ALCOQ^\smallplus}\xspace$) KB ${\cal{K}}$ can be reduced to multiple instances of the problem of finite entailment of a $\ensuremath{\UCQ^\smallplus}\xspace$ by an $\ensuremath{\ALCI^\smallplus}\xspace$ (resp. $\ensuremath{\ALCQ^\smallplus}\xspace$) KB.
Moreover, in these instances, the knowledge base can be assumed to have a trivial ABox (i.e. consisting of one individual with fully specified unary type).
The reduction does not introduce new role names\nb{right now not true for \ensuremath{\ALCOI^\smallplus}\xspace; should be easy to change, but also: we don't need it for \ensuremath{\ALCOI^\smallplus}\xspace}.

As we use this result several times \comment{(twice? thrice?)} and depend on the detailed complexity bounds, we state it as an algorithmic result for several different cases, providing for each of them:
\begin{itemize}
 \item the number of instances to which we reduce;
 \item three bounds on the sizes of these instances:
 \begin{itemize}
   \item size of the KB;
   \item number of disjuncts in the query (call it \emph{query length}(?));
   \item size of the largest disjunct in the query \comment{(number of atoms? variables? binary atoms?)} (call it \emph{query width}(?)).
 \end{itemize}
\end{itemize}

Let ${\cal{K}}$ be an \ensuremath{\ALCOI^\smallplus}\xspace or \ensuremath{\ALCOQ^\smallplus}\xspace KB and $Q$ be a \ensuremath{\UCQ^\smallplus}\xspace with $n$ disjuncts, each of size at most $m$.

\begin{itemize}
 \item If ${\cal{K}}$ is an \ensuremath{\ALCOI^\smallplus}\xspace KB, there is an exponential (in $|{\cal{K}}|$) number of instances, with size of the KB polynomial in $|{\cal{K}}|$, query length $O(|{\cal{K}}|^n)$ and query width at most $3m$.
 \item If ${\cal{K}}$ is an \ensuremath{\ALCOQ^\smallplus}\xspace KB, there is a double exponential (in $|{\cal{K}}|$) number of instances, with size of the KB exponential in $|{\cal{K}}|$, query length $O(2^{n|{\cal{K}}|})$ and query width at most $3m$. \todo{verify}
 \item If ${\cal{K}}$ is an \ensuremath{\ALCOQ^\smallplus}\xspace KB without long at-most restrictions and all but one nominal having guaranteed no outgoing edges, there is an exponential (in $|{\cal{K}}|$) number of instances, with size of the KB polynomial in $|{\cal{K}}|$, query length $O(|{\cal{K}}|^n)$ and query width at most $3m$. \todo{verify, specify the conditions}
\end{itemize}

For the full proof, see Appendix.
The main ideas of the reduction for \ensuremath{\ALCOI^\smallplus}\xspace:
\begin{itemize}
 \item axiomatization of concepts $C_{\exists r. A} \equiv \exists r. A$ and $C_{\exists r\refltrans. A} \equiv \exists r\refltrans. A$ for all concepts $A$ from the original KB;
 \item after fixing the unary types of the nominals, the query can be modified to not use nominals; thus, it stays mostly the same in the instances;
 \item we want to create a set of KBs ${\cal{K}}_i$; each KB corresponds essentially to a guess of the properties of the nominals and their neighbourhoods \comment{(court?)} (unary types, connections between them);
 \item for each model of ${\cal{K}}$, there is a model of some ${\cal{K}}_i$ being the same, but with the nominals removed (and enriched with some concept names).
\end{itemize}
For \ensuremath{\ALCOQ^\smallplus}\xspace similarly, but handling the number restrictions along the way; the crucial observation is that there is a bounded number of relevant successors of the nominals; thus, we can treat them all as nominals too; to get good complexity and a trivial ABox, we need one-step unravelling of the nominals.

\section{Plan of Attack}

Our main technical contribution are the following results.

\begin{theorem}\label{thm:LoweBound}
 Finite entailment of $\ensuremath{\UCQ^\smallplus}\xspace\!$s over \ensuremath{\ALCOI^\smallplus}\xspace or \ensuremath{\ALCOQ^\smallplus}\xspace knowledge bases is \ensuremath{\textsc{2ExpTime}}\xspace-complete.
 \end{theorem}
To prove upper bounds, we will show a series of reductions that will
allow us to deal at the end with a base case where   the query is a
plain UCQ and the knowledge base is `single-role ABox-trivial'  either
in $\ensuremath{\ALCI^\smallplus}\xspace$ or in $\ensuremath{\ALCQ^\smallplus}\xspace$ without at-most restrictions over closures
of roles. These reductions can be seen as different phases in  our
decision procedure, each of them depending on the previous one.

\medskip \noindent {\bf I.}
We start by showing in Section~\ref{sec:ABoxesNomMain} that one can eliminate nominals from the input knowledge bases, i.e.\ roughly,  that one can reduce finite entailment of $\ensuremath{\UCQ^\smallplus}\xspace\!$s over  \ensuremath{\ALCOI^\smallplus}\xspace or \ensuremath{\ALCOQ^\smallplus}\xspace KBs to \ensuremath{\ALCI^\smallplus}\xspace or \ensuremath{\ALCQ^\smallplus}\xspace KBs, respectively. We further show that the input ABox can be assumed to be `trivial' in the sense that it contains no role assertions and that only one individual name occurs in it.

\smallskip \noindent {\bf II.}
In Section~\ref{sec:mulroles} we show that the variants obtained in Step I above can be further reduced to the case where the knowledge base contains a single role name. This is in line with seeing \ensuremath{\ALCQ^\smallplus}\xspace and \ensuremath{\ALCI^\smallplus}\xspace as a fusion of logics~\cite{BaaderLSW02}, where the interaction between different roles is limited. In a nutshell, we show
that there exists a finite counter-model if and only if there exists a tree-like counter-model accepting a decomposition into components interpreting a single role name.

\smallskip \noindent {\bf III.}
In Section~\ref{sec:elim-trans}, assuming  single-role ABox-trivial $\ensuremath{\ALCI^\smallplus}\xspace$ or
$\ensuremath{\ALCQ^\smallplus}\xspace$  KBs, we eliminate transitive closure from queries and from at-most
restrictions. This  step is the one requiring  the most technical
effort. We will develop the notion of hybrid decompositions, which are
tree decompositions that associate with each node arbitrarily large
interpretations, but have a certain more subtle parameter bounded.
We will observe special characteristics of these interpretations that
allow us to establish structural restrictions between neighbouring nodes
in the decomposition.  Roughly, the key result will be  that finite
counter-models can be unravelled  into  counter-models  admitting  a
hybrid decomposition with the above features. This tree-like model
property will then be the basis for automata-based approaches to
finite entailment in this setting.

\smallskip \noindent {\bf IV.}
 Section~\ref{sec:basecase}  provides a decision procedure for the base case described above.  We will  rely again on tree unravelling and automata-based techniques.

\smallskip
For the matching lower bound, we show the following.

\begin{theorem}
 Finite entailment of  $\ensuremath{\CQ^\smallplus}\xspace\!$s over \ALC knowledge bases is \ensuremath{\textsc{2ExpTime}}\xspace-hard.
 \end{theorem}
 %
The proof is  by reducing the word problem of exponentially space
bounded alternating Turing machines,  which is known to be
\ensuremath{\textsc{2ExpTime}}\xspace-hard~\cite{chandraAlternation1981}. The encoding is a direct
adaptation of the one used to show that (arbitrary) entailment of CQs
over $\mathcal{SH}$ knowledge bases is \ensuremath{\textsc{2ExpTime}}\xspace-hard~\cite{EiterLOS09},
but use $\ensuremath{\CQ^\smallplus}\xspace\!$s to compensate for the weaker logic.

\section{Preliminaries}\label{sec:preli}

\subsection{Description Logics}

We consider a vocabulary consisting of countably infinite disjoint
sets of \emph{concept names} $\concepts$,
\emph{role names} $\roles$, and \emph{individual names} $\mn{N_I}$.
A \emph{role} is a role name  or an \emph{inverse role} $r^-$.
The \emph{(transitive-reflexive) closure} of a role $r$ is
$r^*$. \emph{$\ensuremath{(\ALCOIQfwd)^\smallplus}\xspace$-concepts $C,D$} are defined by the grammar
\[
  C,D ::= A
  \mid \neg C
  \mid C \sqcap D
  \mid \{a\}
  \mid \exists s. C
  \mid \qnrleq n {s'} C
\]
where $A \in \mn{N_C}$, $s$ is a role or the closure of a role, $n
\geq 0$ is a natural number given in binary, and $s'$ is a role name or
the closure of a role name.  We will use $\qnrgeq n {s'} C$ as
abbreviation for $\neg \qnrleq {n{-}1} {s'} C$, together with standard
abbreviations $\bot$, $\top$, $C\sqcup D$, $\forall s.C$.
Concepts of the form $\qnrleq n  {s'}  C $, $\qnrgeq n {s'} C$,
and $\{a\}$ are called
\emph{at-most restrictions}, \emph{at-least restrictions},
and \emph{nominals}, respectively. Note that in
$\ensuremath{(\ALCOIQfwd)^\smallplus}\xspace$-concepts, \emph{inverse roles} are not allowed in
at-most and at-least restrictions.

An \emph{$\ensuremath{(\ALCOIQfwd)^\smallplus}\xspace$-TBox \Tmc} is a finite set of \emph{concept
inclusions (CIs)} $C\sqsubseteq D$, where $C,D$ are
$\ensuremath{(\ALCOIQfwd)^\smallplus}\xspace$-concepts.  An \emph{ABox} $\Amc$ is a finite non-empty
set of \emph{concept} and \emph{role assertions} of the form $A(a)$,
$r(a,b)$, $r^*(a,b)$ where $A \in \mn{N_C}$, $r \in \mn{N_R}$ and
$\{a,b\} \subseteq \mn{N_I}$.
 A \emph{knowledge base (KB)} is a pair
${\cal{K}}=({\cal{T}}, {\cal{A}})$. We write $\mn{CN}({\cal{K}})$, $\mn{rol}({\cal{K}})$, $\mn{nom}({\cal{K}})$, and
$\mn{ind}({\cal{K}})$ for, respectively, the set of \emph{all concept names,
role names, nominals, and individuals occurring in ${\cal{K}}$}. The
\emph{counting threshold} of ${\cal{K}}$ is one plus the greatest number
used  in ${\cal{K}}$.  We let $\|{\cal{K}}\|$ be the total size of the
representation of ${\cal{K}}$.

Sublogics of $\ensuremath{(\ALCOIQfwd)^\smallplus}\xspace$ are defined by forbidding any subset of the
following features: nominals (${\cal{O}}$), inverse roles (${\cal{I}}$), counting
(${\cal{Q}}$), and closure of roles ($^\smallplus$); this is indicated by dropping
corresponding letter or decoration from the name of the logic. The symbol
$^\shortminus$ indicates restricted interaction between inverse roles
and counting restrictions,  so if either is forbidden,  $^\shortminus$
is also dropped. The focus of this paper is on the logics $\ensuremath{\ALCOI^\smallplus}\xspace$
and $\ensuremath{\ALCOQ^\smallplus}\xspace$, obtained by forbidding counting and inverse roles,
respectively. Other sublogics of $\ensuremath{(\ALCOIQfwd)^\smallplus}\xspace$, in particular
$\ensuremath{(\ALCIQfwd)^\smallplus}\xspace$, are used to uniformize and share fragments of
arguments.

\subsection{Interpretations}

The semantics is given as usual via \emph{interpretations} $\Imc =
(\Delta^\Imc, \cdot^\Imc)$ consisting of a non-empty \emph{domain}
$\Delta^\Imc$ and an \emph{interpretation function $\cdot^\Imc$}
mapping concept names to subsets of the domain and role names to
binary relations over the domain. Further, we adopt the \emph{standard
name assumption}, i.e., $a^\Imc=a$ for all $a \in \mn{N_I}$.  The
interpretation of complex concepts $C$ is defined in the usual
way~\cite{DLBook}. An interpretation $\Imc$ is a
\emph{model of a TBox \Tmc}, written $\Imc\models\Tmc$ if
$C^\Imc\subseteq D^\Imc$ for all CIs $C\sqsubseteq D\in \Tmc$.  It is
a \emph{model of an ABox \Amc}, written $\Imc\models \Amc$, if $a\in
A^\Imc$ for all $A(a)\in \Amc$,  $(a,b)\in r^\Imc$ for all $r(a,b)\in
\Amc$, and $(a,b)\in (r^\Imc)^*$ for all $r^*(a,b)\in \Amc$, where
$ (r^\Imc)^*$ is the usual transitive-reflexive closure of the binary
relation $r^\Imc$. Finally, $\Imc$ is a \emph{model of a KB
${\cal{K}}=({\cal{T}}, {\cal{A}})$}, written $\Imc\models \Kmc$, if ${\cal{I}}\models {\cal{T}}$ and
$\Imc\models {\cal{A}}$.

An interpretation ${\cal{I}}$ is \emph{finite} if $\Delta^{\cal{I}}$ is finite. An
interpretation $\Imc'$ is a \emph{sub-interpretation} of $\Imc$,
written as $\Imc'\subseteq \Imc$, if $\Delta^{\Imc'}\subseteq
\Delta^\Imc$, $A^{\Imc'}\subseteq A^\Imc$, and $r^{\Imc'}\subseteq
r^{\Imc}$ for all $A\in\mn{N_C}$ and $r\in \mn{N_R}$. For $\Sigma
\subseteq \concepts \cup \roles$, ${\cal{I}}$ is a
\emph{$\Sigma$-interpretation} if $A^{\cal{I}}=\emptyset$ and
$r^{\cal{I}}=\emptyset$ for all $A\in \concepts \setminus \Sigma$ and $r\in
\roles\setminus\Sigma$. The \emph{restriction of $\Imc$ to signature
$\Sigma$} is the maximal $\Sigma$-interpretation $\Imc'$ with
$\Imc'\subseteq \Imc$. The \emph{restriction of $\Imc$ to domain
$\Delta$}, written ${\cal{I}}\upharpoonright \Delta$, is the maximal
sub-interpretation of $\Imc$ with domain $\Delta$. The union ${\cal{I}} \cup
{\cal{J}}$ of ${\cal{I}}$ and ${\cal{J}}$ is an interpretation such that $\Delta^{{\cal{I}}
\cup {\cal{J}}} = \Delta^{{\cal{I}}} \cup \Delta^{{\cal{J}}}$, $A^{{\cal{I}} \cup {\cal{J}}} =
A^{{\cal{I}}} \cup A^{{\cal{J}}}$, and $r^{{\cal{I}} \cup {\cal{J}}} = r^{{\cal{I}}} \cup r^{{\cal{J}}}$
for all $A\in\mn{N_C}$ and $r\in \mn{N_R}$.

A \emph{homomorphism} from interpretation ${\cal{I}}$ to interpretation
${\cal{J}}$, written as $h : {\cal{I}} \to {\cal{J}}$ is a function $h : \Delta^{\cal{I}} \to
\Delta^{\cal{J}}$ that preserves roles, concepts, and individual names: that
is, for all $r \in \roles$, $(h(d), h(e)) \in r^{\cal{J}}$ whenever $(d,e)
\in r^{\cal{I}}$, for all $A \in \concepts$, $h(d) \in A^{\cal{J}}$ whenever $d
\in A^{\cal{I}}$, and $h(a)= a$ for all $a \in \mn{ind}(\Kmc)$.

\subsection{Queries and Finite Entailment}

Let $\ensuremath{\mn{N_{\mn{V}}}}$ be a countably infinite set of \emph{variables}. An
\emph{atom} is an expression of the form $A(t)$, $t = t'$, $r(t,t')$,
or $r^*(t,t')$ with $A \in\concepts$, $r \in \roles$, and $t,t' \in
\ensuremath{\mn{N_{\mn{V}}}}\cup\ensuremath{\mn{N_{\mn{I}}}}$, referred to as \emph{concept},
\emph{equality}, \emph{role}, and \emph{transitive atoms},
respectively.
A \emph{conjunctive query (with transitive atoms)} is a set of atoms,
understood as the conjunction thereof.  We write
$\ensuremath{\CQ^\smallplus}\xspace$ for conjunctive queries (with transitive atoms), and $\ensuremath{\mathcal{C\hspace{-0.25ex}Q}}\xspace$ for
conjunctive queries without transitive atoms.
Let $\textit{var}(q)$ be the set of variables occurring in the atoms of $q \in \ensuremath{\CQ^\smallplus}\xspace$.
A \emph{match for $q$ in $\Imc$} is a function $\eta:\textit{var}(q)\to
\Delta^{\cal{I}}$ such that ${\cal{I}},\eta\models q$ under the standard semantics
of first-order logic, assuming that the extension of $r^*$ is the
reflexive-transitive closure of the extension of $r$.
An interpretation ${\cal{I}}$ \emph{satisfies} $q$, written ${\cal{I}}\models q$, if
there exists a match for $q$ in ${\cal{I}}$.

Fix $p,q \in \ensuremath{\CQ^\smallplus}\xspace$ and a function $\eta:\textit{var}(p)
\to \ensuremath{\mn{N_{\mn{V}}}} \cup \ensuremath{\mn{N_{\mn{I}}}}$. Let $\eta(p)$ be
obtained from $p$ by substituting each $x\in\textit{var}(p)$ with $\eta(x)$.
We call $\eta$ a \emph{homomorphism} if $\eta(p) \subseteq q^*$, where
$q^*$ is obtained by saturating $q$ as follows for all $r$ and all $s,s' \in \{r, r^*\}$:
if $\{x\,{=}\,y, y\,{=}\,z\} \subseteq q$, add $x\,{=}\,z$,
if $\{s(x,y), y\,{=}\,y'\} \subseteq q$, add $s(x,y')$,
if $\{s(x,y), x\,{=}\,x'\} \subseteq q$, add $s(x',y)$,
if $\{s(x, y), s'(y,z)\} \subseteq q$, add $r^*(x,z)$.
Let ${\cal{I}}\models q$. If there is a homomorphism from $p$ to $q$,
then ${\cal{I}}\models p$. If there is a homomorphism from ${\cal{I}}$ to ${\cal{J}}$,
then ${\cal{J}}\models q$.

A union of conjunctive queries is a finite set of $\ensuremath{\CQ^\smallplus}\xspace$s. We write
$\ensuremath{\UCQ^\smallplus}\xspace$ for unions of conjunctive queries, and $\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$ for unions of
conjunctive queries without transitive atoms.
An interpretation ${\cal{I}}$ satisfies $Q\in\ensuremath{\UCQ^\smallplus}\xspace$, written as ${\cal{I}}\models
Q$, if ${\cal{I}} \models q$ for some $q \in Q$.
A \emph{fragment} of $Q$ is a $\ensuremath{\CQ^\smallplus}\xspace$ formed by a \new{connected}
subset of atoms of some $q \in Q$. We let $\|Q\|$ denote the number of all
fragments of $Q$; note that it is exponential in $\max_{q\in Q} |q|$.

We say that ${\cal{K}}$ \emph{finitely entails} ${\cal{Q}}$, written
${\cal{K}}\models_{\mathsf{fin}} Q$, if each finite model of ${\cal{K}}$ satisfies $Q$. A model
of ${\cal{K}}$ that does not satisfy $Q$ is a \emph{counter-model}.  The
\emph{finite entailment problem} asks if a given KB ${\cal{K}}$ finitely
entails a given query $Q$.

We also consider \emph{finite entailment modulo types}, which allows
more precise complexity bounds.  A \emph{unary ${\cal{K}}$-type} is a subset
of $\mn{CN}({\cal{K}})$ including either $A$ or
$\bar A$ for each $A \in \mn{CN}({\cal{K}})$. Let $\mn{Tp}({\cal{K}})$ be the set of all
unary ${\cal{K}}$-types. For an interpretation ${\cal{I}}$ and an element $d \in
\Delta^{\cal{I}}$, the \emph{unary ${\cal{K}}$-type of $d$ in ${\cal{I}}$} is
$\mn{tp}^{\cal{I}}(d) = \left \{ A \in \mn{CN}({\cal{K}}) \bigm | d \in A^{\cal{I}}\right\}$. We
say that ${\cal{I}}$ \emph{realizes} a unary ${\cal{K}}$-type $\tau$ if $\tau =
\mn{tp}^{\cal{I}}(d)$ for some $d \in \Delta^{\cal{I}}$.  For a KB ${\cal{K}}$, a query $Q$,
and a set of unary types $\Theta \subseteq \mn{Tp}({\cal{K}})$ we write ${\cal{K}}
\models_{\mathsf{fin}}^\Theta Q$ if for each finite interpretation ${\cal{I}}$ that only
realizes types from $\Theta$, if ${\cal{I}}\models {\cal{K}}$ then ${\cal{I}}\models Q$.
In this context, a counter-model is a model of ${\cal{K}}$ that only
realizes types from $\Theta$ and does not satisfy $Q$.

\subsection{Normal Form and Additional Assumptions}

Without loss of generality, we assume throughout the paper that all
CIs are in one of the following \emph{normal forms}:
\begin{align*}

  \bigsqcap_i A_i \sqsubseteq \bigsqcup_j B_j,
  \quad A \sqsubseteq \qnrleq n r B,
  \quad A \sqsubseteq \qnrgeq n r B,
  \\
  \quad A \sqsubseteq \qnrleq n {r^*} B,
  \quad A \sqsubseteq \qnrgeq n {r^*} B,
  \\
  \quad A \sqsubseteq \forall r^-. B,
  \quad A\sqsubseteq \exists r^-.B,
  \quad A\sqsubseteq \exists (r^-)^*.B,
  %
\end{align*}
where $A,A_i,B,B_j$ are concept names or nominals, $r\in \mn{N_R}$,
and empty disjunction and conjunction are equivalent to $\bot$ and
$\top$, respectively. In logics without counting, the number $n$
in at-most restrictions must be 0, and in at-least restrictions it
must be 1.
We also assume that for each concept name $A$ used in ${\cal{K}}$ there is a
\emph{complementary} concept name $\bar A$ axiomatized with CIs $\top
\sqsubseteq A \sqcup \bar A$ and $A \sqcap \bar A \sqsubseteq \bot$.

A concept name $B\in\mn{CN}({\cal{K}})$ is \emph{relevant} if ${\cal{K}}$ contains a
CI of the form $A \sqsubseteq \qnrleq n {r^*} B$ with $n>0$. We let
$\mn{RCN}({\cal{K}})$ denote the set of relevant concept names in ${\cal{K}}$.  A
concept name $B$ is \emph{relevant in ${\cal{I}}$ for $d\in\Delta^{\cal{I}}$ with
respect to $r\in\roles$} if $d \in A^{\cal{I}}$ for some CI $A \sqsubseteq
\qnrleq n {r^*} B$ in ${\cal{K}}$ \new{with $n>0$}. We call ${\cal{K}}$
\emph{sticky} if for each model ${\cal{I}}$ of ${\cal{K}}$, each $r \in \roles$,
and each $d\in\Delta^{\cal{I}}$, all concept names relevant for $d$ with
respect to $r$ are also relevant (with respect to $r$) for each
$r$-successor of $d$. Stickiness of ${\cal{K}}$ can be assumed without loss
of generality:
\new{
for each $B\in\mn{RCN}({\cal{K}})$ and $r
\in \mn{rol}({\cal{K}})$ introduce fresh concept names $B_r$ and $\overline B_r$
axiomatized with $\top \sqsubseteq B_r \sqcup \overline B_r $, $B_r
\sqcap \overline B_r \sqsubseteq \bot$, $B_r \sqsubseteq \qnrleq 0 r
{\overline B_r}$, $B_r \sqsubseteq \qnrleq N {r^*} B$, where $N$ is
the counting threshold in ${\cal{K}}$, and add $A \sqsubseteq B_r$ for each
CI $A \sqsubseteq \qnrleq n {r^*} B$ in ${\cal{K}}$.
}

A variable $y$ is \emph{linking} in $q\in\ensuremath{\CQ^\smallplus}\xspace$ if the only atoms in
$q$ using $y$ are $r^*(x, y), r^*(y, z)$ for some $x, z \in
\textit{var}(q)$. In a match $\eta$ for $q$, $\eta(y)$ can be any node on a
path from $\eta(x)$ to $\eta(z)$. We call $q$ \emph{normalized} if in
every atom over $r^*$ at least one variable is linking, and for every
two atoms $r^*(x, y), r^*(y, z)$ with $y$ linking, exactly one of the
variables $x$ and $z$ is linking too. Each query can be normalized by
first eliminating all linking variables, and then subdividing each
$r^*$ atom into three $r^*$ atoms using two fresh linking variables.
Without loss of generality we can assume that the input
\new{$\ensuremath{\UCQ^\smallplus}\xspace$s consist of normalized connected $\ensuremath{\CQ^\smallplus}\xspace$s}.

\section{Eliminating transtive atoms: \ensuremath{\ALCI^\smallplus}\xspace}
Let ${\cal{K}}$ be an \ensuremath{\ALCI^\smallplus}\xspace KB using only one role, let $Q$ be a \ensuremath{\UCQ^\smallplus}\xspace and let $T$ be a set of forbidden unary types.
We will remove the transitive atoms from the query.

We assume there just one individual.

\subsection{Tree-like structure}
We will be interested in arbitrary models and their tree partitions with the following properties:
\begin{itemize}
 \item each bag is finite;
 \item each (directed) edge between bags has exactly one associated edge in the interpretation;
 \item each edge in the interpretation is either inside one bag or is associated to some edge between bags and connects an element from the parent bag and an element from the child bag (preserving the direction of the edge between the bags);
 \item the root bag contains the individual.
\end{itemize}
We will call it an SCC-partition (as each strongly connected component needs to be inside one bag).
For each element $x$ of the interpretation define $\mn{Bag}(x)$ as the bag in the SCC-partition containing $x$.

\begin{definition}
An interpretation is \emph{safe} if it does not contain an infinite simple directed path.
\end{definition}

We will call a model $\Imc$ along with its SCC-partition a \emph{strong counter-example} if:
\begin{itemize}
 \item $\Imc \models {\cal{K}}$;
 \item $\Imc$ is safe;
 \item $\Imc \not\models Q'$, where $Q'$ is $Q$ with each transitive atom $r\trans(x, y)$ replaced with:
 \[ \bigvee_{x'\in\mn{Bag}(x)} \bigvee_{y'\in\mn{Bag}(y)} r\trans(x', y'). \]
\end{itemize}

\begin{lemma}
There exists a finite counter-model iff there exists a strong counter-example.
\end{lemma}
For the left-to-right implication we will construct a strong counter-example from any finite counter-model by unravelling it appropriately.
For the right-to-left one we will develop a procedure deciding whether there exists a strong counter-example; it will follow that if there is one, there is also one with bounded degree of its SCC-partition and it can be folded back to a finite counter-model.

\subsection{Unravelling}
Let $\Imc$ be a finite counter-model.
We will construct a finite counter-model $\Jmc$ with an SCC-partition (forming a strong counter-example).
There will be a homomorphism $h: \Delta^\Jmc \to \Delta^\Imc$, as each element of $\Jmc$ will be constructed as a copy of some element from $\Imc$.

The root bag contains the ABox along with strongly connected components of the individuals.
Then, for each element $x' \in \Delta^\Jmc$, let $x = h(x')$ (i.e. $x'$ was constructed as a copy of $x$) and consider all edges incident to $x$ in $\Imc$.
If any such edge $(x, y)$ or $(y, x)$ was not yet copied to $\Jmc$ (i.e. there is no copy $y'$ of $y$ such that there is an edge between $x'$ and $y'$), create a fresh copy of $y$ and its strongly connected component in $\Jmc$ and add an edge from $x$ to $y'$ (or an inverse one), where $y'$ is the copy of $y$.
Repeat the above for each element added to $\Jmc$.

Now each bag consists of a single strongly connected component (a copy of an SCC from $\Imc$).
No two adjacent bags can be copies of the same SCC from $\Imc$.
It is easy to verify that ${\cal{K}}$ is satisfied.

$Q$ does not have a match in $\Jmc$, because of the homomorphism $h$.

$\Jmc$ with the declared SCC-partition is a strong counter-example; each bag is an SCC, so the query $Q'$ from the definition of a strong counter-example is equivalent to $Q$; and $\Jmc$ is safe, because any two adjacent bags are copies of different SCCs, so the longest directed path in this tree is bounded by the size of $\Imc$.

\input{sections/UCQplusprocedure}
\input{sections/UCQplusconceptqueries}
\input{sections/UCQplusfold}

\section{Eliminating Transitive Atoms}~\label{sec:elim-trans}
In this section we make the hardest step towards proving our main
result: we reduce finite entailment of $\ensuremath{\UCQ^\smallplus}\xspace$s to finite entailment
of $\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$s, for single-role ABox-trivial KBs either in $\ensuremath{\ALCI^\smallplus}\xspace$ or in $\ensuremath{\ALCQ^\smallplus}\xspace$.
Most of the argument is not only shared for the two DLs, but
works for their common extension $\ensuremath{(\ALCIQfwd)^\smallplus}\xspace$.  Thus, throughout this
section we let ${\cal{K}} = ({\cal{T}},{\cal{A}})$ be a single-role $\ensuremath{(\ALCIQfwd)^\smallplus}\xspace$ KB with
a trivial ABox. We also fix some $Q \in \ensuremath{\UCQ^\smallplus}\xspace$ and a set $\Theta$ of
unary types. The overall strategy
is to show that finite counter-models can be unravelled into safe
counter-models admitting tree decompositions with bags of arbitrary
size, but with a certain more subtle width measure bounded. The bags
of these decompositions will be almost strongly connected, which will
allow dropping transitive atoms when evaluating fragments of $Q$ over
a single bag. Moreover, each bag will contain only a bounded number of
elements relevant for at-most restrictions over closures of roles,
meaning that they can be replaced with nominals (for each bag
separately). This way, the existence of bags that together form a safe
counter-model can be reduced to multiple instances of finite
entailment of $\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$s in $\ensuremath{\ALCOI^\smallplus}\xspace$ or $\ensuremath{\ALCOQ^\smallplus}\xspace$ without at-most
restrictions over closures of roles; eliminating nominals as explained
in Section~\ref{sec:ABoxesNomMain}, one arrives at the base case,
solved in the next section. As the last step, from the existence of
such safe counter-models one infers the existence of finite
counter-models.

Given that we are in the single-role case, we shall be using graph
terminology without mentioning the role name.
In particular, a \emph{source} is an element without incoming edges, a
\emph{sink} is an element without outgoing edges, an
\emph{internal} element is one that has both incoming and outgoing
edges, \new{and an \emph{isolated} element is one that has neither
incoming nor outgoing edges.}

\subsection{Unravelling Finite Counter-Models}

We relax the simplistic notion of decomposition used to eliminate
multiple roles by allowing bags to share additional elements with
their neighbours, provided that the total number of these additional
elements is bounded for each bag.

\begin{definition} [hybrid decomposition] \label{def:hybrid}
A \emph{hybrid decomposition} of an interpretation ${\cal{I}}$ is a
tree $T$ in which each node $v \in T$ is labelled with a finite
interpretation ${\cal{I}}_v = (\Delta_v, \cdot^{{\cal{I}}_v})$, called a
\emph{bag}, a set $\Gamma_v \subseteq \Delta_v$, and an element
$f_v\in \Delta_v$, called the \emph{root} of ${\cal{I}}_v$, such that
\begin{enumerate}
\item \label{item:hybrid-union}
  ${\cal{I}} = \bigcup_{v\in T} {\cal{I}}_v $;
\item \label{item:hybrid-connected}
  for each $e\in\Delta^{\cal{I}}$, $\left \{v \in T \bigm| e \in
    \Delta_v\right\}$ is connected in $T$;
\item \label{item:hybrid-disjoint}
  for each edge $(u,v)$ in $T$,
  $\Delta_u \cap \Delta_v  =  \{f_v\} \cup (\Gamma_u
  \cap \Gamma_v)$.
\end{enumerate}
We let $\widetilde\Gamma_u = \left \{f_v \bigm | v \text{ is a child of }
  u\right\}$ and call $\max_{u\in T} |\Gamma_u|$ the \emph{width} of
$T$.
An element $d\in \Delta_u$ is \emph{fresh} in $u$ if $u$ is the root of
$T$ or $d\notin\Delta_{u'}$ for the parent $u'$ of $u$; $d$ is
\emph{local} in $u$ if $d=f_u$ or if
$d\notin\Delta_v$ for all neighbours $v$ of $u$.
\end{definition}

\noindent We often blur the distinction between the node $v$ and the
interpretation ${\cal{I}}_v$, using the term \emph{bag} for both. Note that
each element is fresh in exactly one bag, and the only local
element in $u$ that is not fresh in $u$ is $f_u$ (unless
$u=\varepsilon$, when $f_\varepsilon$ is fresh too).

While Definiton~\ref{def:hybrid} captures the fundamental structural
simplicity of our counter-models, the limitations of the target
special case impose grittier structural requirements.

\begin{definition}[well-formedness] \label{def:well-formed}
If ${\cal{K}}$ uses both inverses and counting, a hybrid decomposition $T$ is
\emph{well-formed} for ${\cal{K}}$ if ${\cal{I}}_\varepsilon \models {\cal{A}}$ and
for each $u\in T$,
\begin{enumerate}

\item \label{item:types}
  for each concept name $A$, $A^{{\cal{I}}_u} = A^{{\cal{I}}} \cap \Delta_u$;

\item \label{item:roots}
  for each child $v$ of $u$, $f_v$ is a fresh sink or source in
  ${\cal{I}}_u$ \new{(or a fresh element of $\Gamma_u$)};

\item \label{item:external}
  for each fresh sink or source $d$ in ${\cal{I}}_u$ \new{(or fresh $ d\in
    \Gamma_u$)},  $d=f_v$ for exactly one child $v$ of $u$;

\item \label{item:rel-consistent}
  for each $w\in T$, if $f_u \in \Gamma_w$, then $\Gamma_u \subseteq
  \Gamma_w$;

\item \label{item:rel-contained}
  for each local element $d$ in ${\cal{I}}_u$ and each concept name
  $A$ relevant for $d$: if $d \in A^{{\cal{I}}_u}$ then $d\in\Gamma_u$, and
  $\Gamma_v \cap A^{{\cal{I}}_v} \subseteq \Gamma_u$ for all $v\in T$ such
  that $f_v$ is  a sink in ${\cal{I}}_u$ or $f_u$ is a \emph{non-isolated} source in ${\cal{I}}_v$.

\end{enumerate}
If ${\cal{K}}$ does not use inverses, ``sink or source'' in items
\ref{item:roots} and \ref{item:external} is replaced with ``sink'', and
the case ``\new{$f_u$ is a non-isolated source in ${\cal{I}}_v$}'' in item
\ref{item:rel-contained} is dropped, \new{but additionally we require that
each element of $\Gamma_u\setminus \{f_u\}$ is a sink in ${\cal{I}}_u$.}
If ${\cal{K}}$ does not use counting, we additionally require that $\Gamma_u
= \emptyset$ for all $u\in T$.
\end{definition}

\noindent Note that in a well-formed hybrid decomposition, each
element is local in exactly one node.

We work with infinite counter-examples because they have simpler
structure, but ultimately we need to make them finite. The following
notion guarantees that this is possible.

\begin{definition}[safety]
A hybrid decomposition $T$ is \emph{safe} if it admits no infinite
sequence of nodes $u_0, u_1, \dots$ such that for all $i$, either
$f_{u_{i+1}}$ is a sink in ${\cal{I}}_{u_{i}}$ or
$f_{u_i}$ is a \new{non-isolated} source in
${\cal{I}}_{u_{i+1}}$.
\end{definition}

Finally, replacing $\ensuremath{\UCQ^\smallplus}\xspace$ with $\mathcal{UCQ}$ is possible thanks to strong
connectedness guarantees on the bags.

\begin{definition}[well-connectedness]
An interpretation ${\cal{J}}$ is \emph{well-connected} if for all $d, e \in
\Delta^{\cal{J}}$, $(d,e) \in (r^*)^{\cal{J}}$ iff either $d=e$ or $d$ is
not a sink and $e$ is not a source in ${\cal{J}}$.  A hybrid decomposition
$T$ is well-connected if ${\cal{I}}_v$ is well-connected for all $v \in T$.
\end{definition}

In the remainder, by a \emph{${\cal{K}}$-decomposition} we mean a hybrid
decomposition well-formed for ${\cal{K}}$, of width at most
$N^{|\mn{RCN}({\cal{K}})|}$ where $N$ is the counting threshold in ${\cal{K}}$.

\begin{lemma} \label{lem:unravelling}
If ${\cal{K}}\notmodels_{\!\!\mathsf{fin}}^\Theta Q$, then there exists a counter-model admitting a
safe and well-connected ${\cal{K}}$-decomposition.
\end{lemma}

\begin{proof}
Let ${\cal{J}}$ be a finite counter-model. We construct the special
counter-model ${\cal{I}}$ and a witnessing ${\cal{K}}$-decomposition $T$ of ${\cal{I}}$
by unravelling ${\cal{J}}$ in a special way. We describe the construction
for the case when ${\cal{K}}$ uses inverses; if it does not, simply replace
``neighbours'' with ``direct successors''.

Because the ABox of ${\cal{K}}$ is trivial, we have $\mn{ind}({\cal{K}}) = \{d\}$. We
begin from the interpretation ${\cal{I}}_\varepsilon$, obtained from ${\cal{J}}
\upharpoonright \{d\}$ by removing the only possible edge,
$f_\varepsilon = d$, and $\Gamma_\varepsilon = \emptyset$.
Now, roughly, for each previously added element $e$
missing a neighbour, we will be adding a new bag containing $e$ with
all its missing neighbours, along with all other elements from
$\mn{cmp}_{\cal{J}}(e)$---the strongly connected component of $e$ in ${\cal{J}}
\upharpoonright \big(\Delta^{\cal{J}}  \setminus \mn{rel}_{\cal{J}}(e)\big)$, or
$\{e\}$ if $e \in \mn{rel}_{\cal{J}}(e)$---with all their neighbours, and $\mn{rel}_{\cal{J}}(e)$.
If an element $f'$ in this bag corresponds to $f \in \Delta^{\cal{J}}$, we
call $f'$ a \emph{copy of} $f$ and $f$ the \emph{original
of} $f'$. For convenience, we extend this nomenclature to the root
bag: if $f' \in \Delta_\varepsilon$, then its original $f \in
\Delta^{\cal{J}}$ is $f'$ itself; if $f \in \Delta^{\cal{J}}$ belongs to
$\Delta_\varepsilon$, then its copy $f'$ in $\Delta_\varepsilon$ is
$f$ itself. We proceed as follows, as long as there is something to do.

For each previously added node $u$ and each \new{sink or source} $d'
\in \Delta_u$ \new{(or $d'\in\Gamma_u$)} fresh in
$u$,  we add a new child $v$ of $u$. Let
$d\in\Delta^{\cal{J}}$ be the original of $d'$ and let $X \subseteq
\Delta^{\cal{J}}$ be the set of the originals of neighbours of $d'$ in
${\cal{I}}_u$. The interpretation ${\cal{I}}_v$ is obtained by
\begin{itemize}
\item
  taking the restriction of ${\cal{J}}$ to the subdomain comprising
 $\mn{rel}_{\cal{J}}(d)$, $\mn{cmp}_{\cal{J}}(d)$, neighbours of $\mn{cmp}_{\cal{J}}(d) \setminus
 \{d\}$, and neighbours of $d$ that do not belong to $X$;
\item
  removing all edges that are not incident with $\mn{cmp}_{\cal{J}}(d)$ and all
  edges between $d$ and elements from $X$ \new{(if ${\cal{K}}$ does not use
    inverses, drop edges outgoing from $\mn{rel}_{\cal{J}}(d) \setminus \{d\}$)};
\item
  replacing each element $e$ with a fresh copy $e'$, except that for
  elements $e \in \{d\} \cup \mn{rel}_{\cal{J}}(d)$ that already have a copy
  $e'$ in ${\cal{I}}_u$, $e'$ is reused in ${\cal{I}}_v$.
\end{itemize}
We let $f_v = d'$ and $\Gamma_v = \left\{e' \bigm| e \in
\mn{rel}_{\cal{J}}(d)\right\}$.

By construction, $T$ is a hybrid decomposition of width bounded by
$\max_{d \in \Delta^{\cal{J}}} |\mn{rel}_{\cal{J}}(d)| \leq N^{|\mn{RCN}({\cal{K}})|}$
(Fact~\ref{fact:relevant}). It is also not difficult to check that $T$
is safe, well connected, and well formed, and that ${\cal{I}} \models {\cal{K}}$
(see Appendix C).
Moreover, mapping each element of ${\cal{I}}$ to its original in ${\cal{J}}$ gives
a homomorphism from ${\cal{I}}$ to ${\cal{J}}$, which implies that
${\cal{I}} \centernot\models Q$, and that ${\cal{I}}$ only realizes types from $\Theta$.
\end{proof}

\subsection{Evaluating Queries over Unravellings}

We aim at distributing query evaluation over bags, like when
eliminating multiple roles.  This is now harder because bags share
more than one element, but it is possible because the total number of
additional shared elements is bounded for each bag.  These elements
will be \emph{parameters} of $Q$-types.

\begin{definition}[nullary $Q$-types]
  A \emph{(nullary) $Q$-type with parameters $\Gamma$} is a set of
  pairs $(p,\eta)$ where $p$ is a fragment of $Q$ and $\eta$ is a
  partial function from $\textit{var}(p)$ to $\Gamma$.
  The \emph{$Q$-type of ${\cal{J}}$ with parameters $\Gamma$} is the set
  $\mn{tp}_{Q}^{\cal{J}}(\Gamma)$ of pairs $(p, \eta)$ where $p$ is a fragment of
  $Q$, and $\eta$ is a partial function from $\textit{var}(p)$
  to $\Gamma$ that can be extended to a matching for $p$ in ${\cal{J}}$.
\end{definition}

The power of $Q$-types with parameters is
\emph{compositionality}. Consider
interpretations ${\cal{J}}_1,{\cal{J}}_2$ and parameter sets
$\Gamma_1, \Gamma_2$.
If $\Gamma'\subseteq \Gamma_1$, then
\[\mn{tp}^{{\cal{J}}_1}_Q(\Gamma')
  =\mn{tp}^{{\cal{J}}_1}_Q(\Gamma_1) \upharpoonright \Gamma'\,,\]
where
$\tau_1 \upharpoonright \Gamma'  = \left\{(p, \eta \upharpoonright
  \Gamma') \bigm | (p, \eta) \in \tau_1 \right\}$ is the
\emph{projection of $\tau_1$ on $\Gamma' $}.
If $\Delta^{{\cal{J}}_1} \cap \Delta^{{\cal{J}}_2}
\subseteq \Gamma_1 \cap \Gamma_2$, then
\[\mn{tp}^{{\cal{J}}_1 \cup {\cal{J}}_2}_Q(\Gamma_1\cup\Gamma_2)
  = \mn{tp}^{{\cal{J}}_1}_Q(\Gamma_1) \oplus \mn{tp}^{{\cal{J}}_2}_Q(\Gamma_2)\,,\]
where
$\tau_1\oplus\tau_2$ is the \emph{composition} of $\tau_1$ and
$\tau_2$ defined as the set of tuples $(p, \eta)$ such that there
exist $\tau \subseteq \tau_1 \cup \tau_2$ with $\textit{var}(p') \setminus
\dom(\eta')$ pairwise disjoint for $(p',\eta')\in\tau$ and a
homomorphism $\widetilde\eta : p \to \bigcup_{(p',\eta') \in \tau}
\eta'(p')$ extending $\eta$.

Like before, we decorate elements with their $Q$-types.

\begin{definition} [$Q$-labellings]
A \emph{$Q$-labelling} for a ${\cal{K}}$-decomposition $T$ of ${\cal{I}}$ is a
function $\sigma$ that maps each element $d$ local in $u\in T$ to a
$Q$-type $\sigma(d)$ with parameters $\{d\} \cup \Gamma_u$.
We call $\sigma$ \emph{correct} if for each $d$
local in $u$, $\sigma(d)$ is the $Q$-type of $\widehat{\cal{I}}_u$ with
parameters $\{d\} \cup \Gamma_u$, where $\widehat{\cal{I}}_u$ is the
interpretation represented by the subtree of $T$ rooted at $u$.
\end{definition}

If an interpretation ${\cal{I}}$ admits a ${\cal{K}}$-decomposition, then ${\cal{I}}
\centernot\models Q$ iff the correct $Q$-labelling for any
${\cal{K}}$-decomposition of ${\cal{I}}$ uses only $Q$-types in which no $q \in Q$
appears. Such $Q$-labellings, called \emph{$Q$-refutations}, are
what we need to find.

Given a ${\cal{K}}$-decomposition, we can (coinductively) compute the
correct $Q$-labelling bottom-up, by composing and projecting $Q$-types
of the current bag with the $Q$-types of its direct subtrees, as
captured in the following lemma.

\begin{lemma} \label{lem:correct}
\new{The correct $Q$-labelling for a ${\cal{K}}$-decomposition $T$ of an
interpretation ${\cal{I}}$ is the least (pointwise) $Q$-labelling $\sigma$ for $T$ such
that}
\[\sigma(d) = \bigg(
  \mn{tp}^{{\cal{I}}_u}_Q\big(\{d\} \cup \Gamma_u \cup \widetilde\Gamma_u\big)
  \oplus \bigoplus_{e\in \widetilde\Gamma_u} \sigma(e)
  \bigg) \upharpoonright \{d\}\cup\Gamma_u\]
for each node $u \in T$ and each element $d$ local in $u$.
\end{lemma}

\subsection{From $\ensuremath{\UCQ^\smallplus}\xspace$ to $\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$}

The condition in Lemma~\ref{lem:correct} provides the locality
required in automata-based decision procedures, but it still relies on
evaluating $\ensuremath{\UCQ^\smallplus}\xspace$s over bags. We now show how to avoid it.

\begin{definition}[localization]
  A \emph{localization} of a $\ensuremath{\CQ^\smallplus}\xspace$ $q$ is any $\ensuremath{\mathcal{C\hspace{-0.25ex}Q}}\xspace$ obtainable from
  $q$ by replacing each atom $r^* (x,y)$ either with $x=y$ or with
  $r(x,y'), r(x',y)$ for some fresh variables $x'$ and $y'$ used only in
  these two atoms.
\end{definition}

Every matching for a $\ensuremath{\UCQ^\smallplus}\xspace$ $q$ in an interpretation ${\cal{J}}$ extends to
a matching for some localization of $q$. So, if ${\cal{J}}$ does not satisfy
any localization of $q$, then ${\cal{J}}\centernot\models q$.  Moreover, if ${\cal{J}}$
is well-connected, then each matching for a localization of $q$ in
${\cal{J}}$ induces a matching for $q$. So, for well-connected ${\cal{J}}$,
${\cal{J}}\centernot\models q$ iff ${\cal{J}}$ does not satisfy any localization of $q$.

\begin{definition}[weak $Q$-types]
 The \emph{weak $Q$-type of ${\cal{J}}$ with parameters $\Gamma$} is the set
 $\mn{wtp}_Q^{\cal{J}}(\Gamma)$ of pairs $(p, \eta)$ such that $p$ is a fragment
 of $Q$ and $\eta$ is a partial function from $\textit{var}(p)$ to $\Gamma$
 that extends to a matching of some localization of $p$ in ${\cal{J}}$.
\end{definition}

Weak $Q$-types are over-approximations of $Q$-types,
\[\mn{tp}_{Q}^{\cal{J}}(\Gamma) \subseteq \mn{wtp}_{Q}^{\cal{J}}(\Gamma)\,,\]
and are exact for well-connected interpretations,
\[{\cal{J}} \text { is well-connected} \implies \mn{tp}_{Q}^{\cal{J}}(\Gamma)  =
  \mn{wtp}_{Q}^{\cal{J}}(\Gamma)\,.\]

By replacing $Q$-types with weak $Q$-types in the condition of
Lemma~\ref{lem:correct}, we avoid evaluating fragments of $\ensuremath{\UCQ^\smallplus}\xspace$ by
evaluating their localizations instead. We also relax the condition by
replacing equality with inclusion, to facilitate the reduction to
finite (non-)entailment.

\begin{definition} [consistency] \label{def:consistency}
A $Q$-labelling $\sigma$ for a ${\cal{K}}$-decomposition $T$ of an
interpretation ${\cal{I}}$ is \emph{consistent} if
\[\sigma(d) \supseteq \bigg(\mn{wtp}^{{\cal{I}}_u}_Q\big(\{d\} \cup \Gamma_u \cup \widetilde\Gamma_u\big) \oplus
\bigoplus_{e\in \widetilde\Gamma_u} \sigma(e)\bigg) \upharpoonright
\{d\}\cup\Gamma_u\]
for each node $u \in T$ and each element $d$ local in $u$.
\end{definition}

For any ${\cal{K}}$-decomposition $T$, the existence of a consistent
$Q$-refutation implies the existence of a correct
$Q$-refutation. Moreover, if $T$ is well-connected, then the two
conditions coincide, which eliminates false negatives in the finite
entailment decision procedure.

\begin{lemma} \label{lem:consistent}
  If a ${\cal{K}}$-decomposition $T$ of ${\cal{I}}$ admits a consistent
  $Q$-refutation, then it admits a correct $Q$-refutation.
  If $T$ is well-connected, then the correct $Q$-labelling is
  consistent.
\end{lemma}

\begin{proof}
  Let $\sigma$ be the correct $Q$-labelling for $T$. By
  Lemma~\ref{lem:correct} and the relation between $Q$-types and weak
  $Q$-types, for each consistent $Q$-labelling $\sigma'$ for $T$,
  $\sigma(v) \subseteq \sigma'(v)$ for all $v \in T$. Consequently, if
  some consistent $Q$-refutation $\sigma'$ for $T$ exists, then $\sigma$
  is a $Q$-refutation as well. As $\sigma$ is correct, the first claim
  of the lemma follows. If $T$ is well-connected, $Q$-types and weak
  $Q$-types coincide. Combined with Lemma~\ref{lem:correct}, this
  implies that $\sigma$ is consistent.
\end{proof}

\begin{lemma} \label{lem:there}
 If ${\cal{K}}\notmodels_{\!\!\mathsf{fin}}^\Theta Q$ then some model of ${\cal{K}}$ realizing only
 types from $\Theta$ has a safe
 ${\cal{K}}$-decomposition admitting a consistent $Q$-refutation.
\end{lemma}

\begin{proof}
Assume ${\cal{K}}\notmodels_{\!\!\mathsf{fin}}^\Theta Q$. By Lemma~\ref{lem:unravelling},
there exists a counter-model ${\cal{I}}$ with a safe and well-connected
${\cal{K}}$-decomposition $T$. Let $\sigma$ be the unique correct
$Q$-labelling for $T$. Because ${\cal{I}} \centernot\models Q$, $\sigma$ is a
$Q$-refutation.  By Lemma~\ref{lem:consistent}, $\sigma$ is
consistent.
\end{proof}

\subsection{Recognizing Safe Counter-Examples}

We now construct an automaton ${\cal{B}}_{{\cal{K}}, Q}$ recognizing safe
${\cal{K}}$-decompositions of models of ${\cal{K}}$, admitting consistent
$Q$-refutations. Like in the case of multiple roles, we
must give the automaton information about shared elements. For
this purpose, we enrich each node $v$ with a tuple $\tup{g}_v$ enumerating
all elements of $\Gamma_v$ that belong to the parent $u$ of $v$, and
on the edge between $u$ and $v$ we put $f_v$ and $\tup{g}_v$.  Again,
the actual elements in $\Delta_v$ and $\Delta_u$ do not matter:
$f_v$ and $\tup{g}_v$ coupled with the label on the edge from $u$ to $v$
determine which elements represented in $v$ and in $u$ should be
identified. Let $M = N^{|\mn{RCN}({\cal{K}})|}$ where $N$ is the counting
threshold in ${\cal{K}}$. We fix a countably infinite set $\Delta$ and
assume that the node alphabet of our automaton is the set of 4-tuples
of the form $({\cal{J}}, f, \Gamma, \tup{g})$ where ${\cal{J}}$ is a finite
interpretation with $\Delta^{\cal{J}} \subseteq \Delta$, $f \in
\Delta^{\cal{J}}$, $\Gamma \subseteq \Delta^{\cal{J}}$, $|\Gamma| \leq K$, and
$\tup{g}$ is a tuple enumerating a subset of $\Gamma$. The edge alphabet
is $\Delta \times \bigcup_{i=0}^M \Delta^{i}$.

The following lemma relies on ${\cal{K}}$ being expressed either in $\ensuremath{\ALCI^\smallplus}\xspace$
or in $\ensuremath{\ALCQ^\smallplus}\xspace$.
By a base-case KB we understand a single-role KB in $\ensuremath{\ALCI^\smallplus}\xspace$ or
$\ensuremath{\ALCQ^\smallplus}\xspace$, respectively, with a trivial ABox and no at-most
restrictions over closures of roles. Let $m=\max_{q \in Q}|q|$.

\begin{lemma} \label{lem:regularity}
  There exists an automaton ${\cal{B}}_{{\cal{K}},Q,\new{\Theta}}$ recognizing those safe
  ${\cal{K}}$-decompositions of models of ${\cal{K}}$ realizing only types from
  $\Theta$ that admit consistent $Q$-refutations.
  The states, initial states, and accepting states of
  ${\cal{B}}_{{\cal{K}}, Q, \new{\Theta}}$ can be computed in time

  $O\big(2^{\mathrm{poly}( \|Q\|, \|{\cal{K}}\|, M^m)}\big)$.
  The question if $(P,q) \in
  \mathsf{step}_{{\cal{B}}_{{\cal{K}},Q, \new{\Theta}}}$ can be reduced to an instance of finite
  entailment modulo types for a base
  case KB of size at most

  $\mathrm{poly}(\|{\cal{K}}\|, \|Q\|, N\cdot M^m)$
  and counting threshold $N$,
  a $\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$ consisting of at most

  $\|Q\|^2 \cdot M^m \cdot m^m$
  $\ensuremath{\mathcal{C\hspace{-0.25ex}Q}}\xspace$s of size $O(m)$,
  and a type set of size at most

  $|\Theta| \cdot 2^{\mathrm{poly}(\|K\|, \|Q\| , N\cdot M^m)}$.
\end{lemma}

\subsection{Making Counter-Examples Finite}

To complete the proof we need to derive finite non-entailment from the
existence of a safe counter-example.

\begin{lemma} \label{lem:back}
  If ${\cal{K}}$ is in $\ensuremath{\ALCI^\smallplus}\xspace$ or $\ensuremath{\ALCQ^\smallplus}\xspace$ and some model of ${\cal{K}}$
  realizing only types from $\Theta$ has a safe ${\cal{K}}$-decomposition
  admitting a consistent $Q$-refutation, then ${\cal{K}}\notmodels_{\!\!\mathsf{fin}}^\Theta Q$.
\end{lemma}

For $\ensuremath{\ALCQ^\smallplus}\xspace$, a finite counter-model comes for free. Indeed, each safe hybrid
decomposition well-formed for a KB without inverses must be
finite, so the interpretation it represents is finite too.

For $\ensuremath{\ALCI^\smallplus}\xspace$, we use the coloured blocking principle.
By Lemma~\ref{lem:regularity}, the set of those ${\cal{K}}$-decompositions
of models of ${\cal{K}}$ that admit a weakly-consistent $Q$-refutation is
recognized by an automaton. Consequently, if nonempty, it contains a
regular tree $T$; that is, $T$ has only finitely many non-isomorphic
subtrees. From the regularity of $T$ it follows that ${\cal{I}}_v$ are
chosen from a finite set, which means that their size is
bounded. Similarly, the branching of $T$ is bounded. Finally, safety
and regularity of $T$ together imply that there is a bound on the
length of sequence of nodes $u_0, u_1, \dots, u_k$ such that for all
$i<k$, either $f_{u_i}$ is a source in ${\cal{I}}_{u_{i+1}}$ or
$f_{u_{i+1}}$ is a sink in ${\cal{I}}_{u_{i}}$. It follows that in the
interpretation ${\cal{I}}$ represented by $T$, both the branching and the
length of simple directed paths is bounded by some $\ell \in \mathbb{N}$.

By Fact~\ref{fact:bounded}, ${\cal{I}}\models Q$ iff ${\cal{I}}\models
Q^{(\ell)}$, where $Q^{(\ell)} \in \ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$ is the query defined in
Section~\ref{sec:mulroles}. Fix $t = \max_{q \in Q^{(\ell)}} |q|$ and
$n = \max(\ell^2, t^2)$.  Let  ${\cal{I}}'$ be an $n$-proper
colouring of ${\cal{I}}$. Let $V$ be the set of nodes $v \in T$ such that
$f_v$ is a sink in ${\cal{I}}_{v'}$ for the parent $v'$ of $v$ and
$f_{v'}$ is a source in ${\cal{I}}_{v''}$ for the parent $v''$ of $v'$. By
the boundedness properties of $T$, each infinite branch of $T$ has
infinitely many nodes in $V$.  On each infinite branch, select the
first node $v \in V$ with an ancestor $\hat v \in V$ such that the
$n$-neighbourhood of $f_{v}$ is isomorphic with the
$n$-neighbourhood of $f_{\hat v}$. The set of
selected nodes forms a maximal antichain in $T$ and, by K\"onig's
Lemma, it is finite. Let ${\cal{F}}$ be the interpretation obtained by
taking the union of ${\cal{I}}_u$ for $u$ ranging over the nodes of $T$ that
have a selected descendent, except that for each selected node $v$,
$f_{v}$ is removed from the domain and all incoming edges are
redirected to $f_{\hat v}$.

\begin{lemma} \label{lem:folding-correct}
  \new{ The length of simple directed paths in ${\cal{F}}$
   is bounded by $\ell$} and ${\cal{F}} \models {\cal{K}}$.
\end{lemma}

By Fact~\ref{fact:coloured-blocking}, ${\cal{F}} \centernot\models Q^{(\ell)}$,
and by Fact~\ref{fact:bounded} and Lemma~\new{\ref{lem:folding-correct}},
${\cal{F}} \centernot\models Q$.  Thus, ${\cal{F}}$ is a finite counter-model.

\subsection{Wrapping up}

  Assume ${\cal{K}}$ is in $\ensuremath{\ALCI^\smallplus}\xspace$ or $\ensuremath{\ALCQ^\smallplus}\xspace$.
  By Lemmas~\ref{lem:there} and \ref{lem:back}, ${\cal{K}}\notmodels_{\!\!\mathsf{fin}}^\Theta Q$
  iff  some model of ${\cal{K}}$ realizing only types from $\Theta$ has a
  safe ${\cal{K}}$-decomposition admitting a  weakly consistent
  $Q$-refutation.
  Combining Lemma~\ref{lem:regularity} and Fact~\ref{fact:emptiness},
  we get a decision procedure for ${\cal{K}}\models_{\mathsf{fin}}^\Theta Q$ running in time
  $O\big(\mathrm{poly}(|\Theta|)\cdot 2^{\mathrm{poly}( \|Q\|, \|{\cal{K}}\|, M^m)}\big)$ and using oracle calls to finite
  entailment modulo types for instances with parameters bounded as in Lemma~\ref{lem:regularity}.

\section{Base Case}~\label{sec:basecase}
We now solve finite entailment modulo types under the assumptions
justified in previous sections; that is, for $Q$ in $\ensuremath{\mathcal{U\hspace{-0.15ex}C\hspace{-0.25ex}Q}}\xspace$ and a
single-role ABox-trivial ${\cal{K}}$ either in $\ensuremath{\ALCI^\smallplus}\xspace$ or in $\ensuremath{\ALCQ^\smallplus}\xspace$
without at-most restrictions over closures of roles. We show that it
suffices to consider tree-shaped counter-models
(Lemma~\ref{lem:tree-shaped}), and that they consitute an effectively
regular set (Lemma~\ref{lem:reg}).  The decision procedure then
amounts to computing the automaton and testing its emptiness; it runs
in time $\mathrm{poly}(|\Theta|, 2^{\|\ensuremath{{\cal{K}}}\xspace\|^2\cdot\|Q\|})$ where $\Theta$ is the
set of allowed types.

An interpretation ${\cal{J}}$ is \emph{tree-shaped} if its elements can be
arranged into a tree such that the unique $f\in\mn{ind}({\cal{K}})$ is the root
and $r$-edges in ${\cal{J}}$ are allowed only between parents and children;
if ${\cal{K}}$ is an $\ensuremath{\ALCQ^\smallplus}\xspace$ KB, $r$-edges must point down.

\begin{lemma} \label{lem:tree-shaped}
  ${\cal{K}}\notmodels_{\!\!\mathsf{fin}}^\Theta Q$ iff there exists a tree-shaped
  counter-model of bounded degree realizing only types from $\Theta$.
\end{lemma}

\begin{proof}

Let ${\cal{I}}$ be a finite counter-model realizing only types from
$\Theta$.  We get a tree-shaped counter-model ${\cal{I}}'$ by unravelling ${\cal{I}}$
from the unique $f \in \mn{ind}({\cal{K}})$. If ${\cal{K}}$ is in $\ensuremath{\ALCQ^\smallplus}\xspace$, we unravel by
adding fresh copies of all direct successors of previously copied
elements from ${\cal{I}}$. If ${\cal{K}}$ is in $\ensuremath{\ALCI^\smallplus}\xspace$, we add fresh copies of
all direct successors and fresh copies of all direct predecessors. It is
clear that ${\cal{I}}'$ is a tree-shaped counter-model realizing only types
from $\Theta$, of degree bounded by twice the degree of ${\cal{I}}$.

Conversely, let ${\cal{I}}$ be a tree-shaped counter-model of bounded degree
realizing only types from $\Theta$.

If ${\cal{K}}$ is in $\ensuremath{\ALCQ^\smallplus}\xspace$, we enrich ${\cal{I}}$ to ensure that witnesses for
at-least restrictions over $r^*$ are never glued with each other. Note
that in this case all $r$-edges in ${\cal{I}}$ point down. Let $N$ be the
counting threshold in ${\cal{K}}$. For each concept name $A$, introduce
fresh concepts names $A_1, A_2, \dots, A_N$, called the {\em shades}
of $A$.  Extend ${\cal{I}}$ to these concept names in such a way that
$A_1^{\cal{I}}, A_2^{\cal{I}}, \dots, A_N^{\cal{I}}$ form a partition of $A^{\cal{I}}$, and
for each $n \leq N$, if $d\in\Delta^{\cal{I}}$ has at least $n$ successors
in $A$, then it has successors in at least $n$ shades of $A$.
This can be done greedily, by processing ${\cal{I}}$ top down, ensuring that
subtrees rooted at unprocessed nodes use each shade of $A$ at most
once. Take a shallowest unprocessed node $v$. For $n=1, 2, \dots, N$,
if $v$ has at least $n$ descendents in $A$ but only $n-1$ are
painted with a shade of $A$, pick an unpainted one and paint it with
an unused shade of $A$. After the whole tree is processed, paint each
remaining element in $A$ with an arbitrary shade of $A$.

For each concept name $B$ (including the shades) enrich ${\cal{I}}$ further
by introducing a fresh concept name $B'$ with extension $(\exists
r^*.B)^{\cal{I}}$ and add $B' \sqsubseteq \exists r^*.B$ to ${\cal{K}}$; if
${\cal{K}}$ is in $\ensuremath{\ALCI^\smallplus}\xspace$, introduce also $B''$ with extension $(\exists
(r^-)^*.B)^{\cal{I}}$ and add $B'' \sqsubseteq \exists (r^-)^*.B$.
Let $n=\max(2, |Q|^2)$ and let ${\cal{I}}'$ be an $n$-proper colouring of
${\cal{I}}$. Consider a level $l$ in ${\cal{I}}'$ such that all $n$-neighbourhoods
realized in ${\cal{I}}'$ are already realized above $l$. For each element
above level $l$, choose a witness for each CI of the form $A
\sqsubseteq \exists r^* .B$ or $A \sqsubseteq \exists (r^-)^*. B$ in
${\cal{K}}$. Restrict the domain to the nodes above level $l$ and the chosen
witnesses, together with the paths that lead to them. Redirect each
edge leaving the restricted domain to some element above level $l$,
preserving the $n$-neighbourhood.

The only nontrivial thing to check is that at-least restrictions are
not violated, in the case when ${\cal{K}}$ is in $\ensuremath{\ALCQ^\smallplus}\xspace$. For restrictions
over $r$, this is because siblings have different colours in
each $n$-proper colouring, so edges leading to different siblings are
never redirected to the same element. For restrictions over $r^*$,
this is because witnesses for the CI $A_i' \sqsubseteq \exists r^*. A_i$ are
preserved for each shade $A_i$ of $A$.
\end{proof}

\begin{lemma} \label{lem:reg}
  The set of tree-shaped counter-models realizing only types from
  $\Theta$ is recognized by an automaton computable in
  time $2^{O(\|\ensuremath{{\cal{K}}}\xspace\|^2\cdot\|Q\|)}$.

\end{lemma}

This is a routine construction. For $\ensuremath{\ALCQ^\smallplus}\xspace$, the node alphabet is
$\Theta$ and the edge alphabet is trivial. To verify that the input
tree is a model of ${\cal{K}}$, the automaton stores the unary type of the
parent of the current node, and for each $A\in \mn{CN}(\ensuremath{{\cal{K}}}\xspace)$, it stores in
the state the minimum number of elements in $A$ to be found in the
current subtree, together with a binary flag indicating if progress
has been made recently in finding them. This component of the
automaton has $(4\cdot N)^{|\mn{CN}(\ensuremath{{\cal{K}}}\xspace)|}$ states, where $N$ is the
counting threshold in ${\cal{K}}$. Verifying that the input tree does not
satisfy $Q$ involves storing a set of subqueries of CQs from $Q$,
which are not to be satisfied in the current subtree. This component
has $2^{\|Q\|}$ states. The whole automaton is the product of the two
components. It is easy to see that the step relation can be computed
in time polynomial in the number of states.

The case of $\ensuremath{\ALCI^\smallplus}\xspace$ is similar, except that the edge
alphabet is $\{r, r^-\}$ and the first component has separate
information about elements reachable and backwards reachable from
current node in the current subtree, and also outside (without
progress flags). The first component thus has $2^{7\cdot|\mn{CN}({\cal{K}})|}$
states, because it only needs to count up to 1.

Note that if the automaton accepts any tree, it also accepts a regular
one, and a regular tree has bounded degree.