Copyright for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).

This is the extended version of a paper presented at DL 2024: 37th
International Workshop on Description Logics.

[The Precise Complexity of Reasoning in $\mathcal{ALC}$ with
$\omega$-Admissible Concrete Domains (Extended Version)]

[orcid=0000-0003-0924-8478<EMAIL_ADDRESS>url=https://lat.inf.tu-dresden.de/ stefborg, ] [orcid=0000-0002-8623-6465,
<EMAIL_ADDRESS>url=https://lat.inf.tu-dresden.de/
debortoli, ] [orcid=0000-0001-5999-2583<EMAIL_ADDRESS>url=https://pkoopmann.github.io, ]

# The Precise Complexity of Reasoning in ALC with Omega-Admissible Concrete
Domains (Extended Version)

Stefan Borgwardt  Filippo De Bortoli  Patrick Koopmann  TU Dresden, Institute
of Theoretical Computer Science
Dresden, Germany  Center for Scalable Data Analytics and Artificial
Intelligence (ScaDS.AI)
Dresden/Leipzig, Germany  Vrije Universiteit Amsterdam, Department of Computer
Science
Amsterdam, The Netherlands

(2024)

###### Abstract

Concrete domains have been introduced in the context of Description Logics to
allow references to qualitative and quantitative values. In particular, the
class of $\omega$-admissible concrete domains, which includes Allen’s interval
algebra, the region connection calculus (RCC8), and the rational numbers with
ordering and equality, has been shown to yield extensions of $\mathcal{ALC}$
for which concept satisfiability w.r.t. a general TBox is decidable. In this
paper, we present an algorithm based on type elimination and use it to show
that deciding the consistency of an $\mathcal{ALC}(\mathfrak{D})$ ontology is
ExpTime-complete if the concrete domain $\mathfrak{D}$ is $\omega$-admissible
and its constraint satisfaction problem is decidable in exponential time.
While this allows us to reason with concept and role assertions, we also
investigate _feature assertions_ $f(a,c)$ that can specify a constant $c$ as
the value of a feature $f$ for an individual $a$. We show that, under
conditions satisfied by all known $\omega$-admissible domains, we can add
feature assertions without affecting the complexity.

###### keywords:

Description Logics Concrete Domains Reasoning Complexity Type Elimination

##  1 Introduction

Reasoning about numerical attributes of objects is a core requirement of many
applications. For this reason, _Description Logics (DLs)_ that integrate
reasoning over an abstract domain of knowledge with references to values drawn
from a _concrete domain_ have already been investigated for over 30 years [1,
2, 3, 4, 5, 6, 7, 8, 9, 10]. In this setting, DLs are extended by _concrete
features_ that are interpreted as partial functions mapping abstract domain
elements to concrete values, such as the feature $\mathsf{diastolic}$ that
describes the diastolic blood pressure of a person. Using _concrete domain
restrictions_ we can then describe constraints over these features and state,
e.g. that all patients have a diastolic blood pressure that is lower than
their systolic blood pressure, by adding the concept inclusion
$\mathsf{Patient}\sqsubseteq\exists\mathsf{diastolic},\mathsf{systolic}.{<}$
to the ontology. More interestingly, we can use _feature paths_ to compare the
feature values of different individuals: the inclusion
$\top\sqsubseteq\forall\mathsf{hasChild}\,\mathsf{age},\mathsf{age}.{<}$
states that children are always younger than their parents.

Unfortunately, dealing with feature paths in DLs is very challenging and often
leads to undecidability [2, 11, 9], which is why restrictive conditions on the
concrete domains were introduced to regain decidability. An approach inspired
from research on constraint satisfaction is based on _$\omega$ -admissibility_
[5], which requires certain compositionality properties for finite and
countable sets of constraints. This enables the composition of full models
from local solutions of sets of concrete domain constraints. Being quite
restrictive, at first only two examples of $\omega$-admissible concrete
domains were known, namely Allen’s interval algebra and the region connection
calculus (RCC8). Recently, the conditions of $\omega$-admissibility were
investigated in more detail, and it was shown that $\omega$-admissible
concrete domains can be obtained from _finitely bounded homogeneous
structures_ [9]. This class includes the rational numbers
$\mathfrak{Q}:=(\mathbb{Q},<,=,>)$ with ordering and equality, and is closed
under union and certain types of product [9].

Despite these extensive investigations, the precise complexity of reasoning
using description logics with concrete domains has been established only for a
few special cases so far [2, 7, 8, 10]. These results have been obtained by
automata-based techniques, and yield decidability or tight complexity bounds
for cases where the concrete domain is not $\omega$-admissible, such as the
ordered integers $(\mathbb{Z},<,=,>)$ [8] or the set of strings over a finite
alphabet with a prefix relation [10]. In contrast, the goal of this paper is
to derive a tight complexity bound for ontology consistency in the extension
of $\mathcal{ALC}$ with any $\omega$-admissible concrete domain. Using an
algorithm based on type elimination, we establish that this decision problem
is ExpTime-complete under the assumption that the concrete domain
$\mathfrak{D}$ is $\omega$-admissible and that its _constraint satisfaction
problem_ (CSP) is decidable in exponential time. The latter condition holds
for all finitely bounded homogeneous structures (including the three examples
from above), since their CSP is guaranteed to be in NP and in some cases, e.g.
for $\mathfrak{Q}$, is decidable in polynomial time.

Additionally, we consider _predicate_ and _feature assertions_. These allow us
to constrain values of features associated to named individuals, e.g. to write
${<}(\mathsf{age}(\mathsf{mary}),\mathsf{age}(\mathsf{bob}))$ to state that
Mary is younger than Bob, or to specify a constant value of a feature for a
named individual, e.g. using $\mathsf{systolic}(\mathsf{mary},122)$ to state
that Mary’s systolic blood pressure equals $122$. We prove that consistency in
the presence of predicate assertions can always be reduced in polynomial time
to consistency without predicate assertions. For feature assertions, we show
that this holds if we consider _homogeneous_ $\omega$-admissible concrete
domains, which again is the case for the three concrete domains from above.
Finally, we show that supporting feature assertions is equivalent to
supporting singleton predicates of the form $=_{c}$ for a constant $c$ in the
concrete domain.

Omitted proofs of the results presented in the text can be found in the
appendix.

##  2 Preliminaries

Concrete Domains. As usual for DLs, we adopt the term _concrete domain_ to
refer to a relational structure $\mathfrak{D}=(D,P_{1}^{D},P_{2}^{D},\dots)$
over a non-empty, countable relational signature $\\{P_{1},P_{2},\dots\\}$,
where $D$ is a non-empty set, and each predicate $P$ has an associated arity
$k\in\mathbb{N}$ and is interpreted by a relation $P^{D}\subseteq D^{k}$. An
example is the structure $\mathfrak{Q}:=(\mathbb{Q},{<},{=},{>})$ over the
rational numbers $\mathbb{Q}$ with standard binary order and equality
relations. Given a countably infinite set $V$ of variables, a _constraint
system_ over $V$ is a set $\mathfrak{C}$ of _constraints_
$P(v_{1},\dotsc,v_{k})$, where $v_{1},\dotsc,v_{k}\in V$ and $P$ is a $k$-ary
predicate of $\mathfrak{D}$. We denote by $V(\mathfrak{C})$ the set of
variables that occur in $\mathfrak{C}$. The constraint system $\mathfrak{C}$
is _satisfiable_ if there is a _homomorphism_ $h\colon V(\mathfrak{C})\to D$
that satisfies every constraint in $\mathfrak{C}$, i.e.
$P(v_{1},\dotsc,v_{k})\in\mathfrak{C}$ implies $(h(v_{1}),\dotsc,h(v_{k}))\in
P^{D}$. We then call $h$ a _solution_ of $\mathfrak{C}$. The _constraint
satisfaction problem_ for $\mathfrak{D}$, denoted
$\operatorname{CSP}(\mathfrak{D})$, is the decision problem asking whether a
finite constraint system $\mathfrak{C}$ over $\mathfrak{D}$ is satisfiable.
The problem $\operatorname{CSP}(\mathfrak{Q})$ is in P, since satisfiability
can be reduced to ${<}$-cycle detection; for example, the 3-clique
$\\{x_{1}<x_{2},\ x_{2}<x_{3},\ x_{3}<x_{1}\\}$ (using infix notation for $<$)
is unsatisfiable over $\mathfrak{Q}$.

To ensure that reasoning in the extension of $\mathcal{ALC}$ with concrete
domain restrictions is decidable, we impose further properties on
$\mathfrak{D}$ regarding its relations and the compositionality of its CSP for
finite and countable constraint systems. We say that $\mathfrak{D}$ is a
_patchwork_ if it satisfies the following conditions:111[5] originally used
only JEPD (jointly exhaustive, pairwise disjoint) and AP (amalgamation
property). JD (jointly diagonal) was later added by [9].

JEPD

for all $k\geq 1$, either $\mathfrak{D}$ has no $k$-ary relation, or $D^{k}$
is partitioned by all $k$-ary relations;

JD

there is a quantifier-free, equality-free first-order formula over the
signature of $\mathfrak{D}$ that defines the equality relation $=$ between two
elements of $\mathfrak{D}$;

AP

if $\mathfrak{B}$, $\mathfrak{C}$ are constraint systems and
$P(v_{1},\dotsc,v_{k})\in\mathfrak{B}\;\text{iff}\;P(v_{1},\dotsc,v_{k})\in\mathfrak{C}$
holds for all $v_{1},\dotsc,v_{k}\in V(\mathfrak{B})\cap V(\mathfrak{C})$ and
all $k$-ary predicates $P$ over $\mathfrak{D}$, then $\mathfrak{B}$ and
$\mathfrak{C}$ are satisfiable iff $\mathfrak{B}\cup\mathfrak{C}$ is
satisfiable.

If $\mathfrak{D}$ is a patchwork, we call a constraint system $\mathfrak{C}$
_complete_ if, for all $k\in\mathbb{N}$, either $\mathfrak{D}$ has no $k$-ary
predicates, or for all $v_{1},\dotsc,v_{k}\in V(\mathfrak{C})$ there is
exactly one $k$-ary predicate $P$ over $\mathfrak{D}$ such that
$P(v_{1},\dotsc,v_{k})\in\mathfrak{C}$. The concrete domain $\mathfrak{D}$ is
_homomorphism $\omega$-compact_ if a countable constraint system
$\mathfrak{C}$ over $\mathfrak{D}$ is satisfiable whenever every finite
constraint system $\mathfrak{C}^{\prime}\subseteq\mathfrak{C}$ is satisfiable.
We now introduce our definition of ExpTime-$\omega$-admissible concrete
domains, which differs from the definitions of $\omega$-admissibility [5, 9]
in that we require $\operatorname{CSP}(\mathfrak{D})$ to be decidable in
exponential time instead of simply decidable.

######  Definition 1.

A concrete domain $\mathfrak{D}$ is _ExpTime -$\omega$-admissible_ if

  * •

$\mathfrak{D}$ has a finite signature,

  * •

$\mathfrak{D}$ is a patchwork,

  * •

$\mathfrak{D}$ is homomorphism $\omega$-compact, and

  * •

$\operatorname{CSP}(\mathfrak{D})$ is decidable in exponential time.

Requiring the signature of $\mathfrak{D}$ to be finite is necessary to ensure
decidability of $\mathcal{ALC}(\mathfrak{D})$ [9]. In Section 4, we will also
consider concrete domains $\mathfrak{D}$ that are _homogeneous_ , that is,
every isomorphism between finite substructures of $\mathfrak{D}$ can be
extended to an isomorphism from $\mathfrak{D}$ to itself. All properties we
have defined here are satisfied by the three examples of Allen’s interval
relations, RCC8, and $\mathfrak{Q}$, as they are _finitely bounded_
homogeneous structures, which are $\omega$-admissible and have CSPs whose
complexity is at most NP (see [9] for details).

Ontologies with Concrete Domain Constraints. We assume the reader to be
familiar with the standard description logic $\mathcal{ALC}$ [12]. To use a
concrete domain $\mathfrak{D}$ in $\mathcal{ALC}$ axioms, we introduce a set
of _concrete features_ $\mathsf{N_{F}}$, where each $f\in\mathsf{N_{F}}$ is
interpreted as a _partial_ function
$f^{\mathcal{I}}\colon\Delta^{\mathcal{I}}\to D$ in an interpretation
$\mathcal{I}$. A _feature path_ is of the form $r_{1}\dots r_{n}f$, where
$r_{1},\dots,r_{n}\in\mathsf{N_{R}}$ are role names and $f\in\mathsf{N_{F}}$.
The semantics of such a path is given by a function

$(r_{1}\dots
r_{n}f)^{\mathcal{I}}(d)\coloneqq\big{\\{}f^{\mathcal{I}}(e)\mid(d,e)\in
r_{1}^{\mathcal{I}}\circ\dots\circ
r_{n}^{\mathcal{I}}\;\text{and}\;f^{\mathcal{I}}(e)\;\text{is
defined}\big{\\}}$

that assigns to each domain element the set of all $f$-values of elements $e$
reachable via the role chain $r_{1}\dots r_{n}$ (which may be empty if there
is no such $e$, or if $f^{\mathcal{I}}(e)$ is always undefined). In a slight
abuse of notation, we allow the case where $n=0$, i.e. $f$ can be seen as both
a feature and a feature path, with slightly different, but equivalent
semantics (that is, a partial function vs. a set-valued function that may
produce either a singleton set or the empty set).
_$\mathcal{ALC}(\mathfrak{D})$ concepts_ are defined similarly to
$\mathcal{ALC}$ concepts, but can additionally use the following concept
constructor: A _concrete domain restriction_ (or simply _CD-restriction_) is
of the form $\exists p_{1},\dots,p_{k}.P$ or $\forall p_{1},\dots,p_{k}.P$,
where $p_{1},\dots,p_{k}$ are feature paths and $P$ is a $k$-ary predicate,
with the semantics

$\displaystyle(\exists p_{1},\dotsc,p_{k}.P)^{\mathcal{I}}$
$\displaystyle\coloneqq\big{\\{}d\in\Delta^{\mathcal{I}}\mid\text{there
are}\;c_{i}\in
p_{i}^{\mathcal{I}}(d)\;\text{for}\;i=1,\dotsc,k\;\text{s.t.}\;(c_{1},\dots,c_{k})\in
P^{D}\big{\\}},$ $\displaystyle(\forall p_{1},\dots,p_{k}.P)^{\mathcal{I}}$
$\displaystyle\coloneqq\big{\\{}d\in\Delta^{\mathcal{I}}\mid\text{if}\;c_{i}\in
p_{i}^{\mathcal{I}}(d)\;\text{for}\;i=1,\dotsc,k,\;\text{then}\;(c_{1},\dots,c_{k})\in
P^{D}\big{\\}}.$

An _$\mathcal{ALC}(\mathfrak{D})$ ontology_
${\mathcal{O}}={\mathcal{A}}\cup{\mathcal{T}}$ consists of an _ABox_
$\mathcal{A}$ and a _TBox_ $\mathcal{T}$ over $\mathcal{ALC}(\mathfrak{D})$
concepts.

Note that we explicitly consider $\mathcal{ALC}(\mathfrak{D})$ and not
$\mathcal{ALCF}(\mathfrak{D})$, i.e. we do not allow functional roles, in
contrast to other definitions from the literature [1, 5]. In the literature,
feature paths are either restricted to contain only functional roles, or to
have a length of at most 2, (compare with [2, 5]). Consequently, we restrict
ourselves to feature paths of length $\leq 2$, that is, assume that they are
of the form $f$ or $rf$. We are not aware of any work that considers feature
paths over non-functional roles of length longer than 2, and leave the
investigation of this case for future work. Without loss of generality, we can
assume that universal CD-restrictions are not used in concepts, because we can
express $\forall p_{1},\dots,p_{k}.P$ as $\lnot\exists
p_{1},\dots,p_{k}.P_{1}\sqcap\dots\sqcap\lnot\exists p_{1},\dots,p_{k}.P_{m}$,
where $P_{1},\dots,P_{m}$ are all $k$-ary predicates of $\mathfrak{D}$ except
for $P$ (the union of these predicates is equivalent to the complement of $P$
due to JEPD, and there are only finitely many of them since the signature is
assumed to be finite). We can additionally assume that concepts do not contain
value restrictions $\forall r.C$ or disjunctions $C\sqcup D$ since they can be
expressed using only negation, conjunction and existential restriction.

##  3 Consistency in $\mathcal{ALC}(\mathfrak{D})$

Let now $\mathfrak{D}$ be a fixed ExpTime-$\omega$-admissible concrete domain,
${\mathcal{O}}={\mathcal{A}}\cup{\mathcal{T}}$ be an
$\mathcal{ALC}(\mathfrak{D})$ ontology, and $\mathcal{M}$ be the set of all
subconcepts appearing in $\mathcal{O}$ and their negations. For the type
elimination algorithm, we start by defining the central notion of _types_ ,
which is standard.

######  Definition 2.

A set $t\subseteq{\mathcal{M}}$ is a _type_ w.r.t. $\mathcal{O}$ if it
satisfies the following properties:

  * •

if $C\sqsubseteq D\in{\mathcal{T}}$ and $C\in t$, then $D\in t$;

  * •

if $\top\in{\mathcal{M}}$, then $\top\in t$;

  * •

if $\neg D\in{\mathcal{M}}$, then $D\in t$ iff $\neg D\notin t$;

  * •

if $D\sqcap D^{\prime}\in{\mathcal{M}}$, then $D\sqcap D^{\prime}\in t$ iff
$D\in t$ and $D^{\prime}\in t$.

Given a model $\mathcal{I}$ of $\mathcal{O}$ and an individual
$d\in\Delta^{{\mathcal{I}}}$, the _type of $d$_ w.r.t. $\mathcal{O}$ is the
set

$t_{{\mathcal{I}}}(d):=\big{\\{}C\in{\mathcal{M}}\mid d\in
C^{{\mathcal{I}}}\big{\\}}.$

Clearly, $t_{{\mathcal{I}}}(d)$ satisfies the four conditions required to be a
type w.r.t. $\mathcal{O}$. We use this connection between individuals and
types to define _augmented types_ that represent the relationship between an
individual, its role successors, and the CD-restrictions that ought to be
satisfied. Hereafter, let $n_{\mathsf{ex}}$ be the number of existential
restrictions $\exists r.C$ in $\mathcal{M}$, and $n_{\mathsf{cd}}$ the number
of CD-restrictions $\exists p_{1},\dotsc,p_{k}.P$ in $\mathcal{M}$. The
maximal arity of predicates $P$ occurring in $\mathcal{M}$ is denoted by New A
Rev., and we define $n_{\mathcal{O}}:=n_{\mathsf{ex}}+n_{\mathsf{cd}}\cdot{\rm
NewARev.}$. Intuitively, each non-negated existential restriction in a type
needs a successor (and associated type) to be realized, while CD-restrictions
may require New A Rev.role successors to fulfill a certain constraint.
Therefore, $n_{\mathcal{O}}$ is an upper bound on the number of successors
needed to satisfy all the non-negated restrictions occurring in a type $t$
w.r.t. $\mathcal{O}$.

Given a type $t_{0}$, we define a constraint system associated with a sequence
of types $t_{1},\dotsc,t_{n_{\mathcal{O}}}$ representing the role successors
of a domain element with type $t_{0}$. This system contains a variable $f^{i}$
for each feature $f$ of an individual with type $t_{i}$ in order to express
the relevant CD-restrictions. Concrete features that are not represented in
this system can remain undefined since their values are irrelevant for
satisfying the CD-restrictions.

######  Definition 3.

A _local system_ for a type $t_{0}$ w.r.t. a sequence of types
$t_{1},\dotsc,t_{n_{\mathcal{O}}}$ is a complete constraint system
$\mathfrak{C}$ for which there exists a _successor function_
$\operatorname{\mathsf{succ}}\colon\mathsf{N_{R}}({\mathcal{O}})\to\mathcal{P}(\\{1,\dots,n_{\mathcal{O}}\\})$,
such that, for all $\exists p_{1},\dots,p_{k}.P\in{\mathcal{M}}$, the
following condition holds:

$\exists p_{1},\dotsc,p_{k}.P\in t_{0}$ iff there is
$P(v_{1},\dotsc,v_{k})\in\mathfrak{C}$ for some variables $v_{1},\dotsc,v_{k}$
such that

$v_{i}=\begin{cases}f^{0}&\text{if $p_{i}=f$, or}\\\ f^{j}&\text{if $p_{i}=rf$
and $j\in\operatorname{\mathsf{succ}}(r)$.}\end{cases}$

We use a _sequence_ instead of a _set_ of types for the role successors, since
there can be TBoxes that require the existence of two successors with the same
type that only differ in their feature values. For example, for the consistent
ontology ${\mathcal{O}}:=\\{\top\sqsubseteq\exists rf,rf.{<}\\}$ over
$\mathfrak{Q}=(\mathbb{Q},{<},{=},{>})$, we have ${\mathcal{M}}=\\{\top,\
\neg\top,\ \exists rf,rf.{<},\ \neg\exists rf,rf.{<}\\}$, and the only type is
$t=\\{\top,\ \exists rf,rf.{<}\\}$. Any $r$-successors witnessing $\exists
rf,rf.{<}$ for an element in a model of $\mathcal{O}$ have the same type $t$.
However, we cannot express the restriction on their $f$-values by the
(unsatisfiable) constraint ${<}(f^{t},f^{t})$, but need to consider two copies
$t_{1},t_{2}$ of $t$ to get the (satisfiable) constraint ${<}(f^{1},f^{2})$.

To merge the local systems associated to types of adjacent elements in a
model, we introduce the following operation. For two local systems
$\mathfrak{C},\mathfrak{C}^{\prime}$, the _merged system_
$\mathfrak{C}\mathop{{\vartriangleleft}_{i}}\mathfrak{C}^{\prime}$ is obtained
as the union of $\mathfrak{C}$ and $\mathfrak{C}^{\prime}$ where we identify
all features with index $i$ in $\mathfrak{C}$ with those of index $0$ in
$\mathfrak{C}^{\prime}$, while keeping the remaining variables separate.
Formally, we first replace all variables $f^{j}$ in $\mathfrak{C}^{\prime}$ by
fresh variables $f^{j^{\prime}}$ and subsequently replace the variables
$f^{0^{\prime}}$ in $\mathfrak{C}^{\prime}$ by $f^{i}$.

######  Definition 4.

An _augmented type_ for $\mathcal{O}$ is a tuple
$\mathfrak{t}:=(t_{0},\dotsc,t_{n_{\mathcal{O}}},\mathfrak{C}_{\mathfrak{t}})$
where $t_{0},\dotsc,t_{n_{\mathcal{O}}}$ are types for $\mathcal{O}$ and
$\mathfrak{C}_{\mathfrak{t}}$ is a local system for $t_{0}$ w.r.t.
$t_{1},\dotsc,t_{n_{\mathcal{O}}}$. The _root_ of $\mathfrak{t}$ is
$\operatorname{\mathsf{root}}(\mathfrak{t}):=t_{0}$. The augmented type
$\mathfrak{t}$ is _locally realizable_ if $\mathfrak{C}_{\mathfrak{t}}$ has a
solution and if there exists a successor function
$\operatorname{\mathsf{succ}}_{\mathfrak{t}}$ for
$\mathfrak{C}_{\mathfrak{t}}$ s.t. for all concepts $\exists
r.C\in{\mathcal{M}}$, it holds that

$\exists r.C\in\operatorname{\mathsf{root}}(\mathfrak{t})$ iff there is
$i\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r)$ such that $C\in t_{i}$.

An augmented type $\mathfrak{t}^{\prime}$ then _patches_ $\mathfrak{t}$ at
$i\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r)$ if
$\operatorname{\mathsf{root}}(\mathfrak{t}^{\prime})=t_{i}$ and the system
$\mathfrak{C}_{\mathfrak{t}}\mathop{{\vartriangleleft}_{i}}\mathfrak{C}_{\mathfrak{t}^{\prime}}$
has a solution. A set of augmented types $\mathbb{T}$ _patches_ the locally
realizable $\mathfrak{t}$ if, for every role name $r$ and every
$i\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r)$, there is a
$\mathfrak{t}^{\prime}\in\mathbb{T}$ that patches $\mathfrak{t}$ at $i$.

For the ontology $\mathcal{O}$ introduced above, we have $n_{\mathcal{O}}=2$
since $\mathcal{M}$ only contains one CD-restriction over a binary predicate.
Using infix notation, all augmented types
$\mathfrak{t}=(t,t,t,\mathfrak{C}_{\mathfrak{t}})$ for $\mathcal{O}$ are such
that $\mathfrak{C}_{\mathfrak{t}}$ contains the constraints $f^{i}=f^{i}$ for
$i=0,1,2$, and either $f^{1}<f^{2}$ or $f^{2}<f^{1}$. There are augmented
types $\mathfrak{t}$ that are not locally realizable, for instance if
$\mathfrak{C}_{\mathfrak{t}}$ contains $f^{0}=f^{1}$, $f^{0}=f^{2}$, and
$f^{1}<f^{2}$. On the other hand, there is a locally realizable augmented type
using the constraints $f^{0}<f^{1}$, $f^{1}<f^{2}$, and $f^{0}<f^{2}$, which
can patch itself both at $i\in\\{1,2\\}$.

To additionally handle named individuals and concept and role assertions, we
introduce a structure $\mathfrak{t}_{\mathcal{A}}$ that describes all ABox
individuals and their connections simultaneously, similar to the common notion
of _precompletion_. The associated constraint system
$\mathfrak{C}_{\mathcal{A}}$ now uses variables $f^{a,i}$ indexed with
individual names $a$ in addition to numbers $i$.

######  Definition 5.

An _ABox type_ for $\mathcal{O}$ is a tuple
$\mathfrak{t}_{\mathcal{A}}:=\big{(}(\mathfrak{t}_{a})_{a\in\mathsf{N_{I}}({\mathcal{A}})},{\mathcal{A}}_{R},\mathfrak{C}_{\mathcal{A}}\big{)}$,
where $\mathfrak{t}_{a}$ are augmented types, ${\mathcal{A}}_{R}$ is a set of
role assertions over $\mathsf{N_{I}}({\mathcal{A}})$ and
$\mathsf{N_{R}}({\mathcal{O}})$, and $\mathfrak{C}_{\mathcal{A}}$ is a
complete and satisfiable constraint system such that, for every
$a\in\mathsf{N_{I}}({\mathcal{A}})$,

  * •

for every concept assertion $C(a)\in{\mathcal{A}}$, we have
$C\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$;

  * •

for every role assertion $r(a,b)\in{\mathcal{A}}$, we have
$r(a,b)\in{\mathcal{A}}_{R}$;

  * •

for every $\lnot\exists r.C\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$
and $r(a,b)\in{\mathcal{A}}_{R}$, we have
$C\notin\operatorname{\mathsf{root}}(\mathfrak{t}_{b})$;

  * •

for every
$P(f_{1}^{j_{1}},\dots,f_{k}^{j_{k}})\in\mathfrak{C}_{\mathfrak{t}_{a}}$, we
have $P(f_{1}^{a,j_{1}},\dots,f_{k}^{a,j_{k}})\in\mathfrak{C}_{\mathcal{A}}$;

  * •

for every $\lnot\exists
p_{1},\dots,p_{k}.P\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$, there
can be no $P(v_{1},\dots,v_{k})\in\mathfrak{C}_{\mathcal{A}}$ with

$v_{i}=\begin{cases}f^{a,0}&\text{if $p_{i}=f$,}\\\ f^{b,0}&\text{if
$p_{i}=rf$ and $r(a,b)\in{\mathcal{A}}_{R}$, or}\\\ f^{a,j}&\text{if
$p_{i}=rf$ and
$j\in\operatorname{\mathsf{succ}}_{\mathfrak{t}_{a}}(r)$;}\end{cases}$

Positive occurrences of existential role or CD-restrictions in the ABox type
do not need to be handled, as these are satisfied by anonymous successors
described in the augmented types $\mathfrak{t}_{a}$.

###  3.1 The Type Elimination Algorithm

Algorithm 1 uses the introduced notions to check consistency of $\mathcal{O}$.

Algorithm 1 Elimination algorithm for consistency of
$\mathcal{ALC}(\mathfrak{D})$ ontologies

1:An $\mathcal{ALC}(\mathfrak{D})$ ontology
${\mathcal{O}}={\mathcal{A}}\cup{\mathcal{T}}$

2:consistent if $\mathcal{O}$ is consistent, and inconsistent otherwise

3:${\mathcal{M}}\leftarrow\text{all subconcepts occurring in {$\mathcal{O}$}
and their negations}$

4:$\mathbb{T}\leftarrow\text{all augmented types for~{}{$\mathcal{O}$}}$

5:while there is $\mathfrak{t}\in\mathbb{T}$ that is not locally realizable or
not patched by $\mathbb{T}$ do

6: $\mathbb{T}\leftarrow\mathbb{T}\setminus\\{\mathfrak{t}\\}$

7:if there is an ABox type $\mathfrak{t}_{\mathcal{A}}$ for $\mathcal{O}$ with
$\mathfrak{t}_{a}\in\mathbb{T}$ for all $a\in\mathsf{N_{I}}({\mathcal{A}})$
then

8: return consistent

9:else

10: return inconsistent

######  Lemma 6 (Soundness).

If Algorithm 1 returns consistent, then $\mathcal{O}$ is consistent.

###### Proof.

Assume that $\mathbb{T}$ and
$\mathfrak{t}_{A}=((\mathfrak{t}_{a})_{a\in\mathsf{N_{I}}({\mathcal{A}})},{\mathcal{A}}_{R},\mathfrak{C}_{\mathcal{A}})$
are obtained after a successful run of the elimination algorithm. We use them
to define a forest-shaped interpretation $\mathcal{I}$ that is a model of
$\mathcal{O}$. The domain of this model consists of pairs $(a,w)$, where
$a\in\mathsf{N_{I}}$ designates a tree-shaped part of $\mathcal{I}$ whose
structure is given by the words $w$ over the alphabet
$\Sigma:=\mathbb{T}\times\\{0,\dotsc,n_{\mathcal{O}}\\}$. A pair
$(\mathfrak{t},i)\in\Sigma$ describes an augmented type and the position
relative to the restriction that this augmented type fulfills w.r.t. its
parent in the tree. For a word $w\in\Sigma^{+}$, we define
$\operatorname{\mathsf{end}}(w):=\mathfrak{t}$ if $(\mathfrak{t},j)$ occurs at
the last position of $w$ for some $j\in\\{0,\dotsc,n_{\mathcal{O}}\\}$.

We start defining the domain of $\mathcal{I}$ by $\Delta^{0}:=\\{(a,w_{a})\mid
a\in\mathsf{N_{I}}({\mathcal{A}}),\ w_{a}:=(\mathfrak{t}_{a},0)\\}$. Observe
that $w_{a}\in\Sigma$, since $\mathfrak{t}_{a}\in\mathbb{T}$. Assuming that
$\Delta^{m}$ is defined, we define $\Delta^{m+1}$ based on $\Delta^{m}$, and
subsequently construct the domain of $\mathcal{I}$ as the union of all sets
$\Delta^{m}$. Given $(a,w)\in\Delta^{m}$ with
$\operatorname{\mathsf{end}}(w)=\mathfrak{t}$, we observe that $\mathfrak{t}$
must have a successor function $\operatorname{\mathsf{succ}}_{\mathfrak{t}}$
s.t. for every $i\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r)$, there is
an augmented type $\mathfrak{u}^{i}\in\mathbb{T}$ patching $\mathfrak{t}$ at
$i$, as otherwise $\mathfrak{t}$ would have been eliminated from $\mathbb{T}$.
We use these augmented types to define
$\Delta_{r}^{m+1}[a,w]:=\\{(a,w\cdot(\mathfrak{u}^{i},i))\mid
i\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r)\\}$ to then obtain

$\Delta^{m+1}:=\Delta^{m}\cup\bigcup\big{\\{}\Delta_{r}^{m+1}[a,w]\mid(a,w)\in\Delta^{m}\;\text{and}\;r\in\mathsf{N_{R}}\big{\\}}$

and set $\Delta^{{\mathcal{I}}}:=\bigcup_{m\in\mathbb{N}}\Delta^{m}$. The
interpretation of individual, concept, and role names over $\mathcal{I}$ is
given by

$\displaystyle a^{\mathcal{I}}$ $\displaystyle:=(a,w_{a}),$ $\displaystyle
A^{{\mathcal{I}}}$
$\displaystyle:=\big{\\{}(a,w)\in\Delta^{{\mathcal{I}}}\mid\operatorname{\mathsf{end}}(w)=\mathfrak{t}\;\text{and}\;A\in\operatorname{\mathsf{root}}(\mathfrak{t})\big{\\}},$
$\displaystyle r^{{\mathcal{I}}}$
$\displaystyle:=\big{\\{}((a,w_{a}),(b,w_{b}))\mid
r(a,b)\in{\mathcal{A}}_{R}\big{\\}}\cup{}$
$\displaystyle\phantom{{}:={}}\big{\\{}((a,w),(a,w^{\prime}))\mid(a,w)\in\Delta^{m}\;\text{and}\;(a,w^{\prime})\in\Delta^{m+1}_{r}[a,w]\;\text{with}\;m\in\mathbb{N}\big{\\}}.$

Defining the interpretation of feature names in $\mathcal{I}$ requires more
work. Given $(a,w)\in\Delta^{{\mathcal{I}}}$ with
$\operatorname{\mathsf{end}}(w)=\mathfrak{t}$, let $\mathfrak{C}_{a,w}$ be the
constraint system obtained by replacing every variable $f^{0}$ in
$\mathfrak{C}_{\mathfrak{t}}$ with $f^{a,w}$ and every other variable $f^{i}$
in $\mathfrak{C}_{\mathfrak{t}}$ with $f^{a,u}$, where $u\in\Sigma^{+}$ is the
unique word of the form $w\cdot(\mathfrak{t}^{\prime},i)$ for which
$(a,u)\in\Delta^{{\mathcal{I}}}$. Correspondingly, let
$\mathfrak{C}_{\mathcal{A}}^{0}$ be the result of replacing all variables
$f^{a,0}$ in $\mathfrak{C}_{\mathcal{A}}$ by $f^{a,w_{a}}$ and $f^{a,i}$ by
$f^{a,u}$, where $u$ is the unique word of the form
$w_{a}\cdot(\mathfrak{t}^{\prime},i)$ for which
$(a,u)\in\Delta^{\mathcal{I}}$. For $m\in\mathbb{N}$, let $\mathfrak{C}^{m}$
be the union of $\mathfrak{C}_{\mathcal{A}}^{0}$ and all constraint systems
$\mathfrak{C}_{a,w}$ for which $(a,w)\in\Delta^{m}$. The proofs of the
following claims can be found in the appendix.

######  Claim 1.

For every $m\in\mathbb{N}$, the constraint system $\mathfrak{C}^{m}$ has a
solution.

Using this claim, we show how to define an interpretation of feature names for
$\mathcal{I}$. Let $\mathfrak{C}^{{\mathcal{I}}}$ be the union of all systems
$\mathfrak{C}^{m}$ for $m\in\mathbb{N}$. Every finite system
$\mathfrak{B}\subseteq\mathfrak{C}^{{\mathcal{I}}}$ is also a subsystem of
$\mathfrak{C}^{m}$ for some $m\in\mathbb{N}$. Since $\mathfrak{C}^{m}$ has a
solution, it follows that $\mathfrak{B}$ has a solution. Every finite
subsystem of $\mathfrak{C}^{{\mathcal{I}}}$ has a solution; since
$\mathfrak{D}$ has the homomorphism $\omega$-compactness property, we infer
that $\mathfrak{C}^{{\mathcal{I}}}$ has a solution $h^{{\mathcal{I}}}$. Using
this solution, we define for every feature name $f$ the interpretation
$f^{{\mathcal{I}}}(a,w):=h^{{\mathcal{I}}}(f^{a,w})$ if $f^{a,w}$ occurs in
$\mathfrak{C}^{{\mathcal{I}}}$, and leave it undefined otherwise.

######  Claim 2.

If $C\in{\mathcal{M}}$ and $(a,w)\in\Delta^{{\mathcal{I}}}$ with
$\operatorname{\mathsf{end}}(w)=\mathfrak{t}$, then
$C\in\operatorname{\mathsf{root}}(\mathfrak{t})$ iff $(a,w)\in
C^{{\mathcal{I}}}$.

By this claim and Definition 2, we know that $\mathcal{I}$ is a model of
$\mathcal{T}$. By Definition 5 we obtain that for each $C(a)\in{\mathcal{A}}$,
we have $C\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$, and thus
$a^{\mathcal{I}}=(a,w_{a})=(a,(\mathfrak{t}_{a},0))\in C^{\mathcal{I}}$.
Similarly, whenever $r(a,b)\in{\mathcal{A}}$, then
$r(a,b)\in{\mathcal{A}}_{R}$, and thus
$(a^{\mathcal{I}},b^{\mathcal{I}})=((a,w_{a}),(b,w_{b}))\in r^{\mathcal{I}}$
by the construction of $\mathcal{I}$. Therefore, we conclude that
$\mathcal{I}$ is also a model of $\mathcal{A}$, and thus of $\mathcal{O}$. ∎

######  Lemma 7 (Completeness).

If $\mathcal{O}$ is consistent, then Algorithm 1 returns consistent.

###### Proof.

Let $\mathcal{I}$ be a model of $\mathcal{O}$ and define the set
$T_{{\mathcal{I}}}$ of all types that are realized in $\mathcal{I}$, that is,

$T_{{\mathcal{I}}}:=\big{\\{}t_{{\mathcal{I}}}(d)\mid
d\in\Delta^{{\mathcal{I}}}\big{\\}}.$

Given that $\mathcal{I}$ is a model of $\mathcal{O}$, every element of
$T_{{\mathcal{I}}}$ is a type according to Definition 2. Using the elements of
$T_{{\mathcal{I}}}$, we construct a set
$\mathbb{T}_{{\mathcal{I}}}:=\\{\mathfrak{t}_{{\mathcal{I}}}(d)\mid
d\in\Delta^{{\mathcal{I}}}\\}$ of augmented types. For any domain element
$d\in\Delta^{{\mathcal{I}}}$, we build the augmented type
$\mathfrak{t}_{{\mathcal{I}}}(d)=(t_{0},\dotsc,t_{n_{\mathcal{O}}},\mathfrak{C}_{d})$
as follows.

First, we set $t_{0}:=t_{{\mathcal{I}}}(d)\in T_{{\mathcal{I}}}$. Assuming
that $\exists r_{i}.C_{i}\in{\mathcal{M}}$ for $i=1,\dotsc,n_{\mathsf{ex}}$,
we select types $t_{1},\dotsc,t_{n_{\mathsf{ex}}}$ to add to $\mathfrak{t}$
that realize the (possibly negated) existential role restrictions occurring in
$t_{0}$. If $\exists r_{i}.C_{i}\in t_{0}$, then we can select $t_{i}$ as the
type of an $r$-successor $d^{\prime}$ of $d$ such that $d^{\prime}\in
C_{i}^{{\mathcal{I}}}$; otherwise, we pick $t_{i}$ as the type of an arbitrary
element in $\Delta^{{\mathcal{I}}}$.

Next, we assume that $\exists
p_{1}^{i},\dotsc,p_{k}^{i}.P_{i}\in{\mathcal{M}}$ for
$i=1,\dotsc,n_{\mathsf{cd}}$ and define the function
$\mathsf{off}(i,j):=n_{\mathsf{ex}}+(i-1)\cdot{\rm NewARev.}+j$ to be able to
refer to the $j$-th path in the $i$-th CD-restriction above. We select types
$t_{\mathsf{off}(i,1)},\dotsc,t_{\mathsf{off}(i,{\rm NewARev.})}$ that realize
the (possibly negated) existential CD-restrictions occurring in $t_{0}$ for
$i=1,\dotsc,n_{\mathsf{cd}}$. If $\exists p^{i}_{1},\dotsc,p^{i}_{k}.P_{i}\in
t_{0}$, then there exist values $v^{i}_{j}\in{(p^{i}_{j})}^{{\mathcal{I}}}(d)$
for $j=1,\dotsc,k$ such that $(v^{i}_{1},\dotsc,v^{i}_{k})\in P^{D}$. If
$p_{j}=rf$ holds for some feature name $f$ and some role name $r$, let
$t_{\mathsf{off}(i,j)}$ be the type of an $r$-successor $d^{\prime}$ of $d$
such that $v_{j}^{i}=f^{{\mathcal{I}}}(d)$. For every $j=1,\dotsc,{\rm
NewARev.}$ for which $t_{\mathsf{off}(i,j)}$ has not been selected this way,
let $t_{\mathsf{off}(i,j)}$ be the type of an arbitrary individual in
$\Delta^{\mathcal{I}}$. Similarly, if $\exists
p^{i}_{1},\dotsc,p^{i}_{k}.P_{i}\notin t_{0}$ then we set
$t_{\mathsf{off}(i,j)}$ be the type of an arbitrary individual in
$\Delta^{\mathcal{I}}$ for $j=1,\dotsc,{\rm NewARev.}$.

The two processes described in the two previous paragraphs yield a sequence of
types $t_{1},\dotsc,t_{n_{\mathcal{O}}}$ that occur in $T_{{\mathcal{I}}}$ and
can thus be associated to individuals
$d_{1},\dotsc,d_{n_{\mathcal{O}}}\in\Delta^{{\mathcal{I}}}$. Using these
individuals, we define the local system associated to our augmented type
$\mathfrak{t}_{{\mathcal{I}}}(d)$. First, we define the constraint system
$\mathfrak{C}_{d}$ that contains the constraint
$P\big{(}f_{1}^{i_{1}},\dotsc,f_{k}^{i_{k}}\big{)}$ iff
$\big{(}f_{1}^{{\mathcal{I}}}(d_{i_{1}}),\dotsc,f_{k}^{{\mathcal{I}}}(d_{i_{k}})\big{)}\in
P^{D}$ for all $i_{1},\dotsc,i_{k}\in\\{0,\dotsc,n_{\mathcal{O}}\\}$. We
associate to this constraint system a successor function
$\operatorname{\mathsf{succ}}_{d}$ that assigns to $r\in\mathsf{N_{R}}$ all
$i\in\\{1,\dotsc,n_{\mathcal{O}}\\}$ for which $d_{i}$ is an $r$-successor of
$d$. This concludes our definition of $\mathfrak{t}_{{\mathcal{I}}}(d)$ for
$d\in\Delta^{{\mathcal{I}}}$, and thus of $\mathbb{T}_{{\mathcal{I}}}$.

######  Claim 3.

Every augmented type in $\mathbb{T}_{{\mathcal{I}}}$ is locally realizable and
patched in $\mathbb{T}_{{\mathcal{I}}}$.

Therefore, no augmented type $\mathfrak{t}\in\mathbb{T}_{{\mathcal{I}}}$ is
eliminated during a run of Algorithm 1, and so
$\mathbb{T}_{\mathcal{I}}\subseteq\mathbb{T}$. We further deduce that
$\mathbb{T}$ cannot become empty, since $T_{{\mathcal{I}}}$ is non-empty.
Using $\mathbb{T}_{{\mathcal{I}}}$ together with our model $\mathcal{I}$ of
${\mathcal{O}}$ we derive an ABox type
$\mathfrak{t}_{{\mathcal{A}}}^{{\mathcal{I}}}=\big{(}(\mathfrak{t}_{a})_{a\in\mathsf{N_{I}}({\mathcal{A}})},{\mathcal{A}}_{R},\mathfrak{C}_{\mathcal{A}}\big{)}$
for ${\mathcal{O}}$. We define each $\mathfrak{t}_{a}$,
$a\in\mathsf{N_{I}}({\mathcal{A}})$, as
$\mathfrak{t}_{a}:=\mathfrak{t}_{{\mathcal{I}}}(a^{{\mathcal{I}}})\in\mathbb{T}_{{\mathcal{I}}}$.
Assuming that $d_{a,i}$ is the domain element used to establish the $i$-th
type in $\mathfrak{t}_{a}$ for $i\in\\{0,\dotsc,n_{\mathcal{O}}\\}$, we define
the constraint system $\mathfrak{C}_{\mathcal{A}}$ s.t.

$P(f_{1}^{a_{1},i_{1}},\dotsc,f_{k}^{a_{k},i_{k}})\in\mathfrak{C}_{\mathcal{A}}\;\text{iff}\;(f_{1}^{{\mathcal{I}}}(d_{a_{1},i_{1}}),\dotsc,f_{k}^{{\mathcal{I}}}(d_{a_{k},i_{k}}))\in
P^{D}.$

Finally, we define the set ${\mathcal{A}}_{R}$ to consist of all role
assertions $r(a,b)$ for which $a,b\in\mathsf{N_{I}}({\mathcal{A}})$,
$r\in\mathsf{N_{R}}({\mathcal{O}})$, and
$(a^{{\mathcal{I}}},b^{{\mathcal{I}}})\in r^{{\mathcal{I}}}$.

######  Claim 4.

The object $\mathfrak{t}_{{\mathcal{A}}}^{{\mathcal{I}}}$ is an ABox type for
$\mathcal{O}$ with $\mathfrak{t}_{a}\in\mathbb{T}_{{\mathcal{I}}}$ for all
$a\in\mathsf{N_{I}}({\mathcal{A}})$.

Thus, there is a suitable ABox type for $\mathcal{O}$, and Algorithm 1 returns
consistent. ∎

We can show in a standard way that Algorithm 1 runs in exponential time w.r.t.
$\mathcal{O}$ and obtain the following theorem (a detailed proof can be found
in the appendix).

######  Theorem 8.

Let $\mathfrak{D}$ be an ExpTime-$\omega$-admissible concrete domain. Then,
the consistency problem for $\mathcal{ALC}(\mathfrak{D})$ ontologies is
ExpTime-complete.

##  4 Concrete Domain Assertions

Beside using concrete domain restrictions on the concept level, we may want to
use feature and predicate assertions in the ABox to either assign a specific
value of a feature to some individual or directly constraint the values of
features of different individuals. Formally, a _feature assertion_ is of the
form $f(a,c)$, where $f\in\mathsf{N_{F}}$, $a\in\mathsf{N_{I}}$, and $c\in D$,
and it is satisfied by an interpretation $\mathcal{I}$ if
$f^{\mathcal{I}}(a^{\mathcal{I}})=c$. _Predicate assertions_ are of the form
$P\big{(}f_{1}(a_{1}),\dotsc,f_{k}(a_{k})\big{)}$, where $P$ is a $k$-ary
relation over $\mathfrak{D}$ and $f_{i}\in\mathsf{N_{F}}$,
$a_{i}\in\mathsf{N_{I}}$ for $i=1,\dotsc,k$. An interpretation $\mathcal{I}$
satisfies such an assertion if
$\big{(}f_{1}^{{\mathcal{I}}}(a_{1}^{{\mathcal{I}}}),\dotsc,f_{k}^{{\mathcal{I}}}(a_{k}^{{\mathcal{I}}})\big{)}\in
P^{D}$. In our setting, we can simulate predicate assertions using concept and
role assertions, which leads to the following result.

######  Theorem 9.

For any ExpTime-$\omega$-admissible concrete domain $\mathfrak{D}$, ontology
consistency in $\mathcal{ALC}(\mathfrak{D})$ with predicate assertions is
ExpTime-complete.

###### Proof.

First, we show how to simulate CD-restrictions of the form $\exists
f.\top_{\mathfrak{D}}$ that describe all individuals $d$ in $\mathcal{I}$ for
which $f^{\mathcal{I}}(d)$ is defined. Although $\top_{\mathfrak{D}}$ may not
be a predicate of $\mathfrak{D}$, by JEPD and the fact that the signature of
$\mathfrak{D}$ is non-empty and finite, $\top_{\mathfrak{D}}$ can be expressed
as the disjunction of some $k$-ary predicates $P_{1},\dots,P_{m}$. This
implies that for every $d\in D$ there is exactly one $k$-ary predicate $P_{i}$
such that $(d,\dotsc,d)\in P_{i}^{D}$. Thus, we can write $\exists
f.\top_{\mathfrak{D}}$ equivalently as ${\exists
f,\dotsc,f.P_{1}}\sqcup{\dotsb}\sqcup{\exists f,\dotsc,f.P_{m}}$, where each
restriction $\exists f,\dots,f.P_{i}$ repeats $f$ for $k$ times.

Let now ${\mathcal{O}}={\mathcal{A}}\cup{\mathcal{T}}$ be an
$\mathcal{ALC}(\mathfrak{D})$ ontology with predicate assertions. We introduce
a fresh individual name $a^{*}$ and fresh role names $r_{a}$ for all
individual names $a\in\mathsf{N_{I}}({\mathcal{O}})$. The ontology
${\mathcal{O}}^{\prime}$ is then obtained from $\mathcal{O}$ by adding the
role assertions $r_{a}(a^{*},a)$ for all $a\in\mathsf{N_{I}}({\mathcal{O}})$,
and replacing all predicate assertions
$P\big{(}f_{1}(a_{1}),\dotsc,f_{k}(a_{k})\big{)}$ in $\mathcal{A}$ by the
concept assertions $(\exists f_{1}.\top_{\mathfrak{D}})(a_{1})$, …, $(\exists
f_{k}.\top_{\mathfrak{D}})(a_{k})$, and $(\forall
r_{a_{1}}f_{1},\dots,r_{a_{k}}f_{k}.P)(a^{*})$. Any model ${\mathcal{I}}$ of
${\mathcal{O}}^{\prime}$ satisfies $(c_{1},\dots,c_{k})\in P^{D}$ for all
possible values $c_{i}\in(r_{a_{i}}f_{i})^{\mathcal{I}}$, and thus in
particular for $c_{i}=f_{i}^{\mathcal{I}}(a_{i}^{\mathcal{I}})$, which shows
that $\mathcal{I}$ is also a model of $\mathcal{O}$. Conversely, from every
model $\mathcal{I}$ of $\mathcal{O}$ we obtain a model of
${\mathcal{O}}^{\prime}$ by choosing an arbitrary element
$d^{*}\in\Delta^{\mathcal{I}}$ for the interpretation of $a^{*}$ and adding
$(d^{*},a^{\mathcal{I}})$ to the interpretation of $r_{a}$ for every
individual name $a$. ∎

Feature assertions can also be simulated under certain conditions. For
concrete domains that contain _singleton_ predicates $=_{c}$ with
$(=_{c})^{D}=\\{c\\}\subseteq D$, we can express any feature assertion
$f(a,c)$ using the concept assertion $(\exists f.{=}_{c})(a)$. However, due to
its finite signature, $\mathfrak{D}$ can only contain finitely many such
predicates, and hence the feature assertions are restricted by the chosen
concrete domain. Due to the JD and JEPD conditions, it turns out that adding
feature assertions is actually _equivalent_ to adding singleton predicates in
the following sense. Here, an _additional singleton predicate_ $=_{c}$ is one
that is not part of $\mathfrak{D}$, but otherwise can be used in an ontology
with the same semantics as defined above; the proof can be found in the
appendix.

######  Theorem 10.

For an $\omega$-admissible concrete domain $\mathfrak{D}$, ontology
consistency in $\mathcal{ALC}(\mathfrak{D})$ with additional singleton
predicates can be polynomially reduced to ontology consistency in
$\mathcal{ALC}(\mathfrak{D})$ with feature assertions.

If we additionally require $\mathfrak{D}$ to be homogeneous, then we can show
that arbitrary feature assertions can already be expressed in ordinary
$\mathcal{ALC}(\mathfrak{D})$ ontologies.

######  Theorem 11.

For an ExpTime-$\omega$-admissible homogeneous concrete domain $\mathfrak{D}$,
ontology consistency in $\mathcal{ALC}(\mathfrak{D})$ with feature assertions
is ExpTime-complete.

###### Proof.

Due to Theorem 9, it suffices to provide a reduction to ontology consistency
with predicate assertions. Let ${\mathcal{O}}={\mathcal{A}}\cup{\mathcal{T}}$
be an $\mathcal{ALC}(\mathfrak{D})$ ontology containing feature assertions.
Let ${\mathcal{A}}^{\prime}$ be the ABox containing all concept and role
assertions from ${\mathcal{A}}$ and, in addition, all predicate assertions
$P(f_{1}(a_{1}),\dotsc,f_{k}(a_{k}))\in{\mathcal{A}}^{\prime}$ for all
combinations of feature assertions $f_{i}(a_{i},c_{i})\in{\mathcal{A}}$ with
$i=1,\dotsc,k$ for which $(c_{1},\dotsc,c_{k})\in P^{D}$ holds. The size of
${\mathcal{A}}^{\prime}$ is polynomial in the input, since the signature of
$\mathfrak{D}$ is fixed.

It is easy to see that every model of ${\mathcal{O}}$ is also a model of
${\mathcal{O}}^{\prime}:={\mathcal{A}}^{\prime}\cup{\mathcal{T}}$. Conversely,
let $\mathcal{I}$ be a model of ${\mathcal{O}}^{\prime}$ and let
$\mathfrak{D}_{\mathcal{A}}$, $\mathfrak{D}_{\mathcal{I}}$ be the finite
substructures of $\mathfrak{D}$ over the domains

$D_{\mathcal{A}}:=\\{c\mid f(a,c)\in{\mathcal{A}}\\}$ and
$D_{\mathcal{I}}:=\\{f^{{\mathcal{I}}}(a)\mid f(a,c)\in{\mathcal{A}}\\}$,

respectively. By definition of ${\mathcal{A}}^{\prime}$ and JEPD, we know that
$\big{(}f_{1}^{{\mathcal{I}}}(a_{1}^{\mathcal{I}}),\dotsc,f_{k}^{{\mathcal{I}}}(a_{k}^{\mathcal{I}})\big{)}\in
P^{D}$ iff $(c_{1},\dotsc,c_{k})\in P^{D}$, for all combinations of feature
assertions $f_{i}(a_{i},c_{i})$ in $\mathcal{A}$. By JD, this in particular
implies that
$f_{1}^{\mathcal{I}}(a_{1}^{\mathcal{I}})=f_{2}^{\mathcal{I}}(a_{2}^{\mathcal{I}})$
iff $f_{1}(a_{1},c),f_{2}(a_{2},c)\in{\mathcal{A}}$ for some value $c\in D$,
which means that the two substructures have the same number of elements.
Moreover, by the first equivalence, the mapping
$f^{{\mathcal{I}}}(a^{\mathcal{I}})\mapsto c$ for all $f(a,c)\in{\mathcal{A}}$
is an isomorphism between $\mathfrak{D}_{\mathcal{I}}$ and
$\mathfrak{D}_{\mathcal{A}}$. Since $\mathfrak{D}$ is homogeneous, there
exists an isomorphism $h\colon D\to D$ such that
$h(f^{{\mathcal{I}}}(a^{\mathcal{I}}))=c$ if $f(a,c)\in{\mathcal{A}}$.
Consequently, we define ${\mathcal{I}}^{\prime}$ from $\mathcal{I}$ by
changing the interpretation of feature names to
$f^{{\mathcal{I}}^{\prime}}(d):=h(f^{{\mathcal{I}}}(d))$ iff this value is
defined for $f\in\mathsf{N_{F}}$ and $d\in\Delta^{{\mathcal{I}}}$. Since $h$
is an isomorphism, we have $C^{\mathcal{I}}=C^{{\mathcal{I}}^{\prime}}$ for
all concepts $C$, including CD restrictions, which shows that
${\mathcal{I}}^{\prime}$ is a model of $\mathcal{T}$ and all concept and role
assertions in $\mathcal{A}$. Moreover, it also satisfies all feature
assertions $f(a,c)\in{\mathcal{A}}$ since
$f^{{\mathcal{I}}^{\prime}}(a^{{\mathcal{I}}^{\prime}})=h(f^{\mathcal{I}}(a^{\mathcal{I}}))=c$
by construction. ∎

Together with Theorem 10, this also shows that one can use arbitrary singleton
equality predicates in $\mathcal{ALC}(\mathfrak{D})$ ontologies over a
homogeneous concrete domain $\mathfrak{D}$, even if $\mathfrak{D}$ contains
only finitely many singleton predicates (or none).

##  5 Conclusion

In this paper, we revisited the problem of reasoning in
$\mathcal{ALC}(\mathfrak{D})$ with an $\omega$-admissible concrete domain
$\mathfrak{D}$, first addressed in [5]. There, it was conjectured that concept
satisfiability w.r.t. a TBox is ExpTime-complete, provided that
$\operatorname{CSP}(\mathfrak{D})$ is decidable in exponential time. Using an
approach based on type elimination, we successfully proved this conjecture. In
addition, we integrated ABox reasoning and showed that reasoning w.r.t. an
$\mathcal{ALC}(\mathfrak{D})$ ontology where one can refer to specific values
via feature assertions is also ExpTime-complete, if in addition to the above
$\mathfrak{D}$ is an $\omega$-admissible homogeneous structure. The main
examples of $\omega$-admissible concrete domains from the literature fulfill
this requirement as they are (reducts of) finitely bounded homogeneous
structures [9], and so we obtain insights into the complexity of reasoning
with extensions of $\mathcal{ALC}$ by concrete domain restrictions ranging
over Allen’s interval algebra, the region connection calculus RCC8, the
rational numbers with ordering and equality, and disjoint combinations of
those domains.

By extending the type elimination algorithm proposed in this paper
appropriately, we believe that it is possible to show that decidability is
preserved in extensions of $\mathcal{ALC}(\mathfrak{D})$ such as
$\mathcal{ALCI}(\mathfrak{D})$, where inverse roles are allowed in both role
and concrete domain restrictions (so that we can write, e.g.
$\forall\mathsf{hasChild}^{-}\,\mathsf{age},\mathsf{hasChild}\,\mathsf{age}.{>}$),
and $\mathcal{ALC\\!Q}(\mathfrak{D})$, which supports qualified number
restrictions. We also plan to use this type elimination approach as a starting
point in our investigations of different inference problems, for instance
signature-based abduction [13] for $\mathcal{ALC}(\mathfrak{D})$ ontologies
and abstract definability for $\mathcal{ALC}(\mathfrak{D})$ TBoxes, i.e.
checking whether their _abstract expressive power_ [14] can be defined in
$\mathcal{ALC}$.

###### Acknowledgements.

This work was partially supported by DFG grant 389792660 as part of TRR 248 –
CPEC, by the German Federal Ministry of Education and Research (BMBF,
SCADS22B) and the Saxon State Ministry for Science, Culture and Tourism (SMWK)
by funding the competence center for Big Data and AI "ScaDS.AI
Dresden/Leipzig". The authors would like to thank Jakub Rydval for his help in
understanding the properties of finitely bounded homogeneous structures.

## References

  * Baader and Hanschke [1991] F. Baader, P. Hanschke,  A Scheme for Integrating Concrete Domains into Concept Languages,  in: J. Mylopoulos, R. Reiter (Eds.), Proceedings of the 12th International Joint Conference on Artificial Intelligence. Sydney, Australia, August 24-30, 1991, Morgan Kaufmann, 1991, pp. 452–457. URL: http://ijcai.org/Proceedings/91-1/Papers/070.pdf.
  * Lutz [2002a] C. Lutz, The complexity of description logics with concrete domains, Ph.D. thesis, RWTH Aachen University, Germany, 2002a. URL: http://nbn-resolving.org/urn:nbn:de:hbz:82-opus-3032.
  * Lutz [2002b] C. Lutz,  Description logics with concrete domains - A survey,  in: P. Balbiani, N. Suzuki, F. Wolter, M. Zakharyaschev (Eds.), Advances in Modal Logic 4, King’s College Publications, 2002b, pp. 265–296. URL: http://www.aiml.net/volumes/volume4/Lutz.ps.
  * Baader et al. [2005] F. Baader, S. Brandt, C. Lutz,  Pushing the EL envelope,  in: L. P. Kaelbling, A. Saffiotti (Eds.), IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Professional Book Center, 2005, pp. 364–369. URL: http://ijcai.org/Proceedings/05/Papers/0372.pdf.
  * Lutz and Miličić [2007] C. Lutz, M. Miličić,  A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes,  Journal of Automated Reasoning 38 (2007) 227–259. doi:10.1007/s10817-006-9049-7.
  * Artale et al. [2012] A. Artale, V. Ryzhikov, R. Kontchakov,  DL-Lite with attributes and datatypes,  in: L. D. Raedt, C. Bessiere, D. Dubois, P. Doherty, P. Frasconi, F. Heintz, P. J. F. Lucas (Eds.), ECAI 2012 - 20th European Conference on Artificial Intelligence, volume 242 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2012, pp. 61–66. doi:10.3233/978-1-61499-098-7-61.
  * Carapelle and Turhan [2016] C. Carapelle, A.-Y. Turhan,  Description Logics Reasoning w.r.t. General TBoxes Is Decidable for Concrete Domains with the EHD-Property,  in: ECAI 2016, IOS Press, 2016, pp. 1440–1448. doi:10.3233/978-1-61499-672-9-1440.
  * Labai et al. [2020] N. Labai, M. Ortiz, M. Šimkus,  An ExpTime Upper Bound for ALC with Integers,  Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning 17 (2020) 614–623. doi:10.24963/kr.2020/61.
  * Baader and Rydval [2022] F. Baader, J. Rydval,  Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains,  Journal of Automated Reasoning 66 (2022) 357–407. doi:10.1007/s10817-022-09626-2.
  * Demri and Quaas [2023] S. Demri, K. Quaas,  First Steps Towards Taming Description Logics with Strings,  in: S. Gaggl, M. V. Martinez, M. Ortiz (Eds.), Logics in Artificial Intelligence, Lecture Notes in Computer Science, Springer Nature Switzerland, Cham, 2023, pp. 322–337. doi:10.1007/978-3-031-43619-2_23.
  * Baader and Rydval [2020] F. Baader, J. Rydval,  Description Logics with Concrete Domains and General Concept Inclusions Revisited,  in: N. Peltier, V. Sofronie-Stokkermans (Eds.), Automated Reasoning, Lecture Notes in Computer Science, Springer International Publishing, Cham, 2020, pp. 413–431. doi:10.1007/978-3-030-51074-9_24.
  * Baader et al. [2017] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge University Press, 2017. doi:10.1017/9781139025355.
  * Koopmann [2021] P. Koopmann,  Signature-based abduction with fresh individuals and complex concepts for description logics,  in: Z. Zhou (Ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI, ijcai.org, 2021, pp. 1929–1935. doi:10.24963/IJCAI.2021/266.
  * Baader and De Bortoli [2024] F. Baader, F. De Bortoli,  The Abstract Expressive Power of First-Order and Description Logics with Concrete Domains,  in: Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC ’24, ACM, New York, NY, USA, 2024, pp. 754–761. doi:10.1145/3605098.3635984.

##  Appendix A Omitted Proofs for Section 3

See 1

###### Proof.

We prove the claim by induction over $m\in\mathbb{N}$. For the base case
$m=0$, observe that $\mathfrak{C}^{0}$ is equal to
$\mathfrak{C}_{\mathcal{A}}^{0}$ since $\mathfrak{C}_{\mathcal{A}}^{0}$
already contains all local systems of the form $\mathfrak{C}_{a,w_{a}}$ (see
Definition 5). Since $\mathfrak{C}_{\mathcal{A}}^{0}$ is equal to
$\mathfrak{C}_{\mathcal{A}}$ up to renaming of variables, the fact that
$\mathfrak{C}_{\mathcal{A}}$ has a solution implies that
$\mathfrak{C}^{0}=\mathfrak{C}_{\mathcal{A}}^{0}$ has a solution as well.

For the inductive step, we assume that $\mathfrak{C}^{m}$ has a solution and
show how to extend it to a solution of $\mathfrak{C}^{m+1}$. We begin by
observing that any constraint system $\mathfrak{C}$ that has a solution $h$
can be extended to a complete constraint system by using $h$ to add any
missing constraints; i.e. if there is no constraint $P(v_{1},\dots,v_{k})$ for
$v_{1},\dots,v_{k}\in V(\mathfrak{C})$, but $\mathfrak{D}$ has $k$-ary
predicates, then we can complete $\mathfrak{C}$ by adding the unique
$P(v_{1},\dots,v_{k})$ for which $(h(v_{1}),\dots,h(v_{k}))\in P^{D}$ (cf.
JEPD). Moreover, this complete constraint system also has $h$ as a solution.
Since $\mathfrak{C}^{m}$ has a solution, let now $\mathfrak{B}$ be the
satisfiable, complete system obtained by extending $\mathfrak{C}^{m}$ in this
way.

Let $(a,w)\in\Delta^{m+1}\setminus\Delta^{m}$. By construction, there is a
unique non-empty word $w^{\prime}\in\Delta^{m}$ and a symbol
$(\mathfrak{t},i)\in\Sigma$ such that $w=w^{\prime}\cdot(\mathfrak{t},i)$. We
notice that $\mathfrak{B}$ and $\mathfrak{C}_{a,w}$ are complete systems that
agree on the constraints over their shared variables $V(\mathfrak{B})\cap
V(\mathfrak{C}_{a,w})$. This holds since all constraints over the shared
variables (which are all of the form $f^{a,w}$) must occur in $\mathfrak{B}$
inside $\mathfrak{C}_{a,w^{\prime}}$; for the case of $w^{\prime}=w_{a}$, this
is because all constraints from $\mathfrak{C}_{a,w_{a}}$ must occur in
$\mathfrak{C}_{\mathcal{A}}^{0}$ by Definition 5, and $\mathfrak{C}_{a,w_{a}}$
is complete. Both $\operatorname{\mathsf{end}}(w^{\prime})$ and $\mathfrak{t}$
belong to $\mathbb{T}$, and $\mathfrak{t}$ patches
$\operatorname{\mathsf{end}}(w^{\prime})$ at $i$, thus
$\mathfrak{C}_{a,w^{\prime}}\cup\mathfrak{C}_{a,w}$ has a solution (cf.
Definition 4). In particular, the relations over the concrete domain
$\mathfrak{D}$ satisfy JEPD, hence there cannot be a tuple of variables
$v_{1},\dotsc,v_{k}$ such that $P(v_{1},\dotsc,v_{k})\in\mathfrak{C}_{a,w}$
and
$P^{\prime}(v_{1},\dotsc,v_{k})\in\mathfrak{C}_{a,w^{\prime}}\subseteq\mathfrak{B}$
with $P\neq P^{\prime}$. Since $\mathfrak{B}$ and $\mathfrak{C}_{a,w}$ are
complete, agree on the constraints over their shared variables, and both have
a solution ($\mathfrak{B}$ by inductive hypothesis, and $\mathfrak{C}_{a,w}$
because $\mathfrak{t}\in\mathbb{T}$), property AP implies that
$\mathfrak{B}\cup\mathfrak{C}_{a,w}$ has a solution, which we can use to
extend $\mathfrak{B}$ to a complete constraint that includes
$\mathfrak{C}_{a,w}$.

We can repeat this process for every
$(a,w)\in\Delta^{m+1}\setminus\Delta^{m}$, because the different constraint
systems $\mathfrak{C}_{a,w}$ do not share variables, and thus we obtain a
constraint system $\mathfrak{B}^{\prime}$ that is complete, has a solution,
and includes $\mathfrak{C}^{m+1}$. Therefore, we conclude that
$\mathfrak{C}^{m+1}$ has a solution. ∎

See 2

###### Proof.

We prove this claim by structural induction over $C\in{\mathcal{M}}$. We first
prove the two base cases where $C$ is either a concept name or an existential
CD-restriction.

  * •

The case $C=A$ is trivially covered by the definition of $A^{{\mathcal{I}}}$.

  * •

Let $C=\exists p_{1},\dotsc,p_{k}.P\in{\mathcal{M}}$. If
$C\in\operatorname{\mathsf{root}}(\mathfrak{t})$, by definition of local
system and because of $\mathfrak{t}\in\mathbb{T}$ we are able to find a
constraint
$P(f_{1}^{j_{1}},\dotsc,f_{k}^{j_{k}})\in\mathfrak{C}_{\mathfrak{t}}$ such
that for each $i=1,\dotsc,k$

    * –

if $p_{i}=f_{i}$, then $j_{i}=0$;

    * –

if $p_{i}=r_{i}f_{i}$, then
$j_{i}\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r_{i})$ and there exists
$\mathfrak{u}^{i}\in\mathbb{T}$ that patches $\mathfrak{t}$ at $j_{i}$.

Using these indices and augmented types, we define the words

$w^{i}:=\begin{cases}w&\text{if $p_{i}=f_{i}$},\\\
w\cdot(\mathfrak{u}^{i},j_{i})&\text{if $p_{i}=r_{i}f_{i}$}.\end{cases}$

for $i=1,\dotsc,k$. It follows that
$P(f_{1}^{a,w^{1}},\dotsc,f_{k}^{a,w^{k}})\in\mathfrak{C}^{{\mathcal{I}}}$,
which implies that
$\big{(}f_{1}^{{\mathcal{I}}}(a,w^{1}),\dotsc,f_{k}^{{\mathcal{I}}}(a,w^{k})\big{)}\in
P^{D}$ by definition of $\mathcal{I}$. Due to the construction of $w^{i}$, we
know that $f_{i}^{{\mathcal{I}}}(a,w^{i})\in p_{i}^{{\mathcal{I}}}(a,w)$ holds
for $i=1,\dotsc,k$, which allows us to conclude that $(a,w)\in
C^{{\mathcal{I}}}$.

Vice versa, assume that $C\notin\operatorname{\mathsf{root}}(\mathfrak{t})$.
By Definition 2, this means that $\lnot
C\in\operatorname{\mathsf{root}}(\mathfrak{t})$. For every tuple of values
$c_{i}\in p_{i}^{{\mathcal{I}}}(w)$, $i=1,\dotsc,k$, we have to show that
$(c_{1},\dots,c_{k})\notin P^{D}$.

We first consider the case that $w=w_{a}$ for some
$a\in\mathsf{N_{I}}({\mathcal{A}})$, and find individual names $a^{i}$ and
words $w^{i}$ such that the variable $f^{a^{i},w^{i}}$ reflects the origin of
the value $c_{i}$, as follows. By construction of $\mathcal{I}$, one of the
following three cases must hold for each $i\in\\{1,\dots,k\\}$.

    * –

If $p_{i}=f_{i}$ and
$c_{i}=f_{i}^{\mathcal{I}}(a,w_{a})=h^{\mathcal{I}}(f_{i}^{a,w_{a}})$, then we
set $a^{i}:=a$ and $w^{i}:=w_{a}$.

    * –

If $p_{i}=r_{i}f_{i}$ and
$c_{i}=f_{i}^{\mathcal{I}}(b,w_{b})=h^{\mathcal{I}}(f_{i}^{b,w_{b}})$ for some
individual name $b$ with $r_{i}(a,b)\in{\mathcal{A}}_{R}$, then we set
$a^{i}:=b$ and $w^{i}:=w_{b}$.

    * –

If $p_{i}=r_{i}f_{i}$ and
$c_{i}=f_{i}^{\mathcal{I}}(a,w^{\prime})=h^{\mathcal{I}}(f_{i}^{a,w^{\prime}})$
for some $r_{i}$-successor $(a,w^{\prime})$ of $(a,w)$ with
$w^{\prime}=w\cdot(\mathfrak{t}^{\prime},j)$ and
$j\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r_{i})$, then we set
$a^{i}:=a$ and $w^{i}:=w^{\prime}$.

By Definition 5 and the fact that $\lnot
C\in\operatorname{\mathsf{root}}(\mathfrak{t})$, we know that
$P\big{(}f_{1}^{a^{1},w^{1}},\dots,f_{k}^{a^{k},w^{k}}\big{)}$ cannot be
contained in $\mathfrak{C}_{\mathcal{A}}^{0}$. However, by construction of
$\mathcal{I}$, the fact that the corresponding feature values are defined
means that the variables $f_{1}^{a^{1},w^{1}},\dots,f_{k}^{a^{k},w^{k}}$ must
all occur in $\mathfrak{C}_{\mathcal{A}}^{0}$. Hence, by completeness of
$\mathfrak{C}_{\mathcal{A}}^{0}$, then,
$P^{\prime}\big{(}f_{1}^{a^{1},w^{1}},\dots,f_{k}^{a^{k},w^{k}}\big{)}\in\mathfrak{C}_{\mathcal{A}}^{0}\subseteq\mathfrak{C}^{\mathcal{I}}$
for some $k$-ary predicate $P^{\prime}$ disjoint with $P$. This means that
$(c_{1},\dotsc,c_{k})=\big{(}h^{\mathcal{I}}(f_{1}^{a^{1},w^{1}}),\dots,h^{\mathcal{I}}(f_{k}^{a^{k},w^{k}})\big{)}\in(P^{\prime})^{D}$,
and thus $(c_{1},\dotsc,c_{k})\notin P^{D}$. This allows us to conclude that
$(a,w_{a})\notin C^{{\mathcal{I}}}$.

For the case that $w\neq w_{a}$ for all $a\in\mathsf{N_{I}}({\mathcal{A}})$,
we can use similar, but simpler, arguments, based on $\mathfrak{C}_{w}$
(Definition 3) instead of $\mathfrak{C}_{\mathcal{A}}^{0}$ (Definition 5).

Let us now assume that the claim holds for $D,C_{1},C_{2}\in{\mathcal{M}}$ and
prove the inductive cases.

  * •

If $C=\neg D\in{\mathcal{M}}$, then
$C\in\operatorname{\mathsf{root}}(\mathfrak{t})$ iff
$D\notin\operatorname{\mathsf{root}}(\mathfrak{t})$ iff $(a,w)\notin
D^{{\mathcal{I}}}$ iff $(a,w)\in C^{{\mathcal{I}}}$, where the equivalences
hold due to Definition 2, the inductive hypothesis, and the semantics of
negation, respectively.

  * •

If $C=C_{1}\sqcap C_{2}\in{\mathcal{M}}$, then
$C\in\operatorname{\mathsf{root}}(\mathfrak{t})$ iff
$C_{1}\in\operatorname{\mathsf{root}}(\mathfrak{t})$ and
$C_{2}\in\operatorname{\mathsf{root}}(\mathfrak{t})$ iff $(a,w)\in
C_{1}^{{\mathcal{I}}}$ and $(a,w)\in C_{2}^{{\mathcal{I}}}$ iff $(a,w)\in
C^{{\mathcal{I}}}$, where the equivalences hold similarly to the case of
concept negation.

  * •

If $C=\exists r.D\in{\mathcal{M}}$, then
$C\in\operatorname{\mathsf{root}}(\mathfrak{t})$ and
$\mathfrak{t}\in\mathbb{T}$ imply that there are
$i\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r)$ and an augmented type
$\mathfrak{t}^{\prime}\in\mathbb{T}$ that patches $\mathfrak{t}$ at $i$ such
that $((a,w),(a,w^{\prime}))\in r^{{\mathcal{I}}}$ with
$w^{\prime}=w\cdot(\mathfrak{t}^{\prime},i)$ and
$D\in\operatorname{\mathsf{root}}(\mathfrak{t}^{\prime})$. By definition of
$\mathcal{I}$ and inductive hypothesis, we deduce that $(a,w^{\prime})\in
D^{{\mathcal{I}}}$, which in turn implies $(a,w)\in C^{{\mathcal{I}}}$.

Vice versa, assume that $C\notin\operatorname{\mathsf{root}}(\mathfrak{t})$,
and thus $\neg C\in\operatorname{\mathsf{root}}(\mathfrak{t})$. Any
$r$-successor $e$ of $(a,w)$ must be of one of the following forms.

    * –

If $w=w_{a}=(\mathfrak{t}_{a},0)$, $e=(b,w_{b})$, and
$r(a,b)\in{\mathcal{A}}_{R}$, then $\lnot
C\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$ implies that
$D\notin\operatorname{\mathsf{root}}(\mathfrak{t}_{b})$ by Definition 5. Since
$\operatorname{\mathsf{end}}(w_{b})=\mathfrak{t}_{b}$, we thus obtain $e\notin
D^{\mathcal{I}}$ by inductive hypothesis.

    * –

If $e=(a,w^{\prime})$ and
$\operatorname{\mathsf{end}}(w^{\prime})=\mathfrak{t}^{\prime}$ patches some
$i\in\operatorname{\mathsf{succ}}_{\mathfrak{t}}(r)$, then $\neg
C\in\operatorname{\mathsf{root}}(\mathfrak{t})$ implies that
$D\notin\operatorname{\mathsf{root}}(\mathfrak{t}^{\prime})$ (see Definition
4). By inductive hypothesis, we conclude that $e\notin D^{\mathcal{I}}$.

This shows that no $r$-successor of $(a,w)$ can satisfy $D$ in $\mathcal{I}$,
and thus $(a,w)\notin C^{\mathcal{I}}$. ∎

See 3

###### Proof.

We notice that $\mathfrak{C}_{d}$ is complete and that $\mathfrak{C}_{d}$ and
$\operatorname{\mathsf{succ}}_{d}$ satisfy all the conditions stated in
Definition 3 and thus constitute a local system. In addition, the mapping
$v_{d}(f^{i}):=f^{{\mathcal{I}}}(d_{i})$ is a solution of $\mathfrak{C}_{d}$,
and thanks to our choice of types $t_{0},\dotsc,t_{n_{\mathcal{O}}}$ we also
obtain that the augmented type $\mathfrak{t}_{{\mathcal{I}}}(d)$ constructed
using this process is locally realizable.

Moreover, for a given augmented type
$\mathfrak{t}=\mathfrak{t}_{{\mathcal{I}}}(d)$ in $\mathbb{T}_{{\mathcal{I}}}$
and $i\in\\{0,\dotsc,n_{\mathcal{O}}\\}$, our construction yields that
$\mathfrak{t}^{\prime}=\mathfrak{t}_{{\mathcal{I}}}(d_{i})$ patches
$\mathfrak{t}$ at $i$; here, $d_{i}$ is the domain element chosen for $t_{i}$
in the construction of $\mathfrak{t}_{{\mathcal{I}}}(d)$. The first condition,
namely that $\operatorname{\mathsf{root}}(\mathfrak{t}^{\prime})=t_{i}$, is
fulfilled by construction. The second condition, i.e. that
$\mathfrak{C}_{\mathfrak{t}}\mathop{{\vartriangleleft}_{i}}\mathfrak{C}_{\mathfrak{t}^{\prime}}$
has a solution, follows from the fact that the individual solutions $v_{d}$,
$v_{d_{i}}$ constructed above agree on the values of the shared variables
$v_{d}(f^{i})=f^{{\mathcal{I}}}(d_{i})=v_{d_{i}}({f^{0}})$. Together with the
conditions proved during the construction of the augmented types, this ensures
that $\mathfrak{t}$ is patched by $\mathbb{T}_{{\mathcal{I}}}$. ∎

See 4

###### Proof.

We show that $\mathfrak{t}^{\mathcal{I}}_{\mathcal{A}}$ satisfies all
conditions stated in Definition 5. If $C(a)\in{\mathcal{A}}$ then
$a^{{\mathcal{I}}}\in C^{{\mathcal{I}}}$ and since
$\operatorname{\mathsf{root}}(\mathfrak{t}_{a})=t_{{\mathcal{I}}}(a^{{\mathcal{I}}})$,
we deduce that $C\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$.
Similarly, if $r(a,b)\in{\mathcal{A}}$ then
$(a^{{\mathcal{I}}},b^{{\mathcal{I}}})\in r^{{\mathcal{I}}}$ holds, which by
definition of ${\mathcal{A}}_{R}$ implies that $r(a,b)\in{\mathcal{A}}_{R}$.
If $\neg\exists r.C\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$ and
$r(a,b)\in{\mathcal{A}}_{R}$, the fact that $b$ is an $r$-successor of $a$ in
$\mathcal{I}$ clearly implies that
$C\notin\operatorname{\mathsf{root}}(\mathfrak{t}_{b})=t_{{\mathcal{I}}}(b^{{\mathcal{I}}})$
must hold. We turn our attention to $\mathfrak{C}_{{\mathcal{A}}}$. If
$P(f_{1}^{j_{1}},\dotsc,f_{k}^{j_{k}})\in\mathfrak{C}_{\mathfrak{t}_{a}}$,
then
$(f_{1}^{{\mathcal{I}}}(d_{a,j_{1}}),\dotsc,f_{k}^{{\mathcal{I}}}(d_{a,j_{k}}))\in
P^{D}$, and by definition of $\mathfrak{C}_{{\mathcal{A}}}$ we obtain
$P(f_{1}^{a_{1},i_{1}},\dotsc,f_{k}^{a_{k},i_{k}})\in\mathfrak{C}_{\mathcal{A}}$.
Next, assume that $a\in\mathsf{N_{I}}({\mathcal{A}})$ and that
$P(v_{1},\dotsc,v_{k})\in\mathfrak{C}_{{\mathcal{A}}}$ holds, where each
variable $v_{i}$ is of one of the forms described in Definition 5 for $a$.
Then, by definition of $\mathfrak{C}_{{\mathcal{A}}}$ we can find values
$c_{i}\in p_{i}^{{\mathcal{I}}}(a^{{\mathcal{I}}})$ for $i=1,\dotsc,k$ such
that $(c_{1},\dotsc,c_{k})\in P^{D}$. Therefore, it follows that $\exists
p_{1},\dotsc,p_{k}.P\in\operatorname{\mathsf{root}}(\mathfrak{t}_{a})$. At
last, we observe that $\mathfrak{C}_{\mathcal{A}}$ has a solution, given by
the interpretation of feature names over $\mathcal{I}$. We conclude that
$\mathfrak{t}^{\mathcal{I}}_{\mathcal{A}}$ is an ABox type for $\mathcal{O}$.
∎

See 8

###### Proof.

It only remains to show that Algorithm 1 runs in exponential time. Each
augmented type $\mathfrak{t}$ contains $n_{\mathcal{O}}+1$ types, each of size
polynomial in the input ontology. Moreover, fixing the types in
$\mathfrak{t}$, there are at most $n_{\mathfrak{D}}\cdot\lvert
V_{\ell}\rvert^{{\rm NewARev.}}$ distinct local systems, where
$n_{\mathfrak{D}}$ is the number of predicates in $\mathfrak{D}$ and
$V_{\ell}=n_{\mathcal{O}}\cdot\lvert\mathsf{N_{F}}\rvert$ the maximal number
of variables. It follows that the number of augmented types is at most
exponential, and thus the loop in 5 takes at most exponentially many
iterations. In each iteration, we need to test whether some
$\mathfrak{t}\in\mathbb{T}$ is not locally realizable or not patched, which
amounts to a number of tests polynomial in $\lvert\mathbb{T}\lvert$, and thus
exponential in the size of ${\mathcal{O}}$. Each such test involves checking
the satisfiability of complete constraint systems
$\mathfrak{C}_{\mathfrak{t}}$ and merged systems
$\mathfrak{C}_{\mathfrak{t}}\mathop{{\vartriangleleft}_{i}}\mathfrak{C}_{\mathfrak{t}^{\prime}}$.
Since $\mathfrak{D}$ is fixed, each (merged) system is of polynomial size.
Since CSP($\mathfrak{D}$) is in ExpTime, each satisfiability test therefore
takes at most exponential time. It follows that the loop in Line 5 takes at
most exponential time in total. It remains to show that also the search for
ABox types in Line 7 takes at most exponential time. For this, it suffices to
observe that there can be at most exponentially many ABox types for
${\mathcal{O}}$, which each have a polynomial-size constraint system attached.
This is not hard to see from Definition 5, since there is one augmented type
for every individual in ${\mathcal{A}}$, the set of possible role assertions
in ${\mathcal{A}}_{R}$ is polynomial in ${\mathcal{O}}$, and the set of
variables in $\mathfrak{C}_{\mathcal{A}}$ is polynomial in the size of the
involved augmented types. ∎

##  Appendix B Omitted Proofs for Section 4

See 10

###### Proof.

Let ${\mathcal{O}}$ be an $\mathcal{ALC}(\mathfrak{D})$ ontology. We show how
to replace all occurrences of an additional singleton predicate $=_{c}$ using
feature assertions. We first replace every CD-restriction $\exists rf.{=_{c}}$
by the equivalent concept $\exists r.\exists f.{=_{c}}$, which means that
$=_{c}$ can occur only in CD-restrictions of the form $\exists f.{=_{c}}$ with
feature paths of length $1$. The idea is now to store the value $c$ in a
special feature $f_{c}$ by using feature assertions in the ABox, and make sure
that the value of $f_{c}$ is equal to $c$ at every element reachable from an
ABox individual by a role chain. We can then express the concept $\exists
f.{=_{c}}$ by making $f$ equal to $f_{c}$, for which we exploit JD.

First, we ensure that $f_{c}$ is a function by the axiom
$\top\sqsubseteq\exists f_{c}.\top_{\mathfrak{D}}$, where
$\top_{\mathfrak{D}}$ is expressed as in the proof of Theorem 9. We next give
$f_{c}$ the value $c$ for all elements reachable from the ABox. If
${\mathcal{O}}$ does not contain an ABox, we introduce a fresh individual name
$a$. For every individual name $a$ occurring in the ABox, or for that fresh
individual name, we add the feature assertion $f_{c}(a,c)$. By JD, equality
between two variables $x$, $y$ can be expressed using a quantifier-free
formula $\phi(x,y)$ over the signature of $\mathfrak{D}$ (i.e. not including
the additional singleton predicates). By JEPD and finiteness of the signature,
we can express negated atoms as disjunctions of positive atoms, so that we may
assume $\phi(x,y)$ to be in DNF. Now consider the formula $\phi(c,y)$, where
$x$ is replaced by the constant $c$. Since $\phi(c,y)$ is equivalent to $c=y$,
we can find a single disjunct $\alpha(c,y)$ of $\phi(c,y)$ such that
$\alpha(c,y)$ is satisfiable and equivalent to $c=y$; otherwise, $\phi(c,y)$
would be satisfied also for values of $y$ other than $c$. For every
$r\in\mathsf{N_{R}}({\mathcal{O}})$, we now obtain the concept $C_{c,r}$ from
$\alpha(c,y)$ by replacing $\wedge$ with $\sqcap$ and every atom
$P(t_{1},\ldots,t_{n})$ with $\forall p_{1},\ldots,p_{n}.P$, where
$p_{i}=f_{c}$ if $t_{i}=c$, and $p_{i}=rf_{c}$ if $t_{i}=y$, and add the axiom
$\top\sqsubseteq C_{c,r}$ to the TBox. This ensures that, in every model
${\mathcal{I}}$ of the resulting ontology, for all elements $d$ that are
reachable from the ABox, we have that $f_{c}^{\mathcal{I}}(d)=c$. We do not
need to consider other elements, since one can show similarly to the proofs of
Lemmas 6 and 7 that, if ${\mathcal{O}}$ is consistent, then it has a forest-
shaped model in which every element is reachable from some element in the
ABox.

We can now replace every concept of the form $\exists f.{=_{c}}$ with a
concept $C_{c,f}$ that is obtained from $\alpha(c,y)$ by replacing $\land$
with $\sqcap$ and atoms $P(t_{1},\ldots,t_{n})$ with $\exists
f_{1},\ldots,f_{n}.P$, where $f_{i}=f_{c}$ if $t_{i}=c$, and $f_{i}=f$ if
$t_{i}=y$. Doing this transformation for all singleton predicates $=_{c}$ in
${\mathcal{O}}$ leads to the required equi-consistent ontology
${\mathcal{O}}^{\prime}$ without singleton predicates. ∎