# Finite Entailment of UCRPQs over ${\cal{ALC}}$ Ontologies

Víctor Gutiérrez-Basulto1 Albert Gutowski2 Yazmín Ibáñez-García1 Filip Murlak2
1Cardiff University, UK
2University of Warsaw, Poland
{a.gutowski, f.murlak<EMAIL_ADDRESS>{gutierrezbasultov, ibanezgarciay
<EMAIL_ADDRESS>
###### Abstract

We investigate the problem of _finite_ entailment of ontology-mediated
queries. We consider the expressive query language, unions of conjunctive
regular path queries (UCRPQs), extending the well-known class of union of
conjunctive queries, with regular expressions over roles. We look at
ontologies formulated using the description logic ${\cal{ALC}}$, and show a
tight 2ExpTime upper bound for entailment of UCRPQs. At the core of our
decision procedure, there is a novel automata-based technique introducing a
stratification of interpretations induced by the deterministic finite
automaton underlying the input UCRPQ.

##  1 Introduction

At the intersection of knowledge representation and database theory lies the
fundamental problem of _ontology-mediated query entailment (OMQE)_ , where the
background knowledge provided by an ontology is used to enrich the answers to
queries posed to databases. In this context, description logics (DLs) are a
widely accepted family of logics used to formulate ontologies. By now, the
OMQE problem under the unrestricted semantics (reasoning over arbitrary
models) is well understood for various query languages and DLs (?). In
contrast, for the _finite_ OMQE problem, where one is interested in reasoning
over finite models only, the overall landscape is rather incomplete. However,
in recent years, the study of finite OMQE has been gaining traction,
considering both lightweight and expressive DLs and (mostly) unions of
conjunctive queries (?; ?; ?; ?; ?; ?; ?; ?).

In this paper we consider the problem of finite OMQE with unions of
conjunctive regular path queries (UCRPQs) as the query language. UCRPQs (?; ?)
are a powerful navigational query language for graph databases in which one
can express that two entities are related by a path of edges that can be
specified by a regular language over binary relations. So, UCRPQs extend
unions of conjunctive queries (UCQs) with atoms that might contain regular
expressions that traverse the edges of the database. Indeed, path navigation
is included in the query language XPath 2.0 for XML data, and it is also
present in the SPARQL 1.1 query language for RDF data through the property
path feature. Given the resemblance of instance data stored in ABoxes in DLs
to graph-like data, several investigations on unrestricted entailment of
various types of navigational query languages mediated by DL ontologies have
been carried out (?; ?; ?; ?; ?; ?), yielding algorithmic approaches and
optimal complexity bounds. For finite entailment of regular path queries
mediated by DL ontologies, there are only undecidability results available
(?). The most relevant positive news are the decidability and computational
complexity results by ? (?) and ? (?) on finite entailment of conjuctive
queries with transitive closure over roles mediated by expressive DL
ontologies.

We focus on ontologies formulated using the description logic ${\cal{ALC}}$.
Note that entailment of UCRPQs over ${\cal{ALC}}$ ontologies is not _finitely
controllable_ , i.e. finite and unrestricted entailment do not coincide as it
is _not_ the case that for any ${\cal{ALC}}$ knowledge base ${\cal{K}}$ and
any UCRPQ $\varphi$, it holds that ${\cal{K}}$ entails $\varphi$ over all
(unrestricted) models iff ${\cal{K}}$ entails $\varphi$ over all finite
models. By assuming that the represented world is finite, we can therefore not
reuse existing complexity bounds or algorithmic approaches to UCRPQ
entailment. From a usability perspective, the suitability of this assumption
depends on the potential applications. A particular interest for navigational
queries comes from bioinformatics and cheminformatics (?; ?; ?; ?; ?; ?). For
instance, experts often need to find associations between entities in protein,
cellular, drug, and disease networks (represented as graph databases), so that
e.g. gene-disease-drug associations (corresponding to paths in the database)
can be discovered for developing new treatment methods. In this type of
applications, databases and the models they represent are clearly meant to be
finite. Importantly, biochemical networks contain complex motifs involving
e.g.  _cycles_ or cliques. This type of patterns can be described using
UCRPQs, however, without the finiteness assumption these patterns could be
disregarded as the associated query might not be entailed when reasoning over
all models (including infinite ones).

### Contribution

The main technical contribution of our investigation is the development of a
dedicated automata-based method for entailment of UCRPQs over ${\cal{ALC}}$
ontologies, providing an optimal upper bound. More precisely, we obtain the
following result, where the matching lower bound is inherited from (?).

######  Theorem 1.

Finite entailment of UCRPQs over ${\cal{ALC}}$ ontologies is 2ExpTime-
complete.

In prior work, ? (?) showed that finite entailment of 2RPQs in
$\mathcal{ALCIOF}$ is undecidable. Theorem 1 thus provides a key step towards
delimiting the decidability boundary of finite OMQE with navigational queries.

At the heart of our approach to finite entailment of UCRPQs in ${\cal{ALC}}$
there is a stratification of interpretations induced by the deterministic
finite automaton underlying the UCRPQ. This stratification builds upon the so-
called _tape construction_ , previously used to efficiently evaluate queries
in the extension of XPath 1.0 where arbitrary regular expressions may appear
as path expressions (?). To realize the tape construction, our method
represents UCRPQs by means of a semiautomaton ${\cal{B}}$ (?) and defines an
expansion of ${\cal{B}}$, allowing to trace runs of ${\cal{B}}$ that begin in
all possible states, on all infixes of the input word. We make interpretations
${\cal{I}}$ knowledgeable of the expansion by enriching paths of ${\cal{I}}$
with its possible runs and by associating edges of ${\cal{I}}$ with levels
$\ell$ induced by the transitions of the expansion. In a similar fashion we
also make CRPQs sensible of levels. With this at hand, we tackle finite
entailment by eliminating the lowest level from a query and from an
interpretation, and then recursively solving the simpler problem. At each step
of this process, we should be able to arrange solutions to simpler problems in
a hierarchical way so that we can reason over them. To this aim, we consider a
variant of entailment that includes an _environment_ , which will provide the
necessary information to position the arranged solutions to simpler problems
in the context of larger interpretations. To better keep track of the
complexity of our recursive method, we introduce a modification of the
entailment problem modulo environment in which we look at a particular type of
finite models: _$(\ell,\ell^{\prime})$ -models_, which are models with edges
of levels $\ell$ or higher that are ‘consistent’ w.r.t. queries referring to
edges of level $\ell^{\prime}$ or higher. We solve the problem of finding
$(\ell,\ell^{\prime})$-models recursively by increasing $\ell$ and
$\ell^{\prime}$ in an alternating way, until both reach the maximum level
$n+1$, with $n$ the number of states of ${\cal{B}}$. This will mean solving
finite entailment modulo environment, and thus standard finite entailment as
well.

### Related Work

We next discuss some existing work relevant to our study.

OMQE of Navigational Queries. As previously discussed, there exist various
works on unrestricted entailment of navigational query languages mediated by
DL ontologies. Most of them concentrate on extensions of regular path queries
(RPQs), such as UCRPQs, and consider both Horn (?) and expressive DLs (?; ?;
?; ?). There have been also some studies on entailment of graph XPath queries
(?; ?; ?).

Finite OMQE.  There exist various decidability results and optimal complexity
bounds for finite entailment of union of conjunctive queries in Horn DLs (?;
?) and in expressive DLs from the $\mathcal{S}$ family (?; ?; ?). In most
cases, the computational complexity coincides with that of the unrestricted
case, but the algorithmic approaches are completely different. On the negative
side, undecidability of finite entailment of UCQs in the more expressive DL
$\mathcal{SHOIF}$ was shown by (?), as well as the undecidability result for
finite entailment of 2RPQs in $\mathcal{ALCIOF}$. Closer to our work are the
positive results on finite entailment of UCQs with transitive closure over
roles in expressive DLs allowing for transitivity or transitive closure over
roles (?; ?). These results close the distance to the undecidability frontier
for finite entailment from a different angle by considering ontology languages
more expressive than ${\cal{ALC}}$, but a subclass of UCRPQs as query
language. In the context of database theory research, finite OMQE (also called
open-world query entailment) has also been investigated; for instance, ? (?)
study finite OMQE for inclusion dependencies and functional dependencies over
relations of arbitrary arity, and ? (?) looks at finite OMQE in the two-
variable fragment of FOL with counting quantifiers.

Finite Controllability.  There have been also a few works on finite
controllability in the context of DLs. For instance, ? (?) recently showed
that the $\mathcal{ZOI}$ and $\mathcal{ZOQ}$ members of the $\mathcal{Z}$
family are finitely controllable for UCQs. Beyond DLs, there have been several
works on UCQ-finite controllability: for the guarded fragment of FOL (?) or
for various fragments of existential rules (?; ?; ?; ?; ?). Closer to our
study, is the work by ? (?) on the classification of finitely and non-finitely
controllable subclasses of CRPQs over ontologies formulated in the guarded-
negation fragment of FOL or in the frontier fragment of existential rules.
However, no complexity results or algorithms for finite entailment are
provided for the non-finitely controllable cases.

##  2 Preliminaries

###  2.1 Description Logics

We consider a vocabulary consisting of countably infinite disjoint sets of
_concept names_ $\mathsf{N_{\mathsf{C}}}$, _role names_
$\mathsf{N_{\mathsf{R}}}$, and _individual names_ $\mathsf{N_{I}}$.
_${\cal{ALC}}$ -concepts $C,D$_ are defined by the grammar

$C,D::=A\mid\neg C\mid C\sqcap D\mid\exists r.C$

where $A\in\mathsf{N_{C}}$ and $r\in\mathsf{N_{R}}$. We use standard
abbreviations $\bot$, $\top$, $C\sqcup D$ and $\forall r.C$.

An _${\cal{ALC}}$ -TBox ${\cal{T}}$_ is a finite set of _concept inclusions
(CIs)_ $C\sqsubseteq D$, where $C,D$ are ${\cal{ALC}}$-concepts. An _ABox_
${\cal{A}}$ is a finite non-empty set of _concept_ and _role assertions_ of
the form $A(a)$, $r(a,b)$, where $A\in\mathsf{N_{C}}$, $r\in\mathsf{N_{R}}$
and $\\{a,b\\}\subseteq\mathsf{N_{I}}$. We write $\mathsf{ind}({\cal{A}})$ for
the _set of individual names_ occurring in ${\cal{A}}$. A _knowledge base
(KB)_ is a pair ${\cal{K}}=({\cal{T}},{\cal{A}})$. We write
$\mathsf{CN}({\cal{K}})$ and $\mathsf{rol}({\cal{K}})$ for the _sets of all
concept and role names_ occurring in ${\cal{K}}$. We let $\|{\cal{K}}\|$ be
the total size of the representation of ${\cal{K}}$.

Without loss of generality, we assume throughout the paper that all CIs are in
one of the following _normal forms_ :

$\bigsqcap_{i}A_{i}\sqsubseteq\bigsqcup_{j}B_{j},\quad A\sqsubseteq\exists
r.B,\quad A\sqsubseteq\forall r.B,$

where $A,A_{i},B,B_{j}\in\mathsf{N_{C}}$, $r\in\mathsf{N_{R}}$, and empty
disjunction and conjunction are equivalent to $\bot$ and $\top$, respectively.
Additionally, for each $A\in\mathsf{CN}({\cal{K}})$ there is a complementary
$\bar{A}\in\mathsf{CN}({\cal{K}})$ axiomatized with $\top\sqsubseteq
A\sqcup\bar{A}$ and $A\sqcap\bar{A}\sqsubseteq\bot$.

###  2.2 Interpretations

The semantics is given as usual via _interpretations_
${\cal{I}}=(\Delta^{\cal{I}},\cdot^{\cal{I}})$ consisting of a non-empty
_domain_ $\Delta^{\cal{I}}$ and an _interpretation function $\cdot^{\cal{I}}$_
mapping concept names to subsets of the domain and role names to binary
relations over the domain, and individual names to elements of the domain. The
interpretation of complex concepts $C$ is defined in the usual way (?). An
interpretation ${\cal{I}}$ is a _model of a TBox ${\cal{T}}$_, written
${\cal{I}}\models{\cal{T}}$ if $C^{\cal{I}}\subseteq D^{\cal{I}}$ for all CIs
$C\sqsubseteq D\in{\cal{T}}$. It is a _model of an ABox ${\cal{A}}$_, written
${\cal{I}}\models{\cal{A}}$, if
$\mathsf{ind}({\cal{A}})\subseteq\Delta^{\cal{I}}$, $a^{\cal{I}}=a$ for each
$a\in\mathsf{ind}({\cal{A}})$, $(a,b)\in r^{\cal{I}}$ for all
$r(a,b)\in{\cal{A}}$, and $a\in A^{\cal{I}}$ for all $A(a)\in{\cal{A}}$. The
first two conditions constitute the so-called _standard name assumption._
Finally, ${\cal{I}}$ is a _model of a KB ${\cal{K}}=({\cal{T}},{\cal{A}})$_,
written ${\cal{I}}\models{\cal{K}}$, if ${\cal{I}}\models{\cal{T}}$ and
${\cal{I}}\models{\cal{A}}$.

An interpretation ${\cal{I}}$ is _finite_ if $\Delta^{\cal{I}}$ is finite. An
interpretation ${\cal{I}}^{\prime}$ is a _sub-interpretation_ of ${\cal{I}}$,
written as ${\cal{I}}^{\prime}\subseteq{\cal{I}}$, if
$\Delta^{{\cal{I}}^{\prime}}\subseteq\Delta^{\cal{I}}$,
$A^{{\cal{I}}^{\prime}}\subseteq A^{\cal{I}}$, and
$r^{{\cal{I}}^{\prime}}\subseteq r^{{\cal{I}}}$ for all $A\in\mathsf{N_{C}}$
and $r\in\mathsf{N_{R}}$. For
$\Sigma\subseteq\mathsf{N_{\mathsf{C}}}\cup\mathsf{N_{\mathsf{R}}}$,
${\cal{I}}$ is an interpretation _over signature_ $\Sigma$ if
$A^{\cal{I}}=\emptyset$ and $r^{\cal{I}}=\emptyset$ for all
$A\in\mathsf{N_{\mathsf{C}}}\setminus\Sigma$ and
$r\in\mathsf{N_{\mathsf{R}}}\setminus\Sigma$. 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\mathsf{N_{C}}$ and $r\in\mathsf{N_{R}}$.

A _unary ${\cal{K}}$-type_ is a subset of $\mathsf{CN}({\cal{K}})$ including
either $A$ or $\bar{A}$ for each $A\in\mathsf{CN}({\cal{K}})$. For an
interpretation ${\cal{I}}$ and an element $d\in\Delta^{\cal{I}}$, the _unary
${\cal{K}}$-type of $d$ in ${\cal{I}}$_ is
$\mathsf{tp}^{\cal{I}}(d)=\left\\{A\in\mathsf{CN}({\cal{K}})\bigm{|}d\in
A^{\cal{I}}\right\\}$. We say that ${\cal{I}}$ _realizes_ a unary
${\cal{K}}$-type $\tau$ if $\tau=\mathsf{tp}^{\cal{I}}(d)$ for some
$d\in\Delta^{\cal{I}}$.

###  2.3 Queries and Finite Entailment

We next introduce the query language. We concentrate on Boolean queries, that
is, queries without answer variables. The extension to queries with answer
variables is standard; see, for example, (?). A _conjunctive regular path
query (CRPQ)_ is a first-order formula

$\varphi=\exists\mathbf{x}\,\psi(\mathbf{x})$

such that $\psi(\mathbf{x})$ is constructed using $\wedge$ over atoms of the
form $A(t)$ or ${\cal{E}}(t,t^{\prime})$ where $A\in\mathsf{N_{C}}$,
$t,t^{\prime}$ are variables from $\mathbf{x}$ or individual names from
$\mathsf{N_{I}}$, and ${\cal{E}}$ is a _path expression_ defined by the
grammar

${\cal{E}},{\cal{E}}^{\prime}::=r\mid{\cal{E}}^{*}\mid{\cal{E}}\cup{\cal{E}}^{\prime}\mid{\cal{E}}\circ{\cal{E}}^{\prime}$

where $r\in\mathsf{N_{\mathsf{R}}}$. Thus, ${\cal{E}}$ is essentially a
regular expression over the (infinite) alphabet $\\{r\mid
r\in\mathsf{N_{\mathsf{R}}}\\}$. The set of individual names in $\varphi$ is
denoted with $\mathsf{ind}(\varphi)$. A _conjunctive query (CQ)_ is a CRPQ
that does not use the operators $*,\cup$ and $\circ$ in path expressions, and
a _regular path query (RPQ)_ consists of a single atom of the form
${\cal{E}}(t,t^{\prime})$.

The semantics of CRPQs is defined via matches. Let us fix a CRPQ
$\varphi=\exists\mathbf{x}\,\psi(\mathbf{x})$ and an interpretation
${\cal{I}}$. A _match for $\varphi$ in ${\cal{I}}$_ is a function

$\pi:\mathbf{x}\cup\mathsf{ind}(\varphi)\to\Delta^{\cal{I}}$

such that $\pi(a)=a$, for all $a\in\mathsf{ind}(\varphi)$, and
${\cal{I}},\pi\models\psi(\mathbf{x})$ under the standard semantics of first-
order logic extended with a rule for atoms of the form
${\cal{E}}(t,t^{\prime})$. More formally, we define:

  * •

${\cal{I}},\pi\models\psi_{1}\wedge\psi_{2}$ iff
${\cal{I}},\pi\models\psi_{1}$ and ${\cal{I}},\pi\models\psi_{2}$;

  * •

${\cal{I}},\pi\models A(t)$ iff $\pi(t)\in A^{\cal{I}}$;

  * •

${\cal{I}},\pi\models{\cal{E}}(t,t^{\prime})$ iff
$(\pi(t),\pi(t^{\prime}))\in{\cal{E}}^{\cal{I}}$, where ${\cal{E}}^{\cal{I}}$
is defined inductively as
$({\cal{E}}^{*})^{\cal{I}}=({\cal{E}}^{\cal{I}})^{*}$,
$({\cal{E}}_{1}\cup{\cal{E}}_{2})^{\cal{I}}={\cal{E}}_{1}^{\cal{I}}\cup{\cal{E}}_{2}^{\cal{I}}$,
$({\cal{E}}_{1}\circ{\cal{E}}_{2})^{\cal{I}}={\cal{E}}_{1}^{\cal{I}}\circ{\cal{E}}_{2}^{\cal{I}}$.

An interpretation ${\cal{I}}$ _satisfies_ $\varphi$, written
${\cal{I}}\models\varphi$, if there exists a match for $\varphi$ in
${\cal{I}}$. A _union of CRPQs (UCRPQ)_ is a finite set of CRPQs and a _union
of CQs (UCQ)_ is a finite set of CQs. An interpretation ${\cal{I}}$ satisfies
an UCRPQ $\Phi$, written as ${\cal{I}}\models\Phi$, if
${\cal{I}}\models\varphi$ for some $\varphi\in\Phi$. We say that ${\cal{K}}$
_finitely entails_ $\Phi$, written ${\cal{K}}\models_{\mathsf{fin}}\Phi$, if
each finite model of ${\cal{K}}$ satisfies $\Phi$. A model of ${\cal{K}}$ that
does not satisfy $\Phi$ is a _counter-model_. The _finite entailment problem_
asks if a given KB ${\cal{K}}$ finitely entails a given query $\Phi$.

###  2.4 UCRPQs via Semiautomata

We work with UCRPQs represented by means of a _semiautomaton_ (?)
${\cal{B}}=(Q,\Gamma,\delta)$ where $Q$ is a finite set of states,
$\Gamma\subseteq\\{r\mid r\in\mathsf{N_{R}}\\}$ is a finite
alphabet—throughout the paper we assume $\Gamma=\mathsf{rol}({\cal{K}})$, and
$\delta:Q\times\Gamma\to Q$ is the transition function. A semiautomaton is
essentially a deterministic finite automaton without initial and final states;
a run of a semiautomaton ${\cal{B}}$ over a word $w$ is defined just like for
a finite automaton, except that it can begin in any state and there is no
notion of accepting runs. Under this representation, an RPQ is an atom over a
binary predicate of the form ${\cal{B}}_{q,q^{\prime}}$ where $q,q^{\prime}\in
Q$ are states of ${\cal{B}}$. We let
${\cal{I}},\pi\models{\cal{B}}_{q,q^{\prime}}(t,t^{\prime})$ iff
$(\pi(t),\pi(t^{\prime}))\in{\cal{B}}_{q,q^{\prime}}^{\cal{I}}$ where
${\cal{B}}_{q,q^{\prime}}^{\cal{I}}$ is the set of pairs $(e,e^{\prime})$ such
that for some $n\in\mathbb{N}$ there exist $r_{1},\ldots,r_{n}\in\Gamma$ and
$e_{0},\ldots,e_{n}\in\Delta^{\cal{I}}$ such that

  * •

$e_{0}=e$ and $e_{n}=e^{\prime}$;

  * •

$(e_{i-1},e_{i})\in(r_{i})^{\cal{I}}$ for all $i\in\\{1,\ldots,n\\}$;

  * •

there exists a run of ${\cal{B}}$ on the word $r_{1}\ldots r_{n}$ that begins
in state $q$ and ends in state $q^{\prime}$.

We also allow _edge atoms_ of the form $r(x,x^{\prime})$ for $r\in\Gamma$.

Each UCRPQ $\Phi$ can be effectively rewritten into a UCRPQ $\Phi^{\prime}$
expressed by means of a semiautomaton ${\cal{B}}$ of size $k\cdot 2^{O(m)}$
where $k$ is the number of path expressions in $\Phi$ and $m$ is their maximal
size. The size of CRPQs in $\Phi^{\prime}$ is bounded by the size of CRPQs in
$\Phi$ and $|\Phi^{\prime}|=2^{\mathrm{poly}{\|\Phi\|}}$, where $\|\Phi\|$ is
the total size of $\Phi$.

For simplicity we work with KBs ${\cal{K}}=({\cal{T}},{\cal{A}})$ where the
ABox ${\cal{A}}$ is _trivial_ ; that is, $\mathsf{ind}({\cal{A}})=\\{a\\}$ for
some $a\in\mathsf{N_{I}}$ and ${\cal{A}}$ contains only concept assertions.
The general finite entailment problem can be reduced to this special case
using the following lemma.

######  Lemma 1.

Given an oracle for finite entailment for trivial ABoxes, the general finite
entailment $({\cal{T}},{\cal{A}})\models_{\mathsf{fin}}\Phi$ can be decided in
time $2^{\mathrm{poly}(\|({\cal{T}},{\cal{A}})\|)\cdot
2^{\mathrm{poly}(\|\Phi\|)}}$ using calls to the oracle for
${\cal{K}}^{\prime}=({\cal{T}},{\cal{A}}^{\prime})$ and $\Phi^{\prime}$
consisting of $2^{\mathrm{poly}(\|\Phi\|)}$ CRPQs of linear size over the same
semiautomaton as $\Phi$.

###  2.5 Entailment Modulo Environment

We solve the entailment problem using a divide-and-conquer approach in which
counter-models are decomposed into simpler ones, whose existence is easier to
decide. Each level of this recursive procedure will involve certain
modifications to the TBox. For complexity reasons we need to pay close
attention to these changes, making sure that no blow-up is involved. To make
it easier, we generalize the entailment problem by turning the modifications
into a separate part of the input, which allows fixing the TBox for the
duration of the whole procedure. At every level of the recursion, we will need
to reason ‘externally’ about the way simpler pieces are put together to form
the larger counter-model, and ‘internally’ about how to specify the required
properties of a piece depending on what is happening outside. We will think of
the models as induced subinterpretations of a larger interpretation. Dually,
the remaining part of the larger interpretation can be seen as an external
context, in which our models live. The relevant features of this context will
be represented by environments, which we now define.

An _environment_ ${\cal{E}}=(\Theta,\varepsilon)$ consists of a set $\Theta$
of unary types and a function $\varepsilon:\Theta\to
2^{\mathsf{rol}({\cal{K}})\times\mathsf{CN}({\cal{K}})}$. The intended meaning
is that only types from $\Theta$ are allowed and each element of an allowed
unary type $\tau$ has an $r$-edge to an element in the extension of $B$ in the
external context for each $(r,B)\in\varepsilon(\tau)$. Accordingly, we say
that ${\cal{I}}$ is a _model of ${\cal{K}}$ modulo ${\cal{E}}$_ and write
${{\cal{I}}\models^{\cal{E}}{\cal{K}}}$ if ${\cal{I}}$ realizes only unary
types from $\Theta$ and it is a model of ${\cal{K}}$ under the following
_relaxed semantics of existential restrictions_ :

  * •

for every existential restriction $\exists r.B$ in ${\cal{K}}$ and every
element $d\in\Delta^{\cal{I}}$, $d\in(\exists r.B)^{\cal{I}}$ iff either there
is an $r$-edge in ${\cal{I}}$ from $d$ to an element $e\in B^{\cal{I}}$ or
$(r,B)\in\varepsilon\left(\mathsf{tp}^{\cal{I}}(d)\right)$.

(The semantics of universal restrictions is not altered and it is the
environment’s reponsibility to account for them.) Correspondingly, a query
$\Phi$ is _finitely entailed by ${\cal{K}}$ modulo ${\cal{E}}$_, written
${\cal{K}}\models_{\mathsf{fin}}^{\cal{E}}\Phi$, if for each finite
interpretation ${\cal{I}}$, if ${\cal{I}}\models^{\cal{E}}{\cal{K}}$ then
${\cal{I}}\models\Phi$. The problem of _finite entailment modulo environment_
is to decide for a given KB ${\cal{K}}$, environment ${\cal{E}}$, and query
$\Phi$ if ${\cal{K}}\models_{\mathsf{fin}}^{\cal{E}}\Phi$.

Note that finite entailment modulo environment and ordinary finite entailment
are interreducible. In one direction, it is enough to take the set of all
unary ${\cal{K}}$-types for $\Theta$ and set $\varepsilon(\tau)=\emptyset$ for
all $\tau\in\Theta$. In the other direction, the conditions imposed on unary
types and the relaxed semantics of existential restrictions can be expressed
easily in the TBox. The latter reduction, however, might significantly
increase the size of the TBox. It is easier to control the size of the input
at different levels of the recursion when these conditions are explicitly
represented in the environment.

##  3 Expansion and Decorations

In order to handle UCRPQs expressed by means of a semiautomaton ${\cal{B}}$ we
need to be able to trace runs of ${\cal{B}}$ that begin in all possible
states, on all infixes of the input word. We achieve this using the following
construction.

Let us fix an arbitrary linear order on the set $Q$ of the states of
${\cal{B}}$. The _expansion_ of ${\cal{B}}$ is a semiautomaton
$\widehat{\cal{B}}$ whose set of states is the set $\widehat{Q}$ of all
permutations of $Q$. Thus, an element of $\widehat{Q}$ can be seen as a tuple
$\mathbf{p}=(p_{1},p_{2},\dots,p_{n})$ such that $p_{i}$ is the image of the
$i$th state of ${\cal{B}}$ under the respective permutation. We refer to
positions in this tuple as _levels_. In particular, the _level of $q\in Q$ in
$\mathbf{p}$_ is the unique $i$ such that $q=p_{i}$. Assuming
$\delta:Q\times\mathsf{rol}({\cal{K}})\to Q$ is the transition function of
${\cal{B}}$, we define the transition function

$\hat{\delta}:\widehat{Q}\times\mathsf{rol}({\cal{K}})\to\widehat{Q}$

of $\widehat{\cal{B}}$ by letting $\hat{\delta}\big{(}\mathbf{p},r\big{)}$ be
the permutation $\mathbf{p}^{\prime}$ obtained by listing all states appearing
in the sequence

$\delta(\mathbf{p},r)=\big{(}\delta(p_{1},r),\delta(p_{2},r),\dots,\delta(p_{n},r)\big{)}$

in the order of their first appearances, followed by all remaining states of
${\cal{B}}$ ordered as in $Q$. Note that the level of $\delta(p_{i},r)$ in
$\mathbf{p}^{\prime}$ is at most $i$. Consider the set
$P\subseteq\\{1,2,\dots,n\\}$ of levels $i$ such that the level of
$\delta(p_{i},r)$ in $\mathbf{p}^{\prime}$ is equal to $i$. It follows from
the definition of $\mathbf{p}^{\prime}$ that $P=\\{1,2,\dots,\ell\\}$ for some
$\ell\in\\{1,2,\dots,n\\}$. We call this number $\ell$ the _level of
transition $\mathbf{p}\stackrel{{\scriptstyle
r}}{{\longrightarrow}}\mathbf{p}^{\prime}$_.

From each run of $\widehat{\cal{B}}$ on a word $w$ we can reconstruct all runs
of ${\cal{B}}$ on $w$. Let
$\mathbf{p}_{0},\mathbf{p}_{1},\dots,\mathbf{p}_{m}$ be a run of
$\widehat{\cal{B}}$ on $w$. Consider a run $q_{0},q_{1},\dots,q_{m}$ of
${\cal{B}}$ on $w$. For $i=0,1,\dots,m$, let $\ell_{i}$ be the level of
$q_{i}$ in $\mathbf{p}_{i}$. Any sequence $\ell_{1},\ell_{2},\dots,\ell_{m}$
associated like this with a run of ${\cal{B}}$ will be called a _thread_ in
the run of $\widehat{\cal{B}}$ (see Fig. 1). Notice that two threads that
begin at different levels can meet at the same level somewhere along the run;
if this happens they remain equal until the end of the run. Also, threads can
be born in the middle of a run of $\widehat{\cal{B}}$, but they never
disappear. A crucial property of threads is that they are non-increasing
sequences: the level of $q_{i+1}$ in $\mathbf{p}_{i+i}$ is bounded by the
level of $q_{i}$ in $\mathbf{p}_{i}$.

Figure 1: A thread in a run of the expansion of a semiautomaton.

######  Lemma 2.

Let $\mathbf{p}_{0},\mathbf{p}_{1},\dots,\mathbf{p}_{m}$ be a run of
$\widehat{\cal{B}}$ on $w$, and let $q,q^{\prime}$ be states of ${\cal{B}}$.
There is a run of ${\cal{B}}$ on $w$ from $q$ to $q^{\prime}$ iff there exist
positions $0\leq j_{1}<j_{2}<\dots<j_{k}=m$, levels
$n\geq\ell_{1}>\ell_{2}>\dots>\ell_{k}\geq 1$, and states
$q_{0},q_{1},\dots,q_{k}$ with $1\leq k\leq n$ such that $q_{0}=q$,
$q_{k}=q^{\prime}$, and

  * •

the level of $q_{0}$ in $\mathbf{p}_{0}$ is $\ell_{1}$ and the level of
$q_{k}$ in $\mathbf{p}_{m}$ is $\ell_{k}$;

  * •

for all $i\in\\{1,2,\dots,k-1\\}$, the level of $q_{i}$ in
$\mathbf{p}_{j_{i}}$ is $\ell_{i}$ and the level of
$\delta\big{(}q_{i},w[j_{i}+1]\big{)}$ in $\mathbf{p}_{j_{i}+1}$ is
$\ell_{i+1}$;

  * •

for all $i\in\\{1,2,\dots,k\\}$, each transition taken in the run up to
$\mathbf{p}_{j_{i}}$ has level at least $\ell_{i}$.

As an illustration of Lemma 2, consider the run of the expanded semiautomaton
shown in Fig.1. Tracing the run of the original semiautomaton on the same
word, starting in state $q_{4}$, we discover the positions $j_{1}=3$ and
$j_{2}=7$ where the corresponding thread drops to a lower level. Between these
positions, the thread stays at the same level, beginning with $\ell_{1}=4$
(taking transitions of levels $5,4,5\geq\ell_{1}$), followed by $\ell_{2}=3$
(taking transitions of levels $5,3,5\geq\ell_{2}$), and $\ell_{3}=1$ (taking a
transition of level $5\geq\ell_{3}$).

The next step is to account for the possible runs of $\widehat{\cal{B}}$ over
paths in the interpretation. Towards this goal, we decorate elements of the
interpretation with states of $\widehat{\cal{B}}$. To avoid additional blow-
up, we represent states of $\widehat{\cal{B}}$ using combinations of fresh
concept names $C_{q,\ell}$ where $q$ is a state of ${\cal{B}}$ and
$\ell\in\\{1,2,\dots,n\\}$ is a level; we write
$\mathsf{CN}(\widehat{\cal{B}})$ for the set of all $C_{q,\ell}$. For a state
$\mathbf{p}=(p_{1},p_{2},\dots,p_{n})$ of $\widehat{\cal{B}}$, by
$C_{\mathbf{p}}$ we mean the concept $C_{p_{1},1}\sqcap
C_{p_{2},2}\sqcap\dots\sqcap C_{p_{n},n}$. We say that an element
$e\in\Delta^{\cal{I}}$ is _decorated_ with state $\mathbf{p}$ if $e\in
C_{\mathbf{p}}^{\cal{I}}$. An interpretation ${\cal{I}}$ is
_$\widehat{\cal{B}}$ -decorated_ if no element has incoming edges over
different roles from $\mathsf{rol}({\cal{K}})$ and ${\cal{I}}$ satisfies the
CIs

$C_{\mathbf{p}}\sqsubseteq\forall r.C_{\hat{\delta}(\mathbf{p},r)}\,,\quad
C_{\mathbf{p}}\sqcap
C_{\mathbf{p}^{\prime}}\sqsubseteq\bot\,,\quad\top\sqsubseteq\bigsqcup_{\mathbf{p}\in\widehat{Q}}C_{\mathbf{p}}$

for all states $\mathbf{p},\mathbf{p}^{\prime}$ of $\widehat{\cal{B}}$ such
that $\mathbf{p}\neq\mathbf{p}^{\prime}$. The axiomatization above is
exponential in the size of ${\cal{B}}$, but we can do better.

######  Lemma 3.

Given ${\cal{B}}$ one can compute in polynomial time a TBox
$\widehat{\cal{T}}_{{\cal{B}}}$ such that
${\cal{I}}\models\widehat{\cal{T}}_{{\cal{B}}}$ iff ${\cal{I}}$ is
$\widehat{\cal{B}}$-decorated.

To every edge in a $\widehat{\cal{B}}$-decorated interpretation ${\cal{I}}$ we
can assign a level as follows. Consider elements
$e,e^{\prime}\in\Delta^{\cal{I}}$ such that $(e,e^{\prime})\in r^{\cal{I}}$
for some $r\in\mathsf{rol}({\cal{K}})$. Note that $(e,e^{\prime})\notin
s^{\cal{I}}$ for every $s\in\mathsf{rol}({\cal{K}})\setminus\\{r\\}$. Let
$\mathbf{p}$ and $\mathbf{p}^{\prime}$ be the states decorating $e$ and
$e^{\prime}$, respectively. It holds that $\mathbf{p}\stackrel{{\scriptstyle
r}}{{\longrightarrow}}\mathbf{p}^{\prime}$. By _the level of the edge_
$(e,e^{\prime})$ we shall understand the level of this transition. A _level-
$\ell$ interpretation_ is a $\widehat{\cal{B}}$-decorated interpretation that
does not contain edges of level strictly below $\ell$; if $\ell>n$, this means
that there are no edges at all. The following lemma is the key to our
algorithm.

######  Lemma 4.

Consider a level-$\ell$ interpretation ${\cal{I}}$ and elements $e\in
C_{q,\ell}^{\cal{I}}$ and $e^{\prime}\in C_{q^{\prime},\ell}^{\cal{I}}$. Then,
$(e,e^{\prime})\in{\cal{B}}_{q,q^{\prime}}^{\cal{I}}$ iff there is a path from
$e$ to $e^{\prime}$ in ${\cal{I}}$.

We make use of Lemma 4 by decomposing RPQs into segments corresponding to
different levels, as was done for the runs of $\widehat{\cal{B}}$ in Lemma 2.
To facilitate this, we make our queries aware of levels. A
_$\widehat{\cal{B}}$ -decorated CRPQ_ is a CRPQ $\varphi$ represented by means
of semiautomaton ${\cal{B}}$ that contains exactly one atom of the form
$C_{q,\ell}(x)$ and exactly one atom of the form
$C_{q^{\prime},\ell^{\prime}}(x^{\prime})$ for each atom
${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ in $\varphi$. We call $\ell$ and
$\ell^{\prime}$ the _begin level_ and the _end level_ of atom
${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ in $\varphi$, respectively. Because
levels never increase in a thread of a run of $\widehat{\cal{B}}$, we can
assume without loss of generality that $\ell\geq\ell^{\prime}$ always holds. A
_level- $\ell$ CRPQ_ is a $\widehat{\cal{B}}$-decorated CRPQ that contains no
RPQ atoms of end level strictly below $\ell$. As all end levels are at most
$n$, a level-$\ell$ CRPQ for $\ell>n$ contains no RPQ atoms; that is, it is a
CQ. To _complete_ a CRPQ $\varphi$ means to turn it into a
$\widehat{\cal{B}}$-decorated CRPQ $\varphi^{\prime}$ by adding unary atoms
over concepts $C_{q,\ell}$ in an arbitrary minimal way. Each resulting
$\varphi^{\prime}$ is called a _completion_ of $\varphi$. Over
$\widehat{\cal{B}}$-decorated interpretations, $\varphi$ is equivalent to the
union of its completions. The _completion of a UCRPQ_ $\Phi$ is the union of
all completions of all CRPQs in $\Phi$.

We conclude this section by showing how to turn any counterexample to
${\cal{K}}\models_{\mathsf{fin}}^{\cal{E}}\Phi$ into a
$\widehat{\cal{B}}$-decorated one. Let ${\cal{I}}$ be an interpretation over
$\mathsf{CN}({\cal{K}})\cup\mathsf{rol}({\cal{K}})$. The _product_ of
${\cal{I}}$ and $\widehat{\cal{B}}$ is the interpretation
${\cal{I}}\times\widehat{\cal{B}}$ over
$\mathsf{CN}(\widehat{\cal{B}})\cup\mathsf{CN}({\cal{K}})\cup\mathsf{rol}({\cal{K}})$
such that

  * •

$\Delta^{{\cal{I}}\times\widehat{\cal{B}}}=\Delta^{\cal{I}}\times\mathsf{rol}({\cal{K}})\times\widehat{Q}$,

  * •

$C^{{\cal{I}}\times\widehat{\cal{B}}}=C^{{\cal{I}}}\times\mathsf{rol}({\cal{K}})\times\widehat{Q}$
for all $C\in\mathsf{CN}({\cal{K}})$,

  * •

$C_{q,\ell}^{{\cal{I}}\times\widehat{\cal{B}}}=\Delta^{{\cal{I}}}\times\mathsf{rol}({\cal{K}})\times\\{(p_{1},p_{2},\ldots,p_{n})\in\widehat{Q}:p_{\ell}=q\\}$
for all $q\in Q$ and $\ell\in\\{1,2,\dots,n\\}$,

  * •

$r^{{\cal{I}}\times\widehat{\cal{B}}}=\big{\\{}\big{(}(e,s,\mathbf{p}),(e^{\prime},r,\mathbf{p}^{\prime})\big{)}:(e,e^{\prime})\in
r^{{\cal{I}}},\mathbf{p}\stackrel{{\scriptstyle
r}}{{\longrightarrow}}\mathbf{p}^{\prime},\linebreak
s\in\mathsf{rol}({\cal{K}})\big{\\}}$ for $r\in\mathsf{rol}({\cal{K}})$.

Note that if ${\cal{I}}$ is finite, so is ${\cal{I}}\times\widehat{\cal{B}}$.

######  Lemma 5.

Let $\Phi$ be a UCRPQ, ${\cal{K}}$ an ${\cal{ALC}}$ KB with a trivial ABox,
and ${\cal{E}}$ an environment.

  * •

${\cal{I}}\times\widehat{\cal{B}}$ is a $\widehat{\cal{B}}$-decorated
interpretation.

  * •

If ${\cal{I}}\not\models\Phi$ then
${\cal{I}}\times\widehat{\cal{B}}\not\models\Phi$.

  * •

If ${\cal{I}}\models^{\cal{E}}{\cal{K}}$ then
${\cal{I}}\times\widehat{\cal{B}}\models^{\cal{E}}{\cal{K}}$ up to identifying
the unique individual $a$ in ${\cal{K}}$ with some
$(a,r,\mathbf{p})\in\Delta^{{\cal{I}}\times\widehat{\cal{B}}}$.

##  4 Core Computational Problem

To solve the entailment problem we eliminate the lowest level from the query
and from the interpretation, and solve the problem with fewer levels
recursively. Eliminating each level will involve interpretations built from
pieces that are solutions for the simplified problem. Evaluating CRPQs over
such interpretations requires breaking them down into fragments and it must
accommodate single RPQs witnessed across multiple pieces.

For a UCRPQ $\Phi$ let $\tilde{\Phi}$ be the completion of an equivalent UCRPQ
represented by means of a semiautomaton ${\cal{B}}$. A  _fragment_ of
$\varphi\in\tilde{\Phi}$ is either of the following:

  * •

a $\widehat{\cal{B}}$-decorated CRPQ of the form
$C_{q_{1},\ell_{1}}(y_{1})\land{\cal{B}}_{q_{1},q_{2}}(y_{1},y_{2})\land
C_{q_{2},\ell_{2}}(y_{2})$ or
$C_{q_{1},\ell_{1}}(y_{1})\land{\cal{B}}_{q_{1},q_{2}}(y_{1},y_{2})\land
C_{q_{2},\ell_{2}}(y_{2})\land r(y_{2},y_{3})\land C_{q_{3},\ell_{3}}(y_{3})$
where $y_{1},y_{2},y_{3}$ are fresh variables and
$r\in\mathsf{rol}({\cal{K}})$,

  * •

a connected $\widehat{\cal{B}}$-decorated CRPQ that can be obtained from
$\varphi$ by dropping selected atoms, replacing selected RPQ atoms
${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ by a subset of
${\cal{B}}_{q,q_{1}}(x,y_{1})$, $r(y_{1},y_{2})$,
${\cal{B}}_{q_{3},q^{\prime}}(y_{3},x^{\prime})$ for some fresh variables
$y_{1},y_{2},y_{3}$ and $r\in\mathsf{rol}({\cal{K}})$, and completing the
resulting CRPQ.

A fragment of a $\Phi$ is a fragment of any of the CRPQs in $\tilde{\Phi}$.
Importantly, a fragment of a fragment of $\Phi$ is also a fragment of $\Phi$,
and each $\varphi\in\tilde{\Phi}$ is a fragment of $\Phi$. Up to renaming
fresh variables, $\Phi$ has $2^{\mathrm{poly}(\|\Phi\|)}$ different fragments,
despite ${\cal{B}}$ being exponential in $\|\Phi\|$.

We now enrich interpretations again by including information about matched
fragments of $\Phi$. For each fragment $\varphi$ of $\Phi$ and each
$\emptyset\neq V\subseteq\textit{var}(\varphi)$ we choose a fresh concept name
$A_{\varphi,V}$. We call an interpretation ${\cal{I}}$ _correct (wrt. $\Phi$)_
if $e\in A_{\varphi,V}^{{\cal{I}}}$ iff $\pi(V)=\\{e\\}$ for some match $\pi$
for $\varphi$ in ${\cal{I}}$. Assuming ${\cal{I}}$ is correct,
${\cal{I}}\models\Phi$ iff $A_{\varphi,V}^{{\cal{I}}}\neq\emptyset$ for some
$\varphi\in\tilde{\Phi}$ and $\emptyset\neq V\subseteq\textit{var}(\varphi)$.
Correctness is not compositional: the union of two correct interpretations
sharing a single element need not be correct. As our method of eliminating
levels relies on such decompositions of interpretations, we replace
correctness with a notion that is weaker, but compositional.

We first abstract the decomposition of a $\widehat{\cal{B}}$-decorated CRPQ
induced by a match in a union of disjoint ‘peripheric’ interpretations, each
sharing a single element with a single ‘core’ interpretation (Fig. 2 shows
three ‘peripheric’ interpretations connected to the ‘core’ by single edges,
included in the ‘peripheric’ interpretations). A _partition_ of a
$\widehat{\cal{B}}$-decorated CRPQ $\varphi$ into
$\varphi^{\prime},\varphi_{1},\dots,\varphi_{k}$ is obtained as follows.
Choose $X^{\prime},X_{1},\dots X_{k}\subseteq\textit{var}(\varphi)$ such that

  * •

$X_{i}\cap X_{j}=\emptyset$ for all $i\neq j$;

  * •

for each atom of the form $r(x,x^{\prime})$ in $\varphi$ there exists $i$ such
that either $\\{x,x^{\prime}\\}\subseteq X_{i}$ or
$\\{x,x^{\prime}\\}\subseteq X^{\prime}$.

Based on $X^{\prime},X_{1},\dots X_{k}$ define
$\varphi^{\prime},\varphi_{1},\dots,\varphi_{k}$ as follows. For each atom of
the form $r(x,x^{\prime})$ in $\varphi$ choose $i$ such that
$\\{x,x^{\prime}\\}\subseteq X_{i}$ and add $r(x,x^{\prime})$ to $\varphi_{i}$
or add $r(x,x^{\prime})$ to $\varphi^{\prime}$ provided that
$\\{x,x^{\prime}\\}\subseteq X^{\prime}$. For each RPQ atom
${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ of begin level $\ell$ and end level
$\ell^{\prime}$ in $\varphi$ do one of the following:

  * •

provided that $\\{x,x^{\prime}\\}\subseteq X^{\prime}$, add
${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ to $\varphi^{\prime}$;

  * •

choose $i$ such that $\\{x,x^{\prime}\\}\subseteq X_{i}$ but
$\\{x,x^{\prime}\\}\not\subseteq X^{\prime}$, and add
${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ to $\varphi_{i}$ (light green RPQ in
Fig. 2);

  * •

choose $i$ such that $x\in X^{\prime}\setminus X_{i}$ and $x^{\prime}\in
X_{i}\setminus X^{\prime}$, a level $m$ such that $\ell\geq
m\geq\ell^{\prime}$, a state $p$ of ${\cal{B}}$, and a fresh variable $y$, and
add ${\cal{B}}_{q,p}(x,y)\land C_{p,m}(y)$ to $\varphi^{\prime}$ and
$C_{p,m}(y)\land{\cal{B}}_{p,q^{\prime}}(y,x^{\prime})$ to $\varphi_{i}$ (blue
and orange in Fig. 2);

  * •

choose $i$ such that $x\in X_{i}\setminus X^{\prime}$ and $x^{\prime}\in
X^{\prime}\setminus X_{i}$, a level $m$ such that $\ell\geq
m\geq\ell^{\prime}$, a state $p$ of ${\cal{B}}$, and a fresh variable $y$, and
add ${\cal{B}}_{q,p}(x,y)\land C_{p,m}(y)$ to $\varphi_{i}$ and
$C_{p,m}(y)\land{\cal{B}}_{p,q^{\prime}}(y,x^{\prime})$ to $\varphi^{\prime}$
(dark green in Fig. 2);

  * •

choose $i\neq j$ such that $x\in X_{i}\setminus X^{\prime}$ and $x^{\prime}\in
X_{j}\setminus X^{\prime}$, levels $m,m^{\prime}$ such that $\ell\geq m\geq
m^{\prime}\geq\ell^{\prime}$, states $p,p^{\prime}$ of ${\cal{B}}$, and fresh
variables $y,y^{\prime}$, add ${\cal{B}}_{q,p}(x,y)\land C_{p,m}(y)$ to
$\varphi_{i}$, $C_{p,m}(y)\land{\cal{B}}_{p,p^{\prime}}(y,y^{\prime})\land
C_{p^{\prime},m^{\prime}}$ to $\varphi^{\prime}$, and
$C_{p^{\prime},m^{\prime}}(y^{\prime})\land{\cal{B}}_{p^{\prime},q^{\prime}}(y^{\prime},x^{\prime})$
to $\varphi_{j}$ (purple in Fig. 2).

Note that for each ${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ exactly one of the
above actions can be performed and the choice of $i$ and $j$ is unique. To
complete the construction, add to $\varphi^{\prime}$ all unary atoms of
$\varphi$ over variables already used in $\varphi^{\prime}$, and similarly for
each $\varphi_{i}$. Observe that for each
$X^{\prime}\subseteq\textit{var}(\varphi)$ there is exactly one choice of
$X_{1},X_{2},\dots,X_{k}$ (up to a permutation) such that the resulting
$\varphi_{1},\varphi_{2},\dots,\varphi_{k}$ are connected (regardless of the
choice of $p,p^{\prime}$ and $m,m^{\prime}$). Assuming that $\varphi$ is a
fragment of $\Phi$, it then holds that so are
$\varphi_{1},\varphi_{2},\dots,\varphi_{k}$.

Figure 2: CRPQ $\varphi$ is distributed over the bags constituting
${\cal{I}}$.

We call ${\cal{I}}$ _consistent (wrt. $\Phi$)_ if for each partition of a
fragment $\varphi$ of $\Phi$ into a CRPQ $\varphi^{\prime}$ and fragments
$\varphi_{1},\varphi_{2},\dots,\varphi_{k}$ with
$\textit{var}(\varphi_{i})\cap\textit{var}(\varphi_{j})=\emptyset$ for $i\neq
j$, $V_{i}=\textit{var}(\varphi_{i})\cap\textit{var}(\varphi^{\prime})$, and
$\emptyset\neq
V\subseteq\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})$, there is
no match $\pi$ for $\varphi^{\prime}$ in ${\cal{I}}$ such that
$\pi(V_{i})=\\{e_{i}\\}\subseteq\big{(}A_{\varphi_{i},V_{i}}\big{)}^{{\cal{I}}}$
for all $i$ but
$\pi(V)=\\{e\\}\not\subseteq\big{(}A_{\varphi,V}\big{)}^{{\cal{I}}}$. Clearly,
all correct interpretations are consistent. The converse is not true in
general, but the following key property is preserved.

######  Lemma 6.

For every UCRPQ $\Phi$ and every consistent ${\cal{B}}$-decorated
interpretation ${\cal{I}}$, if $A_{\varphi,V}^{{\cal{I}}}=\emptyset$ for each
$\varphi\in\tilde{\Phi}$ and $\emptyset\neq V\subseteq\textit{var}(\varphi)$,
then ${\cal{I}}\not\models\Phi$.

Consistency is sufficient to express entailment, but it does not yield well to
the recursive elimination of levels. We generalize it by refining the
information about matched fragments of $\Phi$. We introduce fresh concepts
$A_{\varphi,V}^{\kappa}$ where $\varphi$ is a fragment of $\Phi$,
$\emptyset\neq V\subseteq\textit{var}(\varphi)$,

$\kappa:\textit{var}(\varphi)\to\\{1,2,\dots,\ell\\}\,,$

and $\kappa(V)=\\{\ell\\}$ for some $\ell\in\\{1,2,\dots,n+1\\}$. We write
$\mathsf{CN}_{\ell}^{\Phi}$ for the set of $A_{\psi,V}^{\kappa}$ such that
$\kappa(V)=\\{\ell\\}$. Intuitively, $\kappa$ is a synopsis of when specific
fragments of $\psi$ were matched during the recursive search for the model.
Specifically, $\kappa(x)=\ell$ indicates that $x$ was matched after all levels
strictly below $\ell$ had been eliminated from the query, but while level
$\ell$ was still present. Accordingly, $\ell$-consistency, defined below,
ensures that the synopses built so far are consistently updated while level
$\ell$ is being handled.

We call ${\cal{I}}$ _$\ell$ -consistent (wrt. $\Phi$)_ if for each partition
of a fragment $\varphi$ of $\Phi$ into a CRPQ $\varphi^{\prime}$ of level
$\ell$ and fragments $\varphi_{1},\varphi_{2},\dots,\varphi_{k}$ with
$\textit{var}(\varphi_{i})\cap\textit{var}(\varphi_{j})=\emptyset$ for $i\neq
j$, $V_{i}=\textit{var}(\varphi_{i})\cap\textit{var}(\varphi^{\prime})$, and
$\emptyset\neq
V\subseteq\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})$, there is
no match $\pi$ for $\varphi^{\prime}$ in ${\cal{I}}$ such that
$\pi(V_{i})=\\{e_{i}\\}\subseteq\big{(}A_{\varphi_{i},V_{i}}^{\kappa_{i}}\big{)}^{{\cal{I}}}$
for all $i$ but
$\pi(V)=\\{e\\}\not\subseteq(A_{\varphi,V}^{\kappa})^{{\cal{I}}}$ where

  * •

$\kappa_{i}(x)\leq\ell$ for all $x\in\textit{var}(\varphi_{i})\,$,

  * •

$\kappa(x)=\kappa_{i}(x)$ for all $x\in\textit{var}(\varphi_{i})\setminus
V_{i}\,$,

  * •

$\kappa(x)=\ell$ for all
$x\in\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})\,$.

We stress that while $\varphi^{\prime}$ has level $\ell$, fragments
$\varphi,\varphi_{1},\dots,\varphi_{k}$ can have any level. Note also that
$\ell$-consistency speaks only of concept names in
$\mathsf{CN}_{1}^{\Phi}\cup\mathsf{CN}_{2}^{\Phi}\cup\dots\cup\mathsf{CN}_{\ell}^{\Phi}$.
Identifying $A_{\varphi,V}$ with $A_{\varphi,V}^{\kappa}$ for $\kappa$
constantly equal to 1, we get that consistency and $1$-consistency are
equivalent.

In what follows, by an _$(\ell,\ell^{\prime})$ -interpretation_ we mean an
$\ell^{\prime}$-consistent level-$\ell$ interpretation. By an
_$(\ell,\ell^{\prime})$ -model_ of ${\cal{K}}$ modulo ${\cal{E}}$ we mean an
$(\ell,\ell^{\prime})$-interpretation that is model of ${\cal{K}}$ modulo
${\cal{E}}$. The actual problem we will be solving is the following
_$(\ell,\ell^{\prime})$ -model problem_ for $\ell\leq\ell^{\prime}$: Given a
KB ${\cal{K}}$ with a trivial ABox, an environment ${\cal{E}}$, and a UCRPQ
$\Phi$ decide if there exists a finite $(\ell,\ell^{\prime})$-model of
${\cal{K}}$ modulo ${\cal{E}}$.

By Lemma 5, entailment modulo environment (with trivial ABox) can be reduced
to the $(1,1)$-model problem by modifying the environment to forbid all unary
types containing $A^{\kappa}_{\varphi,V}$ for any $\varphi\in\tilde{\Phi}$,
$\emptyset\neq V\subseteq\textit{var}(\varphi)$, and $\kappa$ constantly equal
1. Note that the reduction does not affect the query $\Phi$, nor the KB
${\cal{K}}$. However, it introduces up to $2^{\mathrm{poly}(\|\Phi\|)}$ new
concept names $A_{\varphi,V}$ and $C_{q,\ell}$. Consequently, the number of
unary types is at most
$2^{|\mathsf{CN}({\cal{K}})|+2^{\mathrm{poly}(\|\Phi\|)}}$. It follows that
the size of the environment is bounded by
$2^{\|{\cal{K}}\|+2^{\mathrm{poly}(\|\Phi\|)}}$.

To solve the $(1,1)$-model problem we will proceed recursively, incrementing
$\ell$ and $\ell^{\prime}$ in an alternating fashion, until
$\ell=\ell^{\prime}=n+1$. At each level of the recursion we will be making
multiple recursive calls. During the recursion the UCRPQ $\Phi$ and the TBox
${\cal{T}}$ will remain unchanged, but the ABox and the environment will
evolve. Importantly, we will not introduce any new concepts, so the size of
the environment will always be bounded by
$2^{\|{\cal{K}}\|+2^{\mathrm{poly}(\|\Phi\|)}}$. The size of the ABox will be
bounded by $\|{\cal{K}}\|+2^{\mathrm{poly}(\|\Phi\|)}$ and the number of
individuals will never grow. In consequence, the total cost of the algorithm
can be computed as the cost of a single recursion step times the number of
steps. In the following sections we will show that each recursion step can be
carried out in time $2^{O(\|{\cal{K}}\|)+2^{\mathrm{poly}(\|\Phi\|)}}$,
excluding the cost of the recursive calls. The depth of the recursion is
$O(n)=2^{\mathrm{poly}(\|\Phi\|)}$. The number of recursive calls within a
single recursion step is also bounded by
$2^{O(\|{\cal{K}}\|)+2^{\mathrm{poly}(\|\Phi\|)}}$. This means that the total
number of recursion steps is $2^{\|{\cal{K}}\|\cdot
2^{\mathrm{poly}(\|\Phi\|)}}$ and so is the overall complexity of the
recursive algorithm for the $(1,1)$-model problem.

##  5 Incrementing the Level of Queries

The main goal of this section is to solve the $(\ell,\ell)$-model problem by
reduction to multiple instances of the $(\ell,\ell+1)$-model problem for
$\ell\leq n$. The $(n+1,n+1)$-model problem is discussed briefly at the end of
the section.

As a first step, we observe that it is enough to consider interpretations
whose DAG of strongly connected components is a tree. For this purpose we
define _tree-like_ interpretations as those that can be decomposed into
multiple finite subinterpretations, called _bags_ , arranged into a (possibly
infinite) tree such that: (1) all bags are pairwise disjoint; (2) between each
parent and child bag there is a single edge, pointing from an element of the
parent bag to an element of the child bag; (3) all other edges are between
elements of the same bag. We think of edges between bags as 2-element
interpretations, called _edge-bags_ , sharing the origin with the parent bag
and the target with the child bag. A tree-like interpretation is then a union
of all its bags and edge-bags. Fig. 2 shows a tree-like interpretation with 4
bags and 3 edge-bags. In tree-like interpretations $\ell$-consistency is a
local property.

######  Lemma 7.

A tree-like interpretation is $\ell$-consistent iff each of its bags and edge-
bags is $\ell$-consistent.

######  Lemma 8.

There is a finite $(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo
${\cal{E}}$ iff there is a finite tree-like $(\ell,\ell^{\prime})$-model of
${\cal{K}}$ modulo ${\cal{E}}$ whose bags are strongly connected.

The next step is to eliminate the lowest level from the queries. An
_$(\ell+1)$ -reduct_ of a level-$\ell$ CRPQ $\varphi$ is any CRPQ that can be
obtained from $\varphi$ by first splitting each RPQ atom
${\cal{B}}_{q_{1},q_{2}}(x_{1},x_{2})$ of begin level $\ell_{1}>\ell$ and end
level $\ell$ into ${\cal{B}}_{q_{1},q^{\prime}_{1}}(x_{1},x^{\prime}_{1})\land
C_{q^{\prime}_{1},\ell^{\prime}_{1}}(x^{\prime}_{1})\land
r(x^{\prime}_{1},x^{\prime}_{2})\land
C_{q^{\prime}_{2},\ell}(x^{\prime}_{2})\land{\cal{B}}_{q^{\prime}_{2},q_{2}}(x^{\prime}_{2},x_{2})$
where $\ell_{1}\geq\ell^{\prime}_{1}\geq\ell+1$, and then dropping from the
resulting CRPQ all atoms whose begin and end level is $\ell$ (all unary atoms
are kept). Note that each $(\ell+1)$-reduct $\varphi^{\prime}$ of $\varphi$ is
a conjunction of at most $|\varphi|$ disjoint fragments of $\varphi$ and that
$\textit{var}(\varphi)\subseteq\textit{var}(\varphi^{\prime})$.

######  Lemma 9.

Over ${\cal{B}}$-decorated interpretations, each level-$\ell$ CRPQ implies the
union of its $(\ell+1)$-reducts. Over strongly-connected level-$\ell$
interpretations, each level-$\ell$ CRPQ is equivalent to the union of its
$(\ell+1)$-reducts.

Because Lemma 8 guarantees tree-like solutions with strongly connected bags,
we can replace $\ell$-consistency with _strong $\ell$-consistency_: the only
difference is that $\pi$ ranges over matches of all possible
$(\ell+1)$-reducts of $\varphi^{\prime}$, rather than over matches of
$\varphi^{\prime}$ itself. We restate Lemma 8 as follows.

######  Lemma 10.

There is a finite $(\ell,\ell)$-model of ${\cal{K}}$ modulo ${\cal{E}}$ iff
there is a finite tree-like level-$\ell$ model of ${\cal{K}}$ modulo
${\cal{E}}$ whose edge bags are $\ell$-consistent and bags strongly
$\ell$-consistent.

It remains to show how to find models of the latter form. Let us first see how
to find one consisting of a single bag; that is, how to find a finite strongly
$\ell$-consistent level-$\ell$ model of ${\cal{K}}$ modulo ${\cal{E}}$. We
will show that this amounts to finding a finite $(\ell,\ell+1)$-model of
${\cal{K}}$ modulo ${\cal{E}}^{\prime}$ for one of the $(\ell+1)$-reducts
${\cal{E}}^{\prime}$ of ${\cal{E}}$ described below.

Consider a fragment $\varphi$, a non-empty set
$V\subseteq\textit{var}(\varphi)$, a partition of $\varphi$ into a CRPQ
$\varphi^{\prime}$ of level $\ell$, and fragments
$\varphi_{1},\varphi_{2},\dots,\varphi_{k}$, as in the definition of (strong)
$\ell$-consistency. Let $\kappa:\textit{var}(\varphi)\to\\{1,2,\dots,\ell\\}$
be such that
$\kappa\big{(}\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})\big{)}=\\{\ell\\}$.
Let $\psi^{\prime}$ be an $(\ell+1)$-reduct of $\varphi^{\prime}$. Consider
CRPQs $\psi$ with $\textit{var}(\varphi)\subseteq\textit{var}(\psi)$ that can
be partitioned into $\psi^{\prime}$ and
$\varphi_{1},\varphi_{2},\dots,\varphi_{k}$. Choose the one with minimal
$\textit{var}(\psi)$. This amounts to merging back all RPQ atoms split during
the partition of $\varphi$, provided that their segments were not affected by
replacing $\varphi^{\prime}$ with $\psi^{\prime}$. The CRPQ $\psi$ is not a
fragment, because it need not be connected: Figure 2 right illustrates passing
from $\varphi$ to $\psi$ consisting of two disconnected fragments. Let
$\psi_{1},\psi_{2},\dots,\psi_{m}$ be the fragments constituting $\psi$ and
let $U_{i}=V\cap\textit{var}(\psi_{i})$. An _$(\ell+1)$ -reduct_
${\cal{E}}^{\prime}$ of ${\cal{E}}$ is constructed by iterating over all
possible choices of $\varphi$, $V$, $\varphi^{\prime}$,
$\varphi_{1},\varphi_{2},\dots,\varphi_{k}$, $\psi^{\prime}$, $\kappa$, as
above, and pruning ${\cal{E}}$ for each choice in one of the following ways:

  * •

either pick $i$ such that $U_{i}=\emptyset$ and remove all unary types that
contain any $A^{\kappa_{i}}_{\psi_{i},W_{i}}$ with
$W_{i}\subseteq\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$,
$\kappa_{i}\big{(}\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})\big{)}=\\{\ell+1\\}$,
and $\kappa_{i}(x)=\kappa(x)$ for all
$x\in\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$ ;

  * •

or remove all unary types that contain some $A^{\kappa_{i}}_{\psi_{i},U_{i}}$
with
$\kappa_{i}\big{(}\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})\big{)}=\\{\ell+1\\}$
and $\kappa(x)=\kappa_{i}(x)$ for all
$x\in\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$, for each $i$
such that $U_{i}\neq\emptyset$, but do not contain $A^{\kappa}_{\varphi,V}$.

######  Lemma 11.

${\cal{I}}$ is a strongly $\ell$-consistent level-$\ell$ model of ${\cal{K}}$
modulo ${\cal{E}}$ iff some interpretation that agrees with ${\cal{I}}$ over
all role names and all concept names except $\mathsf{CN}_{\ell+1}^{\Phi}$ is
an $(\ell+1)$-consistent level-$\ell$ model of ${\cal{K}}$ modulo
${\cal{E}}^{\prime}$ for some $(\ell+1)$-reduct ${\cal{E}}^{\prime}$ of
${\cal{E}}$.

Finite models consisting of multiple bags can be constructed bottom-up by a
least fixed point procedure, using Lemma 11 to find each bag.

######  Lemma 12.

The $(\ell,\ell)$-model problem for an ${\cal{ALC}}$ KB ${\cal{K}}$, a UCRPQ
$\Phi$, and an environment ${\cal{E}}$ can be solved in time

$2^{O(\|{\cal{K}}\|)+2^{\mathrm{poly}(\|\Phi\|)}}$

given an oracle for the $(\ell,\ell+1)$-model problem (with the same UCRPQ and
TBox).

At the bottom of the recursion we need to check if there exists a
$(n+1,n+1)$-model for ${\cal{K}}$ modulo ${\cal{E}}$. Now, a
$\widehat{\cal{B}}$-decorated interpretation is level-$(n+1)$ iff it is
_discrete_ ; that is, it has no edges at all. This allows solving the problem
by a direct inspection. Because the ABox is trivial and $\ell$-consistency is
preserved under restrictions of the domain, it is enough to go through all
singleton interpretations.

######  Lemma 13.

The $(n+1,n+1)$-model problem for an ${\cal{ALC}}$ KB ${\cal{K}}$, a UCRPQ
$\Phi$, and an environment ${\cal{E}}$ can be solved in time
$2^{O(\|{\cal{K}}\|)+2^{\mathrm{poly}(\|\Phi\|)}}$.

##  6 Incrementing the Level of Models

In this section we solve the $(\ell,\ell^{\prime})$-model problem by reduction
to multiple instances of the $(\ell^{\prime},\ell^{\prime})$-model problem for
$\ell<\ell^{\prime}$; that is, we eliminate level-$\ell$ edges from the
interpretations. Like in Section 5, we rely on tree-like models of a special
form; this time, however, they may be infinite and an additional step is
needed to turn them into finite ones.

A $\widehat{\cal{B}}$-decorated interpretation is _$\ell^{\prime}$ -flat_ if
it is a tree-like interpretation where all edges between bags have level
strictly below $\ell^{\prime}$, whereas all edges inside bags have level at
least $\ell^{\prime}$.

######  Lemma 14.

If there exists a finite $(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo
${\cal{E}}$ then there exists an $\ell^{\prime}$-flat
$(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo ${\cal{E}}$ with bounded
degree and bag size.

In contrast to Lemma 8, the above only shows that the reformulated condition
is necessary. We show that it is sufficient, by turning an arbitrary
$\ell^{\prime}$-flat $(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo
${\cal{E}}$ with bounded degree and bag size into a finite
$(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo ${\cal{E}}$. For this we
use _coloured blocking_. For $d\in\Delta^{\cal{I}}$, the _$m$ -neighbourhood
$N_{m}^{{\cal{I}}}(d)$ of $d$_ is the interpretation obtained by restricting
${\cal{I}}$ to elements $e\in\Delta^{\cal{I}}$ within distance $m$ from $d$ in
${\cal{I}}$, enriched with a fresh concept interpreted as $\\{d\\}$. A
_colouring of ${\cal{I}}$ with $k$ colours_ is an extension
${\cal{I}}^{\prime}$ of ${\cal{I}}$ to $k$ fresh concept names
$B_{1},\dots,B_{k}$ such that
$B_{1}^{{\cal{I}}^{\prime}},\dots,B_{k}^{{\cal{I}}^{\prime}}$ is a partition
of $\Delta^{{\cal{I}}^{\prime}}=\Delta^{{\cal{I}}}$. We say that $d\in
B_{i}^{{\cal{I}}^{\prime}}$ has colour $B_{i}$. We call ${\cal{I}}^{\prime}$
_$m$ -proper_ if for each $d\in\Delta^{{\cal{I}}^{\prime}}$ all elements of
$N_{m}^{{\cal{I}}^{\prime}}(d)$ have different colours.

######  Fact 1 (? ?).

If ${\cal{I}}$ has bounded degree, then for all $m\geq 0$ there exists an
$m$-proper colouring ${\cal{I}}^{\prime}$ of ${\cal{I}}$ with finitely many
colours. Consider interpretation ${\cal{J}}$ obtained from
${\cal{I}}^{\prime}$ by redirecting some edges such that the old target and
the new target have isomorphic $m$-neighbourhoods in ${\cal{I}}^{\prime}$.
Then, for each conjunctive query $\varphi$ with at most $\sqrt{m}$ binary
atoms, if ${\cal{I}}\not\models\varphi$, then ${\cal{J}}\not\models\varphi$.

Let ${\cal{I}}$ be an $\ell^{\prime}$-flat $(\ell,\ell^{\prime})$-model of
${\cal{K}}$ modulo ${\cal{E}}$ of bounded degree with bags of size at most
$M$. In order to make Fact 1 applicable, we need to express the
$\ell^{\prime}$-consistency condition over ${\cal{I}}$ by means of a finite
set of conjunctive queries, rather than CRPQs. Towards this end, we show that
over ${\cal{I}}$ each level-$\ell^{\prime}$ CRPQ is equivalent to a UCQ. We
rely on the following observation.

######  Lemma 15.

In a match of a $\widehat{\cal{B}}$-decorated CRPQ in a
$\widehat{\cal{B}}$-decorated interpretation, each path witnessing an RPQ atom
of end level at least $\ell^{\prime}$ uses at most $n-\ell^{\prime}$ edges of
level strictly below $\ell^{\prime}$.

We say that a CRPQ $\varphi$ is _bounded by $K$_ over an interpretation
${\cal{J}}$ if for each match of $\varphi$ in ${\cal{J}}$ each RPQ atom of
$\varphi$ can be witnessed by a path of length at most $K$.

######  Lemma 16.

Let ${\cal{J}}$ be $\widehat{\cal{B}}$-decorated interpretation made up of
disjoint level-$\ell^{\prime}$ interpretations of size at most $M$ connected
by edges of level strictly below $\ell^{\prime}$. Assuming $\ell^{\prime}\leq
n$, each level-$\ell^{\prime}$ CRPQ is bounded by $M(n-\ell^{\prime}+1)^{2}$
over ${\cal{J}}$.

For a ${\cal{B}}$-decorated CRPQ $\varphi$, let $\varphi^{(K)}$ be the UCQ
obtained by taking the union of all CQs that can be obtained from $\varphi$ by
eliminating each RPQ atom ${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ in one of
the following ways: either remove the atom and equate variables $x$ and
$x^{\prime}$, or replace the atom with a CQ of the form

$r_{1}(x,y_{1})\land r_{2}(y_{1},y_{2})\land\dots\land
r_{N}(y_{N-1},x^{\prime})$

where $N\leq K$, $y_{1},\dots,y_{N-1}$ are fresh variables, and there is a run
of ${\cal{B}}$ on $r_{1}\dots r_{N}$ that begins in $q$ and ends in
$q^{\prime}$.

######  Fact 2.

If a ${\cal{B}}$-decorated CRPQ $\varphi$ is bounded by $K$ on an
interpretation ${\cal{J}}$, then ${\cal{J}}\models\varphi$ iff
${\cal{J}}\models\varphi^{(K)}$.

The final step before we can apply Fact 1 is to express
$\ell^{\prime}$-consistency as query evaluation. Consider a partition of a
fragment $\varphi$ of $\Phi$ into a CRPQ $\varphi^{\prime}$ of level
$\ell^{\prime}$ and fragments $\varphi_{1},\varphi_{2},\dots,\varphi_{k}$ with
$\textit{var}(\varphi_{i})\cap\textit{var}(\varphi_{j})=\emptyset$ for $i\neq
j$, $V_{i}=\textit{var}(\varphi_{i})\cap\textit{var}(\varphi^{\prime})$, and
$\emptyset\neq
V\subseteq\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})$. Let $\psi$
be the CRPQ obtained from $\varphi^{\prime}$ as follows. Begin from a copy of
$\varphi^{\prime}$. For each $i\in\\{1,\dots,k\\}$, add to $\psi$ an atom
$A_{\varphi_{i},V_{i}}^{\kappa_{i}}(u)$ for some $\kappa_{i}$ satisfying
$\kappa_{i}(x)\leq\ell$ for all $x\in\textit{var}(\varphi_{i})$ and
$\kappa_{i}(x)=\ell$ for all $x\in V_{i}$, and some variable $u$ in $V_{i}$
($V_{i}$ is nonempty, because $\psi^{\prime}$ is connected), and equate all
variables in $V_{i}$. Similarly, add to $\psi$ the atom
$\bar{A}_{\varphi^{\prime},V}(u)$ for some $\kappa$ satisfying
$\kappa(x)=\ell$ for all
$x\in\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})$ and
$\kappa(x)=\kappa_{i}(x)$ for all
$x\in\textit{var}(\varphi)\cap\textit{var}(\varphi_{i})$, and some $u\in V$,
and equate all variables in $V$. Let $\Phi_{\ell^{\prime}}$ be the union of
all CRPQs $\psi$ obtained as above for different choices of $\varphi$,
$\varphi^{\prime}$, $\varphi_{1},\varphi_{2},\dots,\varphi_{k}$, $V$, and
$\kappa_{1},\kappa_{2},\dots,\kappa_{k}$. Note that $\Phi_{\ell^{\prime}}$ is
a union of level-$\ell^{\prime}$ CRPQ. If $\ell^{\prime}>n$,
$\Phi_{\ell^{\prime}}$ is a UCQ.

######  Lemma 17.

If ${\cal{J}}$ is a $\widehat{\cal{B}}$-decorated interpretation, then
${\cal{J}}$ is $\ell^{\prime}$-consistent iff
${\cal{J}}\not\models\Phi_{\ell^{\prime}}$.

Let $K=M(n-\ell^{\prime}+1)^{2}$. Let $t$ be the maximal number of binary
atoms in one CQ in $\Phi_{\ell^{\prime}}^{(K)}$. (Note that if
$\ell^{\prime}>n$, the query $\Phi_{\ell^{\prime}}$ is a UCQ and
$\Phi_{\ell^{\prime}}^{(K)}$ coincides with $\Phi_{\ell^{\prime}}$.) Fix
$m=t^{2}$ and let ${\cal{I}}^{\prime}$ be an $m$-proper colouring of
${\cal{I}}$. On each infinite branch, select the first bag ${\cal{M}}$ such
that for some bag ${\cal{M}}^{\prime}$ higher on this branch, the
$m$-neighbourhood of the target element $e$ of the edge from the parent of
${\cal{M}}$ to ${\cal{M}}$ is isomorphic to the $m$-neighbourhood of the
target $e^{\prime}$ of the edge from the parent of ${\cal{M}}^{\prime}$ to
${\cal{M}}^{\prime}$. Because the number non-isomorphic of $m$-neighbourhoods
in a structure of bounded degree is bounded, the depth of the selected bags in
the tree of bags is also bounded. The set of selected bags is finite and forms
a maximal antichain. Let ${\cal{F}}$ be the interpretation obtained by taking
the union of all strict ancestors of the selected bags, and for each element
$e$ as above, redirect the edge coming from the parent of ${\cal{M}}$ to
$e^{\prime}$.

Clearly, ${\cal{F}}$ is a finite level-$\ell$ interpretation. It is routine to
check that ${\cal{F}}\models^{\cal{E}}{\cal{K}}$. It remains to prove that
${\cal{F}}$ is $\ell^{\prime}$-consistent. We know that ${\cal{I}}$ is
$\ell^{\prime}$-consistent. By Lemma 17,
${\cal{I}}\not\models\Phi_{\ell^{\prime}}$. By Lemma 16 and Fact 2,
${\cal{I}}\not\models\Phi_{\ell^{\prime}}^{(K)}$. By Fact 1,
${\cal{F}}\not\models\Phi_{\ell^{\prime}}^{(K)}$. By construction, ${\cal{F}}$
satisfies the assumptions of Lemma 16. Hence, by Lemma 16 and Fact 2,
${\cal{F}}\not\models\Phi_{\ell^{\prime}}$. We conclude that ${\cal{F}}$ is
$\ell^{\prime}$-consistent using Lemma 17.

Thus we have proved the converse of Lemma 14.

######  Lemma 18.

If there exists an $\ell^{\prime}$-flat $(\ell,\ell^{\prime})$-model of
${\cal{K}}$ modulo ${\cal{E}}$ with bounded degree and bag size then there
exists a finite $(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo
${\cal{E}}$.

Combining Lemmas 6, 14, and 18, we get that there is a finite
$(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo ${\cal{E}}$ iff there is a
bounded-degree $\ell^{\prime}$-flat model of ${\cal{K}}$ modulo ${\cal{E}}$
whose bags are $\ell^{\prime}$-consistent and have bounded size. As in an
$\ell^{\prime}$-flat model each bag is a level-$\ell^{\prime}$ interpretation,
when we restrict our search to one-bag models the problem is an instance of
the $(\ell^{\prime},\ell^{\prime})$-model problem. Models consisting of
multiple bags can be built coinductively top-down by means of a greatest fixed
point algorithm (similar to type elimination), using the
$(\ell^{\prime},\ell^{\prime})$-model problem to check if each bag exists.

######  Lemma 19.

The $(\ell,\ell^{\prime})$-model problem for an ${\cal{ALC}}$ KB ${\cal{K}}$,
a UCRPQ $\Phi$, and an environment ${\cal{E}}$ can be solved in time

$2^{O(\|{\cal{K}}\|)+2^{\mathrm{poly}(\|\Phi\|)}}$

given an oracle for the $(\ell^{\prime},\ell^{\prime})$-model problem (with
the same UCRPQ and TBox).

##  7 Looking Forward (and Back)

This paper provides first positive results on finite entailment of
navigational queries over DLs ontologies. The main technical contribution is
an optimal automata-based 2ExpTime upper bound for finite entailment of UCRPQs
in ${\cal{ALC}}$.

Let us take a look back at our journey. We devised an expansion of the
semiautomaton used to represent UCRPQs to keep track of its runs that begin in
all possible states, on all infixes of the input word. By making
interpretations and CRPQs knowledgeable of the runs of this expansion, we are
able to associate levels to them as dictated by the transitions of the
expansion. To solve the entailment problem, we use a recursive method
eliminating the lowest level from the query and from the interpretation, and
solving then the simpler problem. In particular, we look at problem of finding
$(\ell,\ell^{\prime})$ models, and solve it by recursively increasing $\ell$
and $\ell^{\prime}$ in an alternating way, until both reach a maximum level:
Section 5 and 6 respectively address the increment of the query level and of
the model. We finally showed what to do when $\ell=\ell^{\prime}=n+1$, which
as argued, is enough to solve the original finite entailment problem.

As for future work, the first immediate step is to extend our method to deal
with test atoms of the form $A?$, which are usually available in UCRPQs. For
the ontology language, we believe our method can be adapted to allow inverses,
nominals or counting. Regarding more expressive query languages, the natural
next step is to consider _two-way_ CRPQs. Our current approach relies on the
fact that information only flows forward, and it is not clear whether it can
be adapted to deal with queries that can go back.

## Acknowledgments

This work was supported by Poland’s National Science Centre grant
2018/30/E/ST6/00042. It also benefited from inspiring discussions with Charles
Paperman.

## References

  * Amarilli and Benedikt 2020 Amarilli, A., and Benedikt, M.  2020\.  Finite open-world query answering with number restrictions.  ACM Trans. Comput. Log. 21(4):27:1–27:73.
  * Amendola, Leone, and Manna 2018 Amendola, G.; Leone, N.; and Manna, M.  2018\.  Finite controllability of conjunctive query answering with existential rules: Two steps forward.  In IJCAI, 5189–5193.  ijcai.org.
  * Baader et al. 2017 Baader, F.; Horrocks, I.; Lutz, C.; and Sattler, U.  2017\.  An Introduction to Description Logic.  Cambridge University Press.
  * Baget et al. 2011 Baget, J.-F.; Leclère, M.; Mugnier, M.-L.; and Salvat, E.  2011\.  On rules with existential variables: Walking the decidability line.  Artificial Intelligence 175(9):1620–1654.
  * Bárány, Gottlob, and Otto 2014 Bárány, V.; Gottlob, G.; and Otto, M.  2014\.  Querying the guarded fragment.  Log. Methods Comput. Sci. 10(2).
  * Bednarczyk and Kieroński 2022 Bednarczyk, B., and Kieroński, E.  2022\.  Finite entailment of local queries in the $\mathcal{Z}$ family of description logics.  In Proc. of AAAI-2022.
  * Bednarczyk and Rudolph 2019 Bednarczyk, B., and Rudolph, S.  2019\.  Worst-case optimal querying of very expressive description logics with path expressions and succinct counting.  In IJCAI, 1530–1536.  ijcai.org.
  * Bienvenu et al. 2014 Bienvenu, M.; Calvanese, D.; Ortiz, M.; and Simkus, M.  2014\.  Nested regular path queries in description logics.  In KR.
  * Bienvenu, Ortiz, and Simkus 2015 Bienvenu, M.; Ortiz, M.; and Simkus, M.  2015\.  Regular path queries in lightweight description logics: Complexity and algorithms.  J. Artif. Intell. Res. 53:315–374.
  * Bojańczyk and Parys 2011 Bojańczyk, M., and Parys, P.  2011\.  XPath evaluation in linear time.  J. ACM 58(4):17:1–17:33.
  * Calvanese et al. 2000 Calvanese, D.; Giacomo, G. D.; Lenzerini, M.; and Vardi, M. Y.  2000\.  Containment of conjunctive regular path queries with inverse.  In KR, 176–185.  Morgan Kaufmann.
  * Calvanese, Eiter, and Ortiz 2014 Calvanese, D.; Eiter, T.; and Ortiz, M.  2014\.  Answering regular path queries in expressive description logics via alternating tree-automata.  Inf. Comput. 237:12–55.
  * Chen et al. 2020 Chen, C.; Huang, H.; Ross, K. E.; Cowart, J. E.; Arighi, C. N.; Wu, C. H.; and Natale, D. A.  2020\.  Protein ontology on the semantic web for knowledge discovery.  Scientific Data 7(1):337.
  * Civili and Rosati 2012 Civili, C., and Rosati, R.  2012\.  A broad class of first-order rewritable tuple-generating dependencies.  In Datalog, volume 7494 of Lecture Notes in Computer Science, 68–80.  Springer.
  * Cook et al. 2016 Cook, C. E.; Bergman, M. T.; Finn, R. D.; Cochrane, G.; Birney, E.; and Apweiler, R.  2016\.  The European Bioinformatics Institute in 2016: Data growth and integration.  Nucleic acids research 44:D20–D26.
  * Danielski and Kieronski 2019 Danielski, D., and Kieronski, E.  2019\.  Finite satisfiability of unary negation fragment with transitivity.  In MFCS, volume 138 of LIPIcs, 17:1–17:15.
  * Figueira, Figueira, and Baque 2020 Figueira, D.; Figueira, S.; and Baque, E. P.  2020\.  Finite controllability for ontology-mediated query answering of CRPQ.  In KR, 381–391.
  * Florescu, Levy, and Suciu 1998 Florescu, D.; Levy, A. Y.; and Suciu, D.  1998\.  Query containment for conjunctive queries with regular expressions.  In PODS, 139–148.  ACM Press.
  * Galgonek et al. 2016 Galgonek, J.; Hurt, T.; Michlíková, V.; Onderka, P.; Schwarz, J.; and Vondrášek, J.  2016\.  Advanced SPARQL querying in small molecule databases.  Journal of Cheminformatics 8(1):31.
  * Ginzburg 1968 Ginzburg, A.  1968\.  Algebraic Theory of Automata.  ACM Monograph Series. Academic Press.
  * Glimm et al. 2008 Glimm, B.; Lutz, C.; Horrocks, I.; and Sattler, U.  2008\.  Conjunctive query answering for the description logic SHIQ.  J. Artif. Intell. Res. 31:157–204.
  * Gogacz and Marcinkowski 2013 Gogacz, T., and Marcinkowski, J.  2013\.  Converging to the chase - A tool for finite controllability.  In LICS, 540–549.  IEEE Computer Society.
  * Gogacz et al. 2019 Gogacz, T.; Gutiérrez-Basulto, V.; Ibáñez-García, Y.; Jung, J. C.; and Murlak, F.  2019\.  On finite and unrestricted query entailment beyond SQ with number restrictions on transitive roles.  In IJCAI, 1719–1725.  ijcai.org.
  * Gogacz et al. 2020 Gogacz, T.; Gutiérrez-Basulto, V.; Gutowski, A.; Ibáñez-García, Y.; and Murlak, F.  2020\.  On finite entailment of non-local queries in description logics.  In KR, 424–433.
  * Gogacz, Ibáñez-García, and Murlak 2018 Gogacz, T.; Ibáñez-García, Y.; and Murlak, F.  2018\.  Finite query answering in expressive description logics with transitive roles.  In Proc. of KR-18.
  * Gottlob, Manna, and Pieris 2018 Gottlob, G.; Manna, M.; and Pieris, A.  2018\.  Finite model reasoning in hybrid classes of existential rules.  In IJCAI, 1831–1837.  ijcai.org.
  * Gutiérrez-Basulto, Ibáñez-García, and Jung 2018 Gutiérrez-Basulto, V.; Ibáñez-García, Y. A.; and Jung, J. C.  2018\.  Answering regular path queries over SQ ontologies.  In AAAI, 1845–1852.  AAAI Press.
  * Hu, Qiu, and Dumontier 2015 Hu, W.; Qiu, H.; and Dumontier, M.  2015\.  Link analysis of life science linked data.  In ISWC (2).
  * Ibáñez-García, Lutz, and Schneider 2014 Ibáñez-García, Y. A.; Lutz, C.; and Schneider, T.  2014\.  Finite model reasoning in Horn description logics.  In KR.
  * Kostylev, Reutter, and Vrgoc 2014 Kostylev, E. V.; Reutter, J. L.; and Vrgoc, D.  2014\.  XPath for DL-Lite ontologies.  In Description Logics.
  * Lysenko et al. 2016 Lysenko, A.; Roznovăţ, I. A.; Saqi, M.; Mazein, A.; Rawlings, C. J.; and Auffray, C.  2016\.  Representing and querying disease networks using graph databases.  BioData Mining 9(1):23.
  * Ortiz and Simkus 2014 Ortiz, M., and Simkus, M.  2014\.  Revisiting the hardness of query answering in expressive description logics.  In RR, volume 8741 of Lecture Notes in Computer Science, 216–223.  Springer.
  * Pratt-Hartmann 2009 Pratt-Hartmann, I.  2009\.  Data-complexity of the two-variable fragment with counting quantifiers.  Inf. Comput. 207(8):867–888.
  * Rajabi and Sanchez-Alonso 2021 Rajabi, E., and Sanchez-Alonso, S.  2021\.  Knowledge discovery using SPARQL property path: The case of disease data set.  Journal of Information Science 47(5):677–687.
  * Rosati 2008 Rosati, R.  2008\.  Finite model reasoning in DL-Lite.  In ESWC.
  * Rudolph 2016 Rudolph, S.  2016\.  Undecidability results for database-inspired reasoning problems in very expressive description logics.  In KR, 247–257.  AAAI Press.
  * Schneider and Simkus 2020 Schneider, T., and Simkus, M.  2020\.  Ontologies and data management: A brief survey.  Künstliche Intell. 34(3):329–353.
  * Stefanoni et al. 2014 Stefanoni, G.; Motik, B.; Krötzsch, M.; and Rudolph, S.  2014\.  The complexity of answering conjunctive and navigational queries over OWL 2 EL knowledge bases.  J. Artif. Intell. Res. 51:645–705.

##  Appendix A Additional Definitions

Let us fix ${\cal{K}}=({\cal{T}},{\cal{A}})$. A _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\mathsf{N_{\mathsf{R}}}$,
$(h(d),h(e))\in r^{\cal{J}}$ whenever $(d,e)\in r^{\cal{I}}$, for all
$A\in\mathsf{N_{\mathsf{C}}}$, $h(d)\in A^{\cal{J}}$ whenever $d\in
A^{\cal{I}}$, and $h(a)=a$ for all $a\in\mathsf{ind}({\cal{A}})$.

##  Appendix B Proofs

See 1

###### Proof.

Let ${\cal{I}}$ be a finite model of ${\cal{K}}=({\cal{T}},{\cal{A}})$ such
that ${\cal{I}}\not\models\Phi$. We can think of ${\cal{A}}$ as an
interpretation with domain $\mathsf{ind}({\cal{A}})$. Then, ${\cal{I}}$
contains a subinterpretation ${\cal{I}}^{\prime}$ that is an isomorphic copy
of ${\cal{A}}$, except that the extension of concepts over
$\mathsf{ind}({\cal{A}})$ is kept as in ${\cal{I}}$. Let ${\cal{J}}$ be the
interpretation obtained by starting from ${\cal{I}}^{\prime}$ and for each
$a\in\mathsf{ind}({\cal{A}})$, adding an isomorphic copy ${\cal{I}}_{a}$ of
${\cal{I}}$ sharing only $a$ with ${\cal{I}}^{\prime}$. Clearly, ${\cal{J}}$
is a model of ${\cal{K}}$ and ${\cal{J}}\not\models\Phi$, because ${\cal{I}}$
is a homomorphic image of ${\cal{J}}$. Note also, that
${\cal{I}}_{a}\models{\cal{T}}$ for all $a\in\mathsf{ind}({\cal{A}})$. This
shows that it suffices to look for counter models that are unions of a _core_
interpretation ${\cal{J}}^{\prime}$ that is a copy of ${\cal{A}}$ up to the
interpretations of concept names, and a collection of disjoint _peripheric_
models ${\cal{J}}_{a}$ of ${\cal{T}}$ such that
$\Delta^{{\cal{I}}_{a}}\cap\Delta^{{\cal{J}}^{\prime}}=\\{a\\}$ for
$a\in\mathsf{ind}({\cal{A}})$.

The algorithm iterates through all possible core models ${\cal{J}}^{\prime}$.
For each ${\cal{J}}^{\prime}$ it needs to decide if there exist peripheric
models ${\cal{J}}_{a}$ for $a\in\mathsf{ind}({\cal{A}})$ such that no partial
match $\pi$ of $\varphi\in\Phi$ in ${\cal{J}}^{\prime}$ can be extended to a
full match of $\varphi$ in the whole ${\cal{J}}$. For this it is enough to
know if $({\cal{T}},{\cal{A}}^{\prime})\models_{\mathsf{fin}}\Phi^{\prime}$
where ${\cal{A}}^{\prime}$ ranges over trivial ABoxes using a fixed individual
$a$ and concept names from $\mathsf{CN}({\cal{K}})$, and $\Phi^{\prime}$
ranges over sets of CRPQs $\varphi_{U}$ for $\varphi\in\Phi$ and
$U\subseteq\textit{var}(\varphi)$ defined as follows. The CRPQ $\varphi_{U}$
is obtained from $\varphi$ by

  * •

dropping all atoms that involve no variable from $U$, as well as all edge
atoms involving a variable not in $U$;

  * •

replacing each ${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ such that $x\in U$ and
$x\notin U$ with ${\cal{B}}_{q,p}(x,a)$ for some $p^{\prime}$, and each
${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ such that $x\notin U$ and
$x^{\prime}\in U$ with ${\cal{B}}_{p,q^{\prime}}(a,x^{\prime})$ for some $p$.

Note that $|\Phi^{\prime}|=2^{\mathrm{poly}(\|\Phi\|)}$ but all CRPQs in
$\Phi^{\prime}$ have size bounded by $\max_{\varphi\in\Phi}|\varphi|$ and the
underlying semiautomaton ${\cal{B}}$ is not altered.

The number of possible choices of ${\cal{A}}^{\prime}$ and $\Phi^{\prime}$ is

$2^{\mathsf{CN}({\cal{K}})}\cdot 2^{2^{\mathrm{poly}(\|\Phi\|)}}\,.$

The number of distinguishable choices for each peripheric model
${\cal{I}}_{a}$ is

$2^{2^{\mathrm{poly}(\|\Phi\|)}}\,.$

This gives up to

$2^{|\mathsf{CN}({\cal{K}})|\cdot|{\mathsf{ind}({\cal{A}})}|}\cdot
2^{2^{\mathrm{poly}(\|\Phi\|)}\cdot|{\mathsf{ind}({\cal{A}})}|}=2^{\mathrm{poly}(\|{\cal{K}}\|)\cdot
2^{\mathrm{poly}(\|\Phi\|)}}$

choices for the algorithm. For each choice there are
$|\Phi|\cdot|{\mathsf{ind}({\cal{A}})}|^{O(m)}$ partial matches to consider.
The cost of verifying a single match is polynomial in the size of
${\cal{J}}^{\prime}$ and the size of a single $\Phi^{\prime}$; that is,
$\mathrm{poly}(\|{\cal{K}}\|,2^{\mathrm{poly}(\|\Phi\|)})$. Overall, the
complexity of the algorithm is

$2^{2^{\mathrm{poly}(\|\Phi\|)}\cdot\mathrm{poly}(\|{\cal{K}}\|)}\,.\qed$

See 2

###### Proof.

($\Rightarrow$) The run of ${\cal{B}}$ from $q$ to $q^{\prime}$ induces a
thread in the run of $\widehat{\cal{B}}$. We can split the thread into
segments that stay at the same level, giving levels
$\ell_{1},\ell_{2},\dots,\ell_{k}$, separated by transitions that decrease the
level. Clearly, $1\leq k\leq n$. The last positions on the subsequent levels
give $j_{1},j_{2},\dots,j_{k}$. It is easy to check that the corresponding
states satisfy the conditions specified in the lemma.

($\Leftarrow$) The first and third condition, combined with the fact that
threads are non-increasing, imply that between indexes $j_{i}+1$ and $j_{i+1}$
the thread—from $\delta(q_{i},w[j_{i}+1])$ in $\mathbf{p}_{j_{i}+1}$ to
$q_{i+1}$ (or $q^{\prime}$ for $i=m-1$) in $\mathbf{p}_{j_{i+1}}$—stays at the
same level; similarly for the prefix and suffix. Combined with the transitions
mentioned in the second condition they give a single thread witnessing a run
of ${\cal{B}}$ from $q$ to $q^{\prime}$ on $w$. ∎

See 3

###### Proof.

It is straightforward to express the condition that no element has incoming
edges over different roles from $\mathsf{rol}({\cal{K}})$. Pick a fresh
concept name $A_{r}$ for each $r\in\mathsf{rol}({\cal{K}})$ and include axioms
$\top\sqsubseteq\forall r.A_{r}$ and $A_{r}\sqcap A_{s}\sqsubseteq\bot$ for
all $r,s\in\mathsf{rol}({\cal{K}})$ with $r\neq s$.

We next provide an alternative axiomatization of

$\displaystyle C_{\mathbf{p}}$ $\displaystyle\sqsubseteq$
$\displaystyle\forall r.C_{\hat{\delta}(\mathbf{p},r)}$ (1) $\displaystyle
C_{\mathbf{p}}\sqcap C_{\mathbf{p}^{\prime}}$ $\displaystyle\sqsubseteq$
$\displaystyle\bot$ (2) $\displaystyle\top$ $\displaystyle\sqsubseteq$
$\displaystyle\bigsqcup_{\mathbf{p}\in\widehat{Q}}C_{\mathbf{p}}$ (3)

To encode conditions (3) we include the following axioms for every
$\ell\in\\{1,\dots,n\\}$.

$\top\sqsubseteq\bigsqcup_{q\in Q}C_{q,\ell}$

and

$C_{q,\ell}\sqcap C_{q^{\prime},\ell}\sqsubseteq\bot$

with $q,q^{\prime}\in Q$ such that $q\neq q^{\prime}$. These, together with
the following will enforce condition (2).

$C_{q,\ell}\sqcap C_{q,\ell^{\prime}}\sqsubseteq\bot$

for each pair $\ell,\ell^{\prime}$ with $\ell\neq\ell^{\prime}$ and each $q\in
Q$.

To ensure that the transitions of $\widehat{\cal{B}}$ are faithfully
represented, we will use auxiliary concepts
$A^{r}_{i,j},D^{r}_{i,j},B^{r}_{i}$ with $i,j\in\\{1,\dots,n\\}$, and $r$ a
role name.

Let $\mathbf{p}=(p_{1},\dots,p_{n})\in\widehat{Q}$, and let
$\delta(\mathbf{p},r)=(p^{\prime}_{1},\dots,p^{\prime}_{n})$, for some
arbitrary (but fixed) role name $r$. We will use concept $A^{r}_{i,j}$ is to
indicate that $\delta(qp_{i},r)=p^{\prime}_{k}$ for some
$k\in\\{1,2,\dots,i\\}$. Further, $D^{r}_{i,j}$ will indicate that
$\delta(p_{i},r)=p^{\prime}_{j}$. Finally, $B^{r}_{\ell}$ will help to
indicate that the level of $\mathbf{p}^{\prime}$ is equal to $\ell$. More
precisely, if an element $d$ in the domain encodes the state $\mathbf{p}$, and
the level of $\delta(\mathbf{p},r)$ is $\ell$, then every $r$-successor of $d$
must satisfy $B^{r}_{\ell}$ (see (9)) below.

We have the following axioms:

$\displaystyle\top$ $\displaystyle\sqsubseteq A^{r}_{1,1}$ (4)

For every triple $q,\ell,\ell^{\prime}$ with $q\in Q$ and
$\ell,\ell^{\prime}\in\\{1,\dots,n\\}$

$\displaystyle C_{q,\ell}\sqcap A^{r}_{\ell,\ell^{\prime}}$
$\displaystyle\sqsubseteq\forall r.(\bigsqcup_{1\leq
k\leq\ell^{\prime}}C_{\delta(q,r),k})$ (5) $\displaystyle
C_{q,\ell}\sqcap\exists r.C_{\delta(q,r),\ell^{\prime}}$
$\displaystyle\sqsubseteq D^{r}_{\ell,\ell^{\prime}}$ (6)

For every $\ell,k$ with $1\leq\ell,k<n$:

$\displaystyle D^{r}_{\ell,k}\sqcap A^{r}_{\ell,k}$ $\displaystyle\sqsubseteq
A^{r}_{\ell+1,k+1}$ (7) $\displaystyle D^{r}_{\ell,k^{\prime}}\sqcap
A^{r}_{\ell,k}$ $\displaystyle\sqsubseteq A_{\ell+1,k}\quad\text{ for every
}k^{\prime}<k$ (8)

For every $k\in\\{1,\dots,n\\}$, and every $\ell<k$,

$\displaystyle D^{r}_{n,\ell}\sqcap A^{r}_{n,k}$
$\displaystyle\sqsubseteq\forall r.B^{r}_{k}$ (9)

And for every $\ell<n$,

$\displaystyle B^{r}_{\ell}$
$\displaystyle\sqsubseteq(\bigsqcup_{i<j}(C_{q_{i},\ell}\sqcap
C_{q_{j},\ell+1}))$ (10)

Finally, we require that for every $\ell,k,k^{\prime}\in\\{1,\dots,n\\}$ such
that $k\neq k^{\prime}$:

$\displaystyle A^{r}_{\ell,k}\sqcap A^{r}_{\ell,k^{\prime}}$
$\displaystyle\sqsubseteq\bot$ (11) $\displaystyle D^{r}_{\ell,k}\sqcap
D^{r}_{\ell,k^{\prime}}$ $\displaystyle\sqsubseteq\bot$ (12) $\displaystyle
B^{r}_{k}\sqcap B^{r}_{k^{\prime}}$ $\displaystyle\sqsubseteq\bot$ (13)

Intuitively, the axioms encode the listing order of
$(\delta(p_{1}),\dots,\delta(p_{n}))$ in
$\hat{\delta}(\mathbf{p})=(p^{\prime}_{1},\dots,p^{\prime}_{n})$ as follows.
(4) encodes that the first position of the tuple is (the only) available for
$\delta(p_{1},r)$. Further, by (5) we have that if $q=p_{\ell}$ and the next
available position for $p_{\ell}$ is $\ell^{\prime}$, then
$\delta(p_{\ell},r)=p^{\prime}_{k}$ for some $1\leq k\leq\ell^{\prime}$, which
means in particular that $\delta(p_{1},r)=p^{\prime}_{1}$.

As mentioned above, (6) is used for “recording” the level of
$\delta(p_{\ell},r)$ using the concept $D^{r}_{\ell,\ell^{\prime}}$. That is,
$D^{r}_{\ell,\ell^{\prime}}$ holds whenever
$\delta(p_{\ell},r)=p^{\prime}_{\ell^{\prime}}$.

Clearly, if $\delta(p_{\ell},r)=p^{\prime}_{k}$, and its next available
position was $k$, then the next available position for $\delta(p_{\ell+1})$ is
$k+1$. This situation is captured by (7). On the other hand, if
$\delta(p_{\ell},r)$ does not takes position $k$ (which is only possible if
$\delta(p_{\ell},r)=p^{\prime}_{k^{\prime}}$, with $k^{\prime}<k$) then $k$ is
available for $\delta(p_{\ell+1},r)$, as captured by (8).

Now, we need to account for the positions not taken by any $\delta(p_{i},r)$.
By the way the positions are taken, it is enough to record the smallest
position unused. This information is encoded using the concept $B^{r}_{k}$.
Thus, if $A^{r}_{n,k}$ and $D_{n,\ell}$, for some $\ell<k$, are both satisfied
then $k$ is the next available position for listing the remaining states
ordered as in $Q=q_{1},\dots q_{n}$. This is captured by (9) and (10).

Finally, the role of CIs (11)–(13) is to ensure the consistency of the
information encoded.

With this intuition in mind, it is not difficult to see (1) is faithfully
encoded. ∎

See 4

###### Proof.

($\Rightarrow$) This is obvious because the definition of
${\cal{B}}^{\cal{I}}_{q,q^{\prime}}$ requires a path from $e$ to $e^{\prime}$
in ${\cal{I}}$.

($\Leftarrow$) Consider a path from $e$ to $e^{\prime}$ in ${\cal{I}}$ and the
corresponding run of the automaton $\widehat{\cal{B}}$. We will focus on the
thread starting in the state $q$. It starts on level $\ell$ because $e\in
C^{\cal{I}}_{q,\ell}$ and cannot drop below level $\ell$ because ${\cal{I}}$
is a level-$\ell$ interpretation. Hence, the thread ends in $e^{\prime}$ on
level $\ell$. But the state in $e^{\prime}$ on level $\ell$ is $q^{\prime}$.
Thus, this thread corresponds to a correct run of ${\cal{B}}$ from $q$ to
$q^{\prime}$. ∎

See 5

###### Proof.

${\cal{I}}\times\widehat{\cal{B}}$ is a $\widehat{\cal{B}}$-decorated
interpretation by construction.

The mapping $(e,r,\mathbf{p})\mapsto e$ from ${\cal{I}}\times{\cal{B}}$ to
${\cal{I}}$ is a homomorphism. Should some $\phi\in\Phi$ be matched in
${\cal{I}}\times\widehat{\cal{B}}$, one could compose the match with the
homomorphism above to obtain a match in ${\cal{I}}$.

Assume that ${\cal{I}}\models{\cal{K}}$. Satisfaction of the ABox transfers
directly to ${\cal{I}}\times{\cal{B}}$. Let us see that
${\cal{I}}\times{\cal{B}}$ is a model of the TBox of ${\cal{K}}$. For CIs of
the forms $\bigcap_{i}A_{i}\sqsubseteq\bigsqcup_{j}B_{j}$ and
$A\sqsubseteq\forall r.B$ this follows from the existance of a homomorphic
mapping from ${\cal{I}}\times{\cal{B}}$ to ${\cal{I}}$, described above. For
CIs of the form $A\sqsubseteq\forall r.B$ the reason is that the transition
function of $\widehat{\cal{B}}$ is defined for each state $\mathbf{p}$ of
$\widehat{\cal{B}}$ and each $r\in\mathsf{rol}({\cal{K}})$, thus each $r$-edge
originating in $e$ will have its counterpart originating in $(e,s,\mathbf{p})$
for each $s$ and $\mathbf{p}$. ∎

See 6

###### Proof.

By contradiction, suppose that ${\cal{I}}\models\Phi$. Then there exists a
match $\pi$ of some $\phi\in\tilde{\Phi}$ in ${\cal{I}}$. Take any element $e$
in the image of $\pi$. The definition of consistency applied for the trivial
partition with $\varphi=\varphi^{\prime}$ implies that $e\in
A^{\cal{I}}_{\varphi,V}$ for $V=\pi^{-1}(a)$. ∎

See 7

###### Proof.

Left to right implication is obvious. For right to left implication assume the
contrary, that all bags and edge-bags are $\ell$-consistent, but there is:

  * •

a fragment $\varphi$ of $\Phi$,

  * •

a partition of $\varphi$ into a CRPQ $\varphi^{\prime}$ of level $\ell$ and
fragments $\varphi_{1},\varphi_{2},\dots,\varphi_{k}$, and sets $V$,
$V_{1},V_{2},\dots,V_{k}$ such that:

    * –

$\textit{var}(\varphi_{i})\cap\textit{var}(\varphi_{j})=\emptyset$ for $i\neq
j$,

    * –

$V_{i}=\textit{var}(\varphi_{i})\cap\textit{var}(\varphi^{\prime})$,

    * –

$\emptyset\neq
V\subseteq\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})$;

  * •

a match $\pi$ for $\varphi^{\prime}$ in ${\cal{I}}$ and functions $\kappa$,
$\kappa_{1},\dots,\kappa_{k}$ such that:

    * –

$\pi(V_{i})=\\{e_{i}\\}\subseteq\big{(}A_{\varphi_{i},V_{i}}^{\kappa_{i}}\big{)}^{{\cal{I}}}$
for all $i$,

    * –

$\pi(V)=\\{e\\}\not\subseteq(A_{\varphi,V}^{\kappa})^{{\cal{I}}}$,

    * –

$\kappa_{i}(x)\leq\ell$ for all $x\in\textit{var}(\varphi_{i})\,$,

    * –

$\kappa(x)=\kappa_{i}(x)$ for all $x\in\textit{var}(\varphi_{i})\setminus
V_{i}\,$,

    * –

$\kappa(x)=\ell$ for all
$x\in\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})\,$.

For each RPQ atom ${\cal{B}}_{q,q^{\prime}}(x,y)$ in $\varphi^{\prime}$,
choose a path from $\pi(x)$ to $\pi(y)$ witnessing that the atom is satisfied.
Pick the parameters above and the witnessing paths for which $\pi$ spans
through the smallest number of bags and edge-bags (we count a bag if some edge
atom in $\varphi^{\prime}$ is mapped by $\pi$ to an edge of this bag, or if
some witnessing path shares an edge with this bag). Note that the match of
$\varphi^{\prime}$ given by $\pi$ and the witnessing paths is connected. This
is because the whole query $\varphi$ is connected and because $\pi(V_{i})$
consists of just one element for each $i$ – the query $\varphi^{\prime}$
itself might not be connected, although it would be if we equated all
variables in each $V_{i}$. The number of bags $\pi$ spans through must be at
least two: were it contained in one bag, this bag would be inconsistent.
Essentially, we will show that we can derive the fact that
$e\in(A_{\varphi,V}^{\kappa})^{{\cal{I}}}$ from $\ell$-consistency conditions
for some matches spanning through smaller number of bags.

Let $b$ be the bag of $e$ (not edge-bag, so it is unique). The match $\pi$
necessarily spans through the bag $b$: otherwise no edge or RPQ is matched
inside $b$, so $\varphi^{\prime}$ consists only of unary atoms, which means
that $k=1$, $\varphi_{1}=\varphi$ and $e=e_{1}$, which easily leads to
contradiction. Let $\psi^{\prime},\psi_{1},\dots,\psi_{m}$ be a partition of
$\varphi$ taking into account the bag $b$, match $\pi$ and the chosen
witnessing paths, where $\psi_{1},\dots,\psi_{m}$ are fragments. That is, in
the definition of a partition:

  * •

the initial set $X^{\prime}$ is the set of variables of $\varphi$ which are
mapped by $\pi$ to the bag $b$ (note that $\pi$ is defined only on
$\textit{var}(\varphi^{\prime})$);

  * •

each RPQ is split (or not) in an appropriate way, depending on whether the
corresponding witnessing path has zero, one, or two endpoints in the bag $b$,
and the fresh variables are assigned level and state according to the last (or
first) elements in $b$ on the corresponding witnessing paths;

  * •

the sets $X_{i}$ are chosen in the way which results in $\psi_{i}$ being
fragments.

Let $U_{i}=\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$ and
$\pi^{\prime}$ be a match agreeing with $\pi$ on
$\textit{var}(\psi^{\prime})\cap\textit{var}(\varphi^{\prime})$, extended with
fresh variables mapped to the appropriate elements on witnessing paths. The
set $\pi^{\prime}(U_{i})$ consists of exactly one element, call it
$e^{\prime}_{i}$. Indeed, for some $i$ there is $j$ such that
$\psi_{i}=\varphi_{j}$ and $U_{i}=V_{j}$, and so
$\pi^{\prime}(U_{i})=\pi(V_{j})=\\{e_{j}\\}$; and for other $i$, $\psi_{i}$
consists of some part of $\varphi^{\prime}$, possibly merged with some
$\varphi_{j}$, with all the variables shared with $\psi^{\prime}$ being
matched to an endpoint of an edge leaving or entering bag $b$.

We claim that for each $i$, $e^{\prime}_{i}\in
A^{\lambda_{i}}_{\psi_{i},U_{i}}$ for some appropriate $\lambda_{i}$, such
that we can use $\ell$-consistency for $b$ to show that
$e\in(A_{\varphi,V}^{\kappa})^{{\cal{I}}}$.

To show that, we need to relate all $\varphi_{j}$ to some $\psi_{i}$.
Specifically, for each $i\in\\{1,\dots,m\\}$, consider all
$j\in\\{1,\dots,k\\}$ such that
$\textit{var}(\psi_{i})\cap\textit{var}(\varphi_{j})\neq\emptyset$. Note that
variables in all $\psi^{\prime},\psi_{1},\dots,\psi_{m}$ are exactly the
variables of $\varphi$, along with some fresh variables splitting some RPQs,
and analogously for $\varphi^{\prime},\varphi_{1},\dots,\varphi_{k}$ (and each
of the fragments $\varphi_{j}$ shares at least one variable with $\varphi$).
Since $\psi^{\prime}$ can be seen as a part of $\varphi^{\prime}$ (in
particular,
$\textit{var}(\varphi)\cap\textit{var}(\psi^{\prime})\subseteq\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})$),
it is easy to see that each $j$ will be assigned to some $i$. For each $i$,
$\psi_{i}$ can be (yet again) partitioned into $\psi^{\prime}_{i}$
(intuitively being the common part of $\varphi^{\prime}$ and $\psi_{i}$) and
$\varphi_{j}$ for all $j$ assigned to this $i$. There is also a match
$\pi_{i}$ agreeing with $\pi$ on
$\textit{var}(\psi_{i}^{\prime})\cap\textit{var}(\varphi^{\prime})$, as usual,
extended with fresh variables from $U_{i}$ mapped to the appropriate elements
on witnessing paths. Since this match spans through fewer bags than $\pi$ (it
does not span through the bag $b$, as all edges and parts of RPQs that were
mapped inside $b$ are in $\psi^{\prime}$), the $\ell$-consistency condition
must be satisfied for this choice of parameters; since
$\pi(V_{j})=\\{e_{j}\\}\subseteq\big{(}A_{\varphi_{j},V_{j}}^{\kappa_{j}}\big{)}^{{\cal{I}}}$
for all $j$, we get that $e^{\prime}_{i}\in A^{\lambda_{i}}_{\psi_{i},U_{i}}$
for $\lambda_{i}$ which agrees with $\kappa_{j}$ on all
$\textit{var}(\varphi_{j})\setminus V_{j}$, and is equal to $\ell$ on all
other variables. Using this fact for all $i$ and using $\ell$-consistency in
the bag $b$ for the match $\pi^{\prime}$, we get that
$e\in(A_{\varphi,V}^{\kappa})^{{\cal{I}}}$ for $\kappa$ which agrees with each
$\kappa_{i}$ on all variables from $\varphi_{i}$ apart from $V_{i}$ and is
equal to $\ell$ on all other variables, which is exactly what needed to be
shown. ∎

See 8

###### Proof.

This is proved by routine unravelling. Let ${\cal{I}}$ be a finite
$(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo ${\cal{E}}$. For each
element $d$ in ${\cal{I}}$ define ${\cal{I}}_{d}$ as the subinterpretation of
${\cal{I}}$ obtained by restricting the domain of ${\cal{I}}$ to the elements
in the maximal strongly connected subset of $\Delta^{\cal{I}}$ that contains
$d$. Recall that the ABox ${\cal{A}}$ of ${\cal{K}}$ is trivial. Let $a$ be
the unique element of $\mathsf{ind}({\cal{A}})$. Begin the construction of a
tree-like model ${\cal{J}}$ by taking a copy of ${\cal{I}}_{a}$. Then, as long
as there exists an element $e$ in ${\cal{J}}$ and a CI $A\sqsubseteq\exists
r.B$ in the TBox of ${\cal{K}}$ such that $e\in A^{\cal{J}}$ but there is yet
no $e^{\prime}\in B^{\cal{J}}$ such that $(e,e^{\prime})\in r^{\cal{J}}$, find
the original $d$ of $e$ in ${\cal{I}}$ and an element $d^{\prime}\in
B^{\cal{I}}$ such that $(d,d^{\prime})\in r^{\cal{I}}$. Add to ${\cal{J}}$ a
copy of ${\cal{I}}_{d^{\prime}}$ as a new bag, with an $r$-edge from $e$ to
the copy of $d^{\prime}$. This construction gives a finite interpretation: the
height of the tree of bags associated to ${\cal{J}}$ is bounded by the height
of the DAG of strongly connected components of ${\cal{I}}$. It is
straightforward to check that ${\cal{J}}$ is a level-$\ell$ model of
${\cal{K}}$ modulo ${\cal{E}}$. It is also clear that ${\cal{J}}$ can be
mapped homomorphically to ${\cal{I}}$ by mapping each element of ${\cal{J}}$
to its original in ${\cal{I}}$. Because $\ell^{\prime}$-consistency is defined
in terms of forbidden matches it follows immediately that
$\ell^{\prime}$-consistency of ${\cal{I}}$ implies $\ell^{\prime}$-consistency
of ${\cal{J}}$. ∎

See 9

###### Proof.

Use Lemma 4 and the definition of reducts. ∎

See 11

###### Proof.

The proof will use constructions that are very similar to the ones used in the
proof of Lemma 7. Let us start with right to left implication. Let ${\cal{I}}$
be some $(\ell+1)$-consistent model of ${\cal{K}}$ modulo ${\cal{E}}^{\prime}$
for some $(\ell+1)$-reduct ${\cal{E}}^{\prime}$ of ${\cal{E}}$. We will show
that the exact same model ${\cal{I}}$ is a strongly $\ell$-consistent model of
${\cal{K}}$ modulo ${\cal{E}}$ (note that strong $\ell$-consistency does not
mention concept names from $\mathsf{CN}^{\Phi}_{\ell+1}$, so adjusting them is
not necessary for this implication). Assume the contrary; so there is:

  * •

a fragment $\varphi$,

  * •

a partition of $\varphi$ into a CRPQ $\varphi^{\prime}$ of level $\ell$ and
fragments $\varphi_{1},\varphi_{2},\dots,\varphi_{k}$, and sets $V$,
$V_{1},V_{2},\dots,V_{k}$ such that:

    * –

$\textit{var}(\varphi_{i})\cap\textit{var}(\varphi_{j})=\emptyset$ for $i\neq
j$,

    * –

$V_{i}=\textit{var}(\varphi_{i})\cap\textit{var}(\varphi^{\prime})$,

    * –

$\emptyset\neq
V\subseteq\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})$;

  * •

a match $\pi$ for some $(\ell+1)$-reduct $\psi^{\prime}$ of $\varphi^{\prime}$
in ${\cal{I}}$ and functions $\kappa$, $\kappa_{1},\dots,\kappa_{k}$ such
that:

    * –

$\pi(V_{i})=\\{e_{i}\\}\subseteq\big{(}A_{\varphi_{i},V_{i}}^{\kappa_{i}}\big{)}^{{\cal{I}}}$
for all $i$,

    * –

$\pi(V)=\\{e\\}\not\subseteq(A_{\varphi,V}^{\kappa})^{{\cal{I}}}$,

    * –

$\kappa_{i}(x)\leq\ell$ for all $x\in\textit{var}(\varphi_{i})\,$,

    * –

$\kappa(x)=\kappa_{i}(x)$ for all $x\in\textit{var}(\varphi_{i})\setminus
V_{i}\,$,

    * –

$\kappa(x)=\ell$ for all
$x\in\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})\,$.

For each RPQ atom ${\cal{B}}_{q,q^{\prime}}(x,y)$ in $\psi^{\prime}$, choose a
path from $\pi(x)$ to $\pi(y)$ witnessing that the atom is satisfied.

When constructing ${\cal{E}}^{\prime}$, the exact same parameters were
considered ($\varphi$, its partition into $\varphi^{\prime}$,
$\varphi_{1},\varphi_{2},\dots,\varphi_{k}$, $(\ell+1)$-reduct $\psi^{\prime}$
of $\varphi^{\prime}$, the set $V$ and the function $\kappa$), sets
$U_{1},\dots,U_{m}$ and fragments $\psi_{1},\dots,\psi_{m}$ were defined (note
that for a fixed match $\pi$ and witnessing paths, partial matches and partial
witnessing paths for $\psi_{i}$ can also be obtained, for the parts common
with $\psi^{\prime}$), and a choice was made:

  * •

either pick $i$ such that $U_{i}=\emptyset$ and remove all unary types that
contain any $A^{\lambda_{i}}_{\psi_{i},W_{i}}$ with
$W_{i}\subseteq\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$,
$\lambda_{i}\big{(}\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})\big{)}=\\{\ell+1\\}$,
and $\lambda_{i}(x)=\kappa(x)$ for all
$x\in\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$ ;

  * •

or remove all unary types that contain some $A^{\lambda_{i}}_{\psi_{i},U_{i}}$
with
$\lambda_{i}\big{(}\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})\big{)}=\\{\ell+1\\}$
and $\kappa(x)=\lambda_{i}(x)$ for all
$x\in\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$, for each $i$
such that $U_{i}\neq\emptyset$, but do not contain $A^{\kappa}_{\varphi,V}$.

For each $i\in\\{1,\dots,m\\}$ consider a partition of $\psi_{i}$ into
$\psi^{\prime}_{i}$ (intuitively being the common part of $\psi_{i}$ and
$\psi^{\prime}$) and fragments $\varphi_{j}$ for all $j$ such that
$\textit{var}(\varphi_{j})\cap\textit{var}(\psi_{i})\neq\emptyset$, and a
match $\pi_{i}$ of $\psi^{\prime}_{i}$ agreeing with $\pi$ and the choice of
witnessing paths.

If the first choice was made, take the chosen $i$, choose any element
$e^{\prime}$ in the image of
$\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$ under $\pi_{i}$, and
let $W_{i}$ be the preimage of $e^{\prime}$ under $\pi_{i}$. By
$(\ell+1)$-consistency, we see that $e^{\prime}\in
A^{\lambda_{i}}_{\psi_{i},W_{i}}$, where $\lambda_{i}$ agrees with
$\kappa_{j}$ (and $\kappa$) on $\textit{var}(\varphi_{j})\setminus V_{j}$ for
all $j$ such that
$\textit{var}(\varphi_{j})\cap\textit{var}(\psi_{i})\neq\emptyset$, and is
equal to $\ell+1$ on all other variables. However, all unary types containing
this concept were forbidden in ${\cal{E}}^{\prime}$, which is a contradiction
with ${\cal{I}}$ being a model of ${\cal{K}}$ modulo ${\cal{E}}^{\prime}$.

If the second choice was made, use $(\ell+1)$-consistency for each $\psi_{i}$
with $U_{i}\neq\emptyset$ and its partition as described above, which proves
that $e\in A^{\lambda_{i}}_{\psi_{i},U_{i}}$ for some $\lambda_{i}$ agreeing
with $\kappa_{j}$ (and $\kappa$) on $\textit{var}(\varphi_{j})\setminus V_{j}$
for all $j$ such that
$\textit{var}(\varphi_{j})\cap\textit{var}(\psi_{i})\neq\emptyset$, and is
equal to $\ell+1$ on all other variables. Thus, because of the environment
${\cal{E}}^{\prime}$, $A^{\kappa}_{\varphi,V}$ must also be satisfied. (Note
that the union of $\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$
for all $i$ with $U_{i}\neq\emptyset$ is equal to the union of
$\textit{var}(\varphi_{j})\setminus V_{j}$ for all $\varphi_{j}$ which are not
disjoint with all $\psi_{i}$ considered here).

Now we will prove left to right implication. Assume that ${\cal{I}}$ is a
strongly $\ell$-consistent model of ${\cal{K}}$ modulo ${\cal{E}}$. Let
${\cal{I}}^{\prime}$ be an interpretation that agrees with ${\cal{I}}$ over
all role and concept names except $\mathsf{CN}_{\ell+1}^{\Phi}$, and in which
the interpretation of these concept names is _correct_ in the following sense.
First, for each $e\in\left(A^{\kappa}_{\varphi,V}\right)^{{\cal{I}}^{\prime}}$
with $\mathsf{CN}_{\ell}^{\Phi}$ we let
$e\in\left(A^{\kappa^{\prime}}_{\varphi,V}\right)^{{\cal{I}}^{\prime}}$ where
$\kappa^{\prime}(x)=\ell+1$ for $x\in V$ and $\kappa^{\prime}(x)=\kappa(x)$
for $x\in\textit{var}(\varphi)\setminus V$. Then, we add element $e$ to
$(A^{\kappa}_{\varphi,V})^{{\cal{I}}^{\prime}}$ with
$(A^{\kappa}_{\varphi,V})^{{\cal{I}}^{\prime}}\in\mathsf{CN}^{\Phi}_{\ell+1}$
if and only if there exists some partition of $\varphi$ into
$\varphi^{\prime},\varphi_{1},\dots,\varphi_{k}$, sets $V_{1},\dots,V_{k}$ and
a match $\pi$ for $\varphi^{\prime}$ in ${\cal{I}}^{\prime}$ with all
requirements exactly as in the definition of $(\ell+1)$-consistency, in which
additionally $\kappa_{i}(x)\leq\ell$ for all
$x\in\textit{var}(\varphi_{i})\setminus V_{i}$ and $\kappa_{i}(x)=\ell+1$ for
all $x\in V_{i}$, for $i\in\\{1,\dots,k\\}$. Note that this does not leave
many choices regarding the partition: all variables $x$ such that
$\kappa(x)=\ell+1$ must be in $\varphi^{\prime}$, all other variables of
$\varphi$ must be outside $\varphi^{\prime}$, so it is even known which RPQ
atoms are split; only the levels and states of the fresh variables might
differ between different partitions.

The interpretation ${\cal{I}}^{\prime}$ is $(\ell+1)$-consistent, since any
partition of some $\varphi$ and a corresponding match (as in the definition of
$(\ell+1)$-consistency) for which $\kappa_{i}(V_{i})=\\{\ell+1\\}$ for some
$i$, can be “unwrapped” to ones satisfying the correctness condition, as
follows. If $e_{i}\in A^{\kappa_{i}}_{\varphi_{i},V_{i}}$ and
$\kappa_{i}(V_{i})=\\{\ell+1\\}$, by the correctness condition, there is a
partition of $\varphi_{i}$ and an appropriate match witnessing that. This
partition and match of $\varphi_{i}$ can me “merged” into the partition and
match of $\varphi$. Applying this procedure for all $i$ such that
$\kappa_{i}(V_{i})=\\{\ell+1\\}$ results in a partition and a match of
$\varphi$ to which the correctness condition can be applied.

Now we will construct an appropriate $(\ell+1)$-reduct ${\cal{E}}^{\prime}$ of
${\cal{E}}$. Consider some parameters $\kappa$,
$\varphi,\varphi^{\prime},\varphi_{1},\dots,\varphi_{k},\psi^{\prime}$, $V$,
define $\psi_{1},\dots,\psi_{m},U_{1},\dots,U_{m}$ as when constructing an
$(\ell+1)$-reduct of the environment; recall that $\kappa$ uses levels at most
$\ell$, and
$\kappa\big{(}\textit{var}(\varphi)\cap\textit{var}(\varphi^{\prime})\big{)}=\\{\ell\\}$.
We need to choose one of the two options mentioned in the construction. If for
some $i$ such that $U_{i}=\emptyset$, the interpretation ${\cal{I}}^{\prime}$
does not violate the restrictions imposed by the first choice (that is, there
are no elements in concept $A^{\kappa_{i}}_{\psi_{i},W_{i}}$ in
${\cal{I}}^{\prime}$ for all $W_{i}$ and $\kappa_{i}$ as defined during the
construction of a reduct), choose this option and this $i$. Otherwise, choose
the second option, knowing that in ${\cal{I}}^{\prime}$ for each $i$ such that
$U_{i}=\emptyset$ there is some element $e_{i}\in
A^{\kappa_{i}}_{\psi_{i},W_{i}}$ for some $W_{i}$ and $\kappa_{i}$ such that
$W_{i}\subseteq\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$,
$\kappa_{i}\big{(}\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})\big{)}=\\{\ell+1\\}$,
and $\kappa_{i}(x)=\kappa(x)$ for all
$x\in\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$.

We claim that ${\cal{I}}^{\prime}$ is a model of ${\cal{K}}$ modulo the
environment ${\cal{E}}^{\prime}$ constructed as above. Suppose this is not the
case. By the construction of ${\cal{E}}^{\prime}$, the interpretation
${\cal{I}}^{\prime}$ satisfies all the requirements imposed by the first
choice. Hence, it must be the case that ${\cal{I}}^{\prime}$ does not satisfy
the requirements imposed by the second choice; that is, in
${\cal{I}}^{\prime}$ there is an element $e$ in concepts
$A^{\kappa_{i}}_{\psi_{i},U_{i}}$ where
$\kappa_{i}\big{(}\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})\big{)}=\\{\ell+1\\}$
and $\kappa(x)=\kappa_{i}(x)$ for all
$x\in\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$, for all $i$
such that $U_{i}\neq\emptyset$, but not in $A^{\kappa}_{\varphi,V}$.

For each $i\in\\{1,\dots,m\\}$ and the witnessing element
$e_{i}\in\left(A^{\kappa_{i}}_{\psi_{i},W_{i}}\right)^{{\cal{I}}^{\prime}}$
(if $U_{i}\neq\emptyset$, we let $e_{i}=e$ and $W_{i}=U_{i}$), take the
partition and match $\pi_{i}$ guaranteed by the correctness condition; all
variables from $\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$ are
guaranteed to be in the domain of $\pi_{i}$. Merge all these matches together
into one match $\pi^{\prime}$. It is nearly a match of $\psi^{\prime}$; since
$\kappa_{i}$ determines for each $i$ which RPQ atoms in $\psi_{i}$ will be
split in the partition, and it agrees with $\kappa$ on this matter, we can
identify the splitting variables in $\psi^{\prime}$ and in the domain of
$\pi_{i}$; but these variables
($\textit{var}(\psi^{\prime})\setminus\bigcup_{i}\textit{var}(\psi_{i})$)
might have different states and levels assigned in $\pi^{\prime}$; since
${\cal{I}}$ is a level-$\ell$ interpretation, the assigned levels are at most
$\ell$. Let $\tilde{\psi}^{\prime}$ be an $(\ell+1)$-reduct of $\psi^{\prime}$
with states and levels of these variables adjusted to match the ones in
$\pi^{\prime}$. Let $\tilde{\pi}$ be $\pi^{\prime}$ adjusted to
$\tilde{\psi}^{\prime}$ (it is easy to modify a match for a CRPQ to a match of
its $(\ell+1)$-reduct). We get that there is a partition of $\varphi$ into
$\tilde{\varphi}^{\prime}$, $\tilde{\varphi}_{1},\dots,\tilde{\varphi}_{h}$,
sets $\tilde{V_{1}},\dots,\tilde{V_{h}}$ and the match $\tilde{\pi}$ of an
$(\ell+1)$-reduct $\tilde{\psi}^{\prime}$ of $\tilde{\varphi}^{\prime}$ to
${\cal{I}}^{\prime}$, where $\tilde{\pi}(\tilde{V_{i}})=\\{\tilde{e_{i}}\\}$,
$\tilde{e_{i}}\in\left(A^{\lambda_{i}}_{\tilde{\varphi_{i}},\tilde{V_{i}}}\right)^{{\cal{I}}^{\prime}}$,
and $\lambda_{i}$ do not use level $\ell+1$.

Using strong $\ell$-consistency of ${\cal{I}}$ with these parameters gives us
that $e\in\left(A^{\lambda}_{\varphi,V}\right)^{\cal{I}}$ for some $\lambda$.
One just needs to show that $\lambda(x)=\kappa(x)$ for all
$x\in\textit{var}(\varphi)$ to arrive at a contradiction. The matches
$\pi_{i}$ obtained from correctness condition for
$e_{i}\in\left(A^{\kappa_{i}}_{\psi_{i},W_{i}}\right)^{{\cal{I}}^{\prime}}$
guarantee that $\kappa_{i}(x)=\kappa(x)$ for all
$x\in\textit{var}(\psi_{i})\setminus\textit{var}(\psi^{\prime})$. We also know
that all $x\in\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$ are in
the domain of $\pi_{i}$, so (by the above use of strong $\ell$-consistency)
$\lambda(x)=\ell$ for
$x\in\textit{var}(\psi_{i})\cap\textit{var}(\psi^{\prime})$, and
$\lambda(x)=\kappa(x)$ for all other variables of $\varphi$, which is exactly
what is needed. ∎

See 12

###### Proof.

By Lemma 10 it suffices to decide if there is a finite tree-like level-$\ell$
model of ${\cal{K}}=({\cal{T}},{\cal{A}})$ modulo
${\cal{E}}=(\Theta,\varepsilon)$ whose edge-bags are $\ell$-consistent and
bags are strongly $\ell$-consistent. Our algorithm will compute the set of
unary types that are realizable in such interpretations of increasing height.
Here, by the height of a tree-like interpretation we mean the number of edges
on the longest path from the root bag to a leaf bag.

Th algorithm begins from the empty set of types $\Phi_{0}=\emptyset$. In round
$h=1,2,\dots$, based on the set $\Phi_{h-1}$ it computes the set $\Phi_{h}$ of
types that can be realized in models of height $h-1$. The type $\tau$ is added
to $\Phi_{h}$ iff there exists a finite strongly $\ell$-consistent
level-$\ell$ model of ${\cal{K}}_{\tau}=({\cal{T}},{\cal{A}}_{\tau})$ modulo
${\cal{E}}_{h}$ where

${\cal{A}}_{\tau}=\left\\{A(a)\bigm{|}A\in\tau\right\\}$

for a designated $a\in\mathsf{N_{I}}$ and ${\cal{E}}_{h}$ is defined based on
${\cal{E}}$ and $\Phi_{h-1}$ as explained below; for the existence test we use
Lemma 11.

For unary types $\tau_{1},\tau_{2}$ and a role name $r$ let
${\cal{J}}_{(\tau_{1},r,\tau_{2})}$ be the edge-bag built from an element
$e_{1}$ of type $\tau_{1}$ and an element $e_{2}$ of type $\tau_{2}$ connected
by an $r$-edge. We let ${\cal{E}}_{h}=(\Theta,\varepsilon_{h})$ and include
$(r,B)$ in $\varepsilon_{h}(\tau_{1})$ for $\tau_{1}\in\Theta$ iff either
$(r,B)\in\varepsilon(\tau_{1})$ or there exists $\tau_{2}\in\Theta_{h-1}$ such
that $B\in\tau_{2}$ and ${\cal{I}}_{(\tau_{1},r,\tau_{2})}$ is an
$(\ell,\ell)$-interpretation and satisfies all CIs of the form
$A^{\prime}\sqsubseteq\forall r.B^{\prime}$ in ${\cal{T}}$. Recall that the
first condition amounts to checking that ${\cal{I}}_{(\tau_{1},r,\tau_{2})}$
is ${\cal{B}}$-decorated
(${\cal{I}}_{(\tau_{1},r,\tau_{2})}\models\widehat{\cal{T}}_{\cal{B}}$),
level-$\ell$, and $\ell$-consistent.

Because the computed sets satisfy

$\Phi_{0}\subseteq\Phi_{1}\subseteq\dots\subseteq\Phi_{h-1}\subseteq\Phi_{h}\subseteq\dots,$

after at most $2^{|\mathsf{CN}({\cal{K}})|+2^{\mathrm{poly}(\|{\cal{K}}\|)}}$
rounds the sets $\Phi_{h}$ stabilize. The algorithm should return yes iff the
last $\Phi_{h}$ contains a unary type compatible with the assertions made by
the Abox ${\cal{A}}$ of ${\cal{K}}$ about the unique individual it mentions.
It is not hard to check that each round can be performed in time
$2^{O(\|{\cal{K}}\|)+2^{\mathrm{poly}(\|{\cal{K}}\|)}}$, yielding the desired
complexity upper bound. ∎

See 13

###### Proof.

Let us first see when a discrete interpretation is $(n+1)$-consistent.
Consider a partition of a fragment $\varphi$ into
$\varphi^{\prime},\varphi_{1},\dots,\varphi_{k}$ like in the definition of
$(n+1)$-consistency. Because $\varphi^{\prime}$ has level $n+1$, it must be a
UCQ. If $\varphi^{\prime}$ contains a binary atom, it cannot be matched in a
discrete interpretation. Hence, we can assume that $\varphi^{\prime}$ contains
no binary atoms. Fragments $\varphi_{1},\dots,\varphi_{k}$ share no variables,
but $\varphi$ is connected, so $k=1$. It follows that $\varphi_{1}=\varphi$
and $V\subseteq\textit{var}(\varphi^{\prime})\subseteq V_{1}$. Then,
$(n+1)$-consistency reduces to the condition
$A^{\kappa}_{\varphi,V_{1}}\sqsubseteq A^{\kappa}_{\varphi,V}$ for all
$\kappa$ such that $\kappa(x)=n+1$ for all $x\in V_{1}$. We can capture
$(n+1)$-consistency of the model by replacing ${\cal{E}}$ with the environment
${\cal{E}}^{\prime}=(\Theta^{\prime},\epsilon^{\prime})$ obtained from
${\cal{E}}$ by filtering out unary types that violate this condition. This can
be done in time polynomial in the size of ${\cal{E}}$.

It remains to decide if there is a discrete model of ${\cal{K}}$ modulo
${\cal{E}}^{\prime}$. This is the case iff for the individual $a$ mentioned in
${\cal{A}}$ there is a type $\tau\in\Theta^{\prime}$ compatible with the
assertions on $a$ in ${\cal{A}}$ such that for each concept inclusion
$A\sqsubseteq\exists r.B$ in ${\cal{T}}$ if $A\in\tau$ then
$(r,B)\in\varepsilon^{\prime}(\tau)$. This can be checked in time polynomial
in the size of ${\cal{K}}$ and ${\cal{E}}^{\prime}$.

Overall, the existence of an $(n+1,n+1)$-model of ${\cal{K}}$ modulo
${\cal{E}}$ can be decided in time polynomial in the size of ${\cal{K}}$ and
${\cal{E}}$; that is, in time
$2^{O(\|{\cal{K}}\|)+2^{\mathrm{poly}(\|\Phi\|)}}$. ∎

See 14

###### Proof.

This is also proved by routine unravelling, much like Lemma 8. The difference
is that this time for ${\cal{I}}_{d}$ we take the interpretation ${\cal{I}}$
with all edges of level strictly below $\ell^{\prime}$ removed. This
unravelling procedure may pass through the same element multiple times on the
same branch, so the resulting tree-like structure ${\cal{J}}$ may be infinite.
Because new bags are added to ${\cal{J}}$ only when a witness is missing in
the parent bag, it follows that all edges between bags have level strictly
below $\ell^{\prime}$ (all edges of level at least $\ell^{\prime}$ are already
copied in the parent bag, together with their targets). Hence, ${\cal{J}}$ is
$\ell^{\prime}$-flat. The size of each bag is equal to the size of ${\cal{I}}$
and the degree within each bag is bounded by the maximal degree in
${\cal{I}}$. The number of child bags connected to the same element in the
parent bag is bounded by the size of the TBox. Hence, the degree in
${\cal{J}}$ is bounded. Checking that ${\cal{J}}$ is a
$(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo ${\cal{E}}$ is
straightforward, just like in Lemma 8. ∎

See 15

###### Proof.

Suppose a $\widehat{\cal{B}}$-decorated CRPQ $\varphi$ is matched in a
$\widehat{\cal{B}}$-decorated interpretation ${\cal{J}}$. Each path in
${\cal{J}}$ corresponds to the run $\rho$ of $\widehat{B}$ obtained by reading
the states decorating the elements on the path. Such a path witnesses an RPQ
atom ${\cal{B}}_{q,q^{\prime}}(x,x^{\prime})$ iff the thread of $\rho$
beginning in $q$ ends in $q^{\prime}$. If the atom has end level at least
$\ell^{\prime}$, then the level of $q^{\prime}$ in the last state of $\rho$
must be at least $\ell^{\prime}$. Observe however that each edge of level
strictly below $\ell^{\prime}$ brings all threads from levels $\ell^{\prime}$
and higher at least one level down. Consequently, the path may use at most
$n-\ell^{\prime}$ edges of level strictly below $\ell^{\prime}$. ∎

See 16

###### Proof.

Consider a level-$\ell^{\prime}$ CRPQ $\varphi$ matched in ${\cal{J}}$.
Consider a witnessing path $e_{0},e_{1},\dots,e_{k}$ in ${\cal{J}}$. Let
$\mathbf{p}_{0},\mathbf{p}_{1},\dots,\mathbf{p}_{k}$ be the run of
$\widehat{\cal{B}}$ corresponding to the witnessing path and let
$\ell_{0},\ell_{1},\dots,\ell_{k}$ be the thread in $\rho$ that corresponds to
the witnessing run $q_{0},q_{1},\dots,q_{k}$ of ${\cal{B}}$. We have
$\ell_{0}\geq\ell_{1}\geq\dots\geq\ell_{k}\geq\ell^{\prime}$. Suppose that for
some $i<j$ we have $e_{i}=e_{j}$ and $\ell_{i}=\ell=j$. It follows immediately
that $\mathbf{p}_{i}=\mathbf{p}_{j}$ and $q_{i}=q_{j}$. Thus, we can choose a
shorter witnessing path by skipping $e_{i+1},e_{i+2},\dots,e_{j}$.
Consequently, it is enough to look at witnessing paths that visit each element
at most $(n-\ell^{\prime}+1)$ times. From the assumption on the structure of
${\cal{J}}$ and from Lemma 15 it follows that every simple witnessing path has
length at most $M(n-\ell^{\prime}+1)^{2}$. ∎

See 19

###### Proof.

By Lemma 14 it suffices to decide if there exists an $\ell^{\prime}$-flat
$(\ell,\ell^{\prime})$-model of ${\cal{K}}$ modulo ${\cal{E}}$ with bounded
degree and bag size. Using Lemma 7 and the definition of
$\ell^{\prime}$-flatness this is amounts to deciding if there exists a
(possibly infinite) tree-like model of ${\cal{K}}$ modulo ${\cal{E}}$ such
that each bag is a finite $(\ell^{\prime},\ell^{\prime})$-interpretation, each
edge-bag is an $(\ell,\ell^{\prime})$-interpretation but not
level-$\ell^{\prime}$, and the size of bags and the degree of elements is
bounded.

The algorithms is similar to the one in Lemma 12. The main difference is that
the model can now be infinite. Suppose for a while, however, that we are
interested in computing only finite models. Then we can proceed just like in
Lemma 12, computing sets

$\emptyset=\Phi_{0}\subseteq\Phi_{1}\subseteq\Phi_{2}\subseteq\dots$

but as we are after $\ell^{\prime}$-consistent bags, rather than strongly
$\ell^{\prime}$-consistent, we reduce directly to the
$(\ell^{\prime},\ell^{\prime})$-model problem for ${\cal{K}}_{\tau}$ defined
like before, and ${\cal{E}}_{h}$ define almost like before, the difference
being that we additionally require that the edge in
${\cal{J}}_{(\tau_{1},r,\tau_{2})}$ has level strictly below $\ell^{\prime}$.
We do not need to do anything about the size of the bags and the degree,
because in a finite interpretation these are always bounded.

In order to take into account also infinite models, we replace induction by
co-induction. The algorithm proceeds just like described above but it starts
from $\Phi_{0}$ containing all unary types over $\mathsf{CN}({\cal{K}})$ and
concepts $C_{q,k}$ and $A_{\psi,V}^{\kappa}$. It follows that

$\Phi_{0}\supseteq\Phi_{1}\supseteq\dots\supseteq\Phi_{h-1}\supseteq\Phi_{h}\supseteq\dots\,.$

Like before, the sequence must stabilize after at most
$2^{|\mathsf{CN}({\cal{K}})|+2^{\mathrm{poly}(\|{\cal{K}}\|)}}$ steps. We
claim that the algorithm can answers yes iff the last computed $\Phi_{h}$
contains a type compatible with the ABox of ${\cal{K}}$. This is because one
can built the potentially infinite model top down plugging in as bags the
models witnessing the addition of $\tau$ to $\Phi_{h}$ in the last round.
Importantly, the number of these witnesses is finite, because the number of
invoked instances of the $(\ell^{\prime},\ell^{\prime})$-model problem is
finite. Consequently, the size of bags in the constructed model is bounded.
The number of child bags attached to each element is bounded by the number of
existential restrictions in the TBox of ${\cal{K}}$, so the degree in the
constructed model is also bounded. The complexity bound follows like in Lemma
12. ∎