# Querying Circumscribed Description Logic Knowledge Bases

Carsten Lutz1 Quentin Manière1,2 Robin Nolte3
1Department of Computer Science, Leipzig University, Germany
2Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI),
Dresden/Leipzig, Germany
3University of Bremen, Digital Media Lab, Germany
{carsten.lutz<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Circumscription is one of the main approaches for defining non-monotonic
description logics (DLs) and the decidability and complexity of traditional
reasoning tasks, such as satisfiability of circumscribed DL knowledge bases
(KBs), are well understood. For evaluating conjunctive queries (CQs) and
unions thereof (UCQs), in contrast, not even decidability has been
established. In this paper, we prove decidability of (U)CQ evaluation on
circumscribed DL KBs and obtain a rather complete picture of both the combined
complexity and the data complexity for DLs ranging from $\mathcal{ALCHIO}$ via
${\cal EL}$ to various versions of DL-Lite. We also study the much simpler
atomic queries (AQs).

##  1 Introduction

While standard description logics (DLs), such as those underlying the OWL 2
ontology language, do not support non-monotonic reasoning, it is generally
acknowledged that extending DLs with non-monotonic features is very useful.
Concrete examples of applications include ontological modeling in the
biomedical domain (?; ?) and the formulation of access control policies (?).
Circumscription is one of the traditional AI approaches to non-monotonicity,
and it provides an important way to define non-monotonic DLs. In contrast to
other approaches, such as default rules, it does not require the adoption of
strong syntactic restrictions to preserve decidability. DLs with
circumscription are closely related to several other approaches to non-
monotonic DLs, in particular to DLs with defeasible inclusions and typicality
operators (?; ?; ?; ?; ?).

The main feature of circumscription is that selected predicate symbols can be
minimized, that is, the extension of these predicates must be minimal
regarding set inclusion. Other predicates may vary freely or be declared
fixed. In addition, a preference order can be declared on the minimized
predicates. In DLs, minimizing or fixing role names causes undecidability of
reasoning, and consequently, only concept names may be minimized or fixed (?).
The traditional AI use of circumscription is to introduce and minimize
abnormality predicates such as ${\sf AbnormalBird}$, which makes it possible
to formulate defeasible implications such as ‘birds fly, unless they are
abnormal, which shouldn’t be assumed unless there is a reason to do so.’
Circumscription is also closely related to the closure of predicates symbols
as studied, for instance, in (?; ?; ?); in fact, this observation goes back to
(?; ?). While DLs usually assume open-world semantics and represent incomplete
knowledge, such closed predicates are interpreted under a closed-world
assumption, reflecting that complete knowledge is available regarding those
predicates. Circumscription may then be viewed as a soft form of closing
concept names: there are no other instances of a minimized concept name except
the explicitly asserted ones unless we are forced to introduce (a minimal set
of) additional instances to avoid inconsistency.

A primary application of DLs is ontology-mediated querying, where an ontology
is used to enrich data with domain knowledge. Surprisingly, little is known
about ontology-mediated querying with DLs that support circumscription. For
the important conjunctive queries (CQs) and unions of CQs (UCQs), in fact, not
even decidability has been established. This paper aims to close this gap by
studying the decidability and precise complexity of ontology-mediated querying
for DLs with circumscription, both w.r.t. combined complexity and data
complexity. We consider the expressive DL $\mathcal{ALCHIO}$, the tractable
(without circumscription) DL ${\cal EL}$, and several members of tge DL-Lite
family. These may be viewed as logical cores of the profiles OWL 2 DL, OWL 2
EL, and OWL 2 QL of the OWL 2 ontology language (?).

One of our main results is that UCQ evaluation is decidable in all these DLs
when circumscription is added. It is 2Exp-complete in $\mathcal{ALCHIO}$
w.r.t. combined complexity, and thus not harder than query evaluation without
circumscription. W.r.t. data complexity, however, there is a significant
increase from coNP\- to $\Uppi^{\textrm{P}}_{2}$-completeness. For ${\cal
EL}$, the combined and data complexity turns out to be identical to that of
$\mathcal{ALCHIO}$. This improves lower bounds from (?). All these lower
bounds already hold for CQs. Remarkably, the $\Uppi^{\textrm{P}}_{2}$ lower
bound for data complexity already holds when there is only a single minimized
concept name (and thus no preference relation) and without fixed predicates.
The complexities for DL-Lite are lower, though still high. A summary can be
found in Table 1. Evaluation is ‘only’ coNP-complete w.r.t. data complexity
for all considered versions of DL-Lite, except when role disjointness
constraints are added (this case is not in the table). The combined complexity
remains at 2Exp when role inclusions are present and drops to coNExp without
them. The lower bounds already apply to very basic versions of DL-Lite that
are positive in the sense that they do not provide concept disjointness
constraints, and the upper bounds apply to expressive versions that include
all Boolean operators.

We also study the evaluation of the basic yet important atomic queries (AQs),
conjunctive queries of the form $A(x)$ with $A$ a concept name. Also here, we
obtain a rather complete picture of the complexity landscape. It is known from
(?) that AQ evaluation in $\mathcal{ALCHIO}$ is $\textnormal{\sc
coNExp}^{\textnormal{\sc NP}}$-complete w.r.t. combined complexity. We show
that the lower bound holds already for ${\cal EL}$. Moreover, our
$\Uppi^{\textrm{P}}_{2}$-lower bound for the data complexity of (U)CQ-
evaluation in ${\cal EL}$ mentioned above only requires an AQ, and thus AQ
evaluation in both $\mathcal{ALCHIO}$ and ${\cal EL}$ are
$\Uppi^{\textrm{P}}_{2}$-complete w.r.t. data complexity. For DL-Lite, the
data complexity drops to PTime in all considered versions, and the combined
complexity ranges from coNExp-complete to $\Uppi^{\textrm{P}}_{2}$-complete,
depending on which Boolean operators are admitted. A summary can be found in
Table 2.

Proof details are in the appendix.

|  ${\cal EL}$, $\mathcal{ALCHIO}$ |  $\textrm{DL-Lite}_{\sf core}^{\cal H}$, $\textrm{DL-Lite}_{\sf bool}^{\cal H}$ | $\textrm{DL-Lite}_{\sf bool}$ |  $\textrm{DL-Lite}_{\sf core}$, $\textrm{DL-Lite}_{\sf horn}$
---|---|---|---|---
Combined complexity |  2Exp -c.(Thm. 1, 2) |  2Exp -c.(†) (Thm. 1, 5) |  coNExp -c.(Thm. 6, 13) |  coNExp -c.(†) (Thm. 6, 7)
Data complexity |  $\Uppi^{\textrm{P}}_{2}$-c.(Thm. 3, 4) |  coNP -c.(Thm. 8, 9) |  coNP -c.(Thm. 8, 9) |  coNP -c.(Thm. 8, 9)
Table 1: Complexity of (U)CQ evaluation on circumscribed KBs.
$\cdot^{(\dagger)}$ indicates that UCQs are needed for lower bound.

Related Work. A foundational paper on description logics with circumscription
is (?), which studies concept satisfiability and knowledge base consistency in
the $\mathcal{ALCHIO}$ family of DLs; these problems are interreducible with
AQ evaluation in polynomial time (up to complementation). The same problems
have been considered in (?) for ${\cal EL}$ and DL-Lite and in (?) for DLs
without the finite model property, including a version of DL-Lite. The recent
(?) is the only work we are aware of that considers ontology-mediated querying
in the context of circumscription. It provides lower bounds for ${\cal EL}$
and DL-Lite, which are both improved in the current paper, but no decidability
results / upper bounds. A relaxed version of circumscription that enjoys lower
complexity has recently been studied in (?). We have already mentioned
connections to DLs with defeasible inclusions and typicality operators, see
above for references. A connection between circumscription and the complexity
class $\Uppi^{\textrm{P}}_{2}$ was first observed in (?), and this complexity
shows up in our data complexity results. Our proofs, however, are quite
different.

##  2 Preliminaries

Let ${\sf N_{C}}$, ${\sf N_{R}}$, and ${\sf N_{I}}$ be countably infinite sets
of _concept names_ , _role names_ , and _individual names_. An _inverse role_
takes the form $r^{-}$ with $r$ a role name, and a _role_ is a role name or an
inverse role. If $r=s^{-}$ is an inverse role, then $r^{-}$ denotes $s$. An
_${\cal ALCIO}$ concept_ $C$ is built according to the rule $C,D::=\top\mid
A\mid\\{a\\}\mid\neg C\mid C\sqcap D\mid\exists r.D$ where $A$ ranges over
concept names, $a$ over individual names, and $r$ over roles. A concept of the
form $\\{a\\}$ is called a _nominal_. We write $\bot$ as abbreviation for
$\neg\top$, $C\sqcup D$ for $\neg(\neg C\sqcap\neg D)$, and $\forall r.C$ for
$\neg\exists r.\neg C$. An _$\mathcal{ALCI}$ concept_ is a nominal-free ${\cal
ALCIO}$ concept. An _${\cal EL}$ concept_ is an $\mathcal{ALCI}$ concept that
uses neither negation nor inverse roles.

An _$\mathcal{ALCHIO}$ TBox_ is a finite set of _concept inclusions (CIs)_
$C\sqsubseteq D$, where $C,D$ are ${\cal ALCIO}$ concepts, and _role
inclusions (RIs)_ $r\sqsubseteq s$, where $r,s$ are roles. In an _${\cal EL}$
TBox_, only ${\cal EL}$ concepts may be used in CIs, and RIs are disallowed.
An _ABox_ is a finite set of _concept assertions_ $A(a)$ and _role assertions_
$r(a,b)$ where $A$ is a concept name, $r$ a role name, and $a,b$ are
individual names. We use ${\sf ind}(\mathcal{A})$ to denote the set of
individual names used in $\mathcal{A}$. An _$\mathcal{ALCHIO}$ knowledge base
(KB)_ takes the form $\mathcal{K}=(\mathcal{T},\mathcal{A})$ with
$\mathcal{T}$ an $\mathcal{ALCHIO}$ TBox and $\mathcal{A}$ an ABox.
$\mathcal{ALCHI}$ TBoxes and KBs are defined analogously but may not use
nominals.

The semantics is defined as usual in terms of interpretations
$\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ with
$\Delta^{\mathcal{I}}$ the (non-empty) _domain_ and $\cdot^{\mathcal{I}}$ the
_interpretation function_ , we refer to (?) for full details. An
interpretation satisfies a CI $C\sqsubseteq D$ if $C^{\mathcal{I}}\subseteq
D^{\mathcal{I}}$ and likewise for RIs. It satisfies an assertion $A(a)$ if
$a\in A^{\mathcal{I}}$ and $r(a,b)$ if $(a,b)\in r^{\mathcal{I}}$; we thus
make the _standard names assumption_. An interpretation $\mathcal{I}$ is a
_model_ of a TBox $\mathcal{T}$, written $\mathcal{I}\models\mathcal{T}$, if
it satisfies all inclusions in it. Models of ABoxes and KBs are defined
likewise. For an interpretation $\mathcal{I}$ and
$\Delta\subseteq\Delta^{\mathcal{I}}$, we use $\mathcal{I}|_{\Delta}$ to
denote the restriction of $\mathcal{I}$ to subdomain $\Delta$.

A _signature_ is a set of concept and role names referred to as _symbols_. For
any syntactic object $O$ such as a TBox or an ABox, we use ${\sf sig}(O)$ to
denote the symbols used in $O$ and $|O|$ to denote the _size_ of $O$, meaning
the encoding of $O$ as a word over a suitable alphabet.

We next introduce several more restricted DLs of the DL-Lite family. A _basic
concept_ is of the form $A$ or $\exists r.\top$. A $\textrm{DL-Lite}_{\sf
core}^{\cal H}$ TBox is a finite set of concept inclusions $C\sqsubseteq D$,
_(concept) disjointness assertions_ $C\sqsubseteq\neg D$, and role inclusions
$r\sqsubseteq s$ where $C,D$ are basic concepts and $r,s$ roles. We drop
superscript $\cdot^{\mathcal{H}}$ if no role inclusions are admitted, use
subscript $\cdot_{{\sf horn}}$ to indicate that the concepts $C,D$ in concept
inclusions may be conjunctions of basic concepts, and subscript $\cdot_{{\sf
bool}}$ to indicate that $C,D$ may be Boolean combinations of basic concepts,
that is, built from basic concepts using $\neg$, $\sqcap$, $\sqcup$.

A _circumscription pattern_ is a tuple ${\sf
CP}=(\prec,\mathsf{M},\mathsf{F},\mathsf{V})$, where $\prec$ is a strict
partial order on $\mathsf{M}$ called the _preference relation_ , and
$\mathsf{M}$, $\mathsf{F}$ and $\mathsf{V}$ are a partition of ${\sf N_{C}}$.
The elements of $\mathsf{M}$, $\mathsf{F}$ and $\mathsf{V}$ are the
_minimized_ , _fixed_ and _varying_ concept names. Role names always vary to
avoid undecidability (?). The preference relation $\prec$ on $\mathsf{M}$
induces a preference relation $<_{\sf CP}$ on interpretations by setting
$\mathcal{J}<_{\sf CP}\mathcal{I}$ if the following conditions hold:

  1. 1.

$\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}}$,

  2. 2.

for all $A\in\mathsf{F}$, $A^{\mathcal{J}}=A^{\mathcal{I}}$,

  3. 3.

for all $A\in\mathsf{M}$ with $A^{\mathcal{J}}\not\subseteq A^{\mathcal{I}}$,
there is a $B\in\mathsf{M}$, $B\prec A$, such that $B^{\mathcal{J}}\subsetneq
B^{\mathcal{I}}$,

  4. 4.

there exists an $A\in\mathsf{M}$ such that $A^{\mathcal{J}}\subsetneq
A^{\mathcal{I}}$ and for all $B\in\mathsf{M}$, $B\prec A$ implies
$B^{\mathcal{J}}=B^{\mathcal{I}}$.

A _circumscribed KB (cKB)_ takes the form ${\sf Circ_{\sf CP}}(\mathcal{K})$
where $\mathcal{K}$ is a KB and ${\sf CP}$ a circumscription pattern. A model
$\mathcal{I}$ of $\mathcal{K}$ is a _model_ of ${\sf Circ_{\sf
CP}}(\mathcal{K})$, denoted $\mathcal{I}\models{\sf Circ_{\sf
CP}}(\mathcal{K})$, if no $\mathcal{J}<_{\sf CP}\mathcal{I}$ is a model of
$\mathcal{K}$. A cKB ${\sf Circ_{\sf CP}}(\mathcal{K})$ is _satisfiable_ if it
has a model.

A _conjunctive query (CQ)_ takes the form
$q(\bar{x})=\exists\bar{y}\,\varphi(\bar{x},\bar{y})$ where $\bar{x}$ and
$\bar{y}$ are tuples of variables and $\varphi$ is a conjunction of _atoms_
$A(z)$ and $r(z,z^{\prime})$, with $A\in{\sf N_{C}}$, $r\in{\sf N_{R}}$, and
$z,z^{\prime}$ variables from $\bar{x}\cup\bar{y}$. The variables in $\bar{x}$
are the _answer variables_ , and ${\sf var}(q)$ denotes $\bar{x}\cup\bar{y}$.
We take the liberty to view $q$ as a set of atoms, writing, e.g., $\alpha\in
q$ to indicate that $\alpha$ is an atom in $q$. We may also write
$r^{-}(x,y)\in q$ in place of $r(y,x)\in q$. A CQ $q$ gives rise to an
interpretation $\mathcal{I}_{q}$ with $\Delta^{\mathcal{I}_{q}}={\sf var}(q)$,
$A^{\mathcal{I}_{q}}=\\{x\mid A(x)\in q\\}$, and
$r^{\mathcal{I}_{q}}=\\{(x,y)\mid r(x,y)\in q\\}$ for all $A\in{\sf N_{C}}$
and $r\in{\sf N_{R}}$. A union of conjunctive queries (UCQ) $q(\bar{x})$ is a
disjunction of CQs that all have the same answer variables $\bar{x}$. The
_arity_ of $q$ is the length of $\bar{x}$, and $q$ is _Boolean_ if it is of
arity zero. An _atomic query (AQ)_ is a CQ of the simple form $A(x)$, with $A$
a concept name.

With a homomorphism from a CQ $q$ to an interpretation $\mathcal{I}$, we mean
a homomorphism from $\mathcal{I}_{q}$ to $\mathcal{I}$ (defined as usual). A
tuple $\bar{d}\in(\Delta^{\mathcal{I}})^{|\bar{x}|}$ is an _answer_ to a UCQ
$q(\bar{x})$ on an interpretation $\mathcal{I}$, written $\mathcal{I}\models
q(\bar{d})$, if there is a homomorphism $h$ from a CQ $p$ in $q$ to
$\mathcal{I}$ with $h(\bar{x})=\bar{d}$. A tuple $\bar{a}\in{\sf
ind}(\mathcal{A})$ is an _answer_ to $q$ on a cKB ${\sf Circ_{\sf
CP}}(\mathcal{K})$ with $\mathcal{K}=(\mathcal{T},\mathcal{A})$, written ${\sf
Circ_{\sf CP}}(\mathcal{K})\models q(\bar{a})$, if $\mathcal{I}\models
q(\bar{a})$ for all models $\mathcal{I}$ of ${\sf Circ_{\sf
CP}}(\mathcal{K})$.

######  Example 1.

Consider a database about universities. The TBox contains domain knowledge
such as

$\begin{array}[]{rcl}{\sf University}&\sqsubseteq&{\sf
Organization}\\\\[2.84526pt] {\sf Organization}&\sqsubseteq&{\sf
Public}\sqcup{\sf Private}\\\\[2.84526pt] {\sf Public}\sqcap{\sf
Private}&\sqsubseteq&\bot.\end{array}$

Circumscription can be used to express defeasible inclusions. For example,
from a European perspective, universities are usually public:

$\begin{array}[]{rcl}{\sf University}&\sqsubseteq&{\sf Public}\sqcup{\sf
Ab}_{U}\end{array}$

where ${\sf Ab}_{U}$ is a fresh ‘abnormality’ concept name that is minimized.
If the ABox contains

${\sf University}({\sf leipzigu}),{\sf University}({\sf mit}),{\sf
Private}({\sf mit})$

and we pose the CQ $q(x)={\sf Organization}(x)\wedge{\sf Public}(x)$, then the
answer is ${\sf leipzigu}$.

We may also use circumscription to implement a soft closed-world assumption,
similar in spirit to soft constraints in constraint satisfaction. Assume that
the ABox additionally contains a database of nonprofit corporations:

$\begin{array}[]{rl}{\sf NPC}({\sf greenpeace})&{\sf NPC}({\sf
wwf})\end{array}$

and that this database is _essentially complete_ , expressed by minimizing
${\sf NPC}$. If we also know that

$\begin{array}[]{@{}c@{}}\begin{array}[]{rcl}{\sf
IvyLeagueU}&\sqsubseteq&\exists{\sf ownedBy}.({\sf NPC}\sqcap{\sf
Rich})\\\\[2.84526pt] {\sf DonationBased}&\sqsubseteq&\neg{\sf
Rich}\end{array}{}\\\\[8.53581pt] \begin{array}[]{rcl}{\sf DonationBased}({\sf
greenpeace})&{\sf DonationBased}({\sf wwf})\\\\[2.84526pt] {\sf
IvyLeagueU}({\sf harvard})\end{array}\end{array}$

then we are forced to infer that our list of NPCs was not actually complete as
all explicitly known NPCs are not rich, but a rich NPC must exist. A strict
closed-world assumption would instead result in an inconsistency.

Let $\mathcal{L}$ be a description logic such as $\mathcal{ALCHIO}$ or ${\cal
EL}$ and let $\mathcal{Q}$ be a query language such as UCQ, CQ, or AQ. With
_$\mathcal{Q}$ evaluation on circumscribed $\mathcal{L}$ KBs_, we mean the
problem to decide, given an $\mathcal{L}$ cKB ${\sf Circ_{\sf
CP}}(\mathcal{K})$ with $\mathcal{K}=(\mathcal{T},\mathcal{A})$, a query
$q(\bar{x})$ from $\mathcal{Q}$, and a tuple $\bar{a}\in{\sf
ind}(\mathcal{A})^{|\bar{x}|}$, whether ${\sf Circ_{\sf
CP}}(\mathcal{K})\models q(\bar{a})$. When studying the combined complexity of
this problem, all of ${\sf Circ_{\sf CP}}(\mathcal{K})$, $q$, and $\bar{a}$
are treated as inputs. For data complexity, in contrast, we assume $q$,
$\mathcal{T}$, and ${\sf CP}$ to be fixed and thus of constant size.

##  3 Between $\mathcal{ALCHIO}$ and ${\cal EL}$

We study the complexity of query evaluation on circumscribed KBs for DLs
between $\mathcal{ALCHIO}$ and ${\cal EL}$. In fact, we prove 2Exp-
completeness in combined complexity and $\Uppi^{\mathrm{P}}_{2}$-completeness
in data complexity for all these DLs.

###  3.1 Fundamental Observations

We start with some fundamental observations that underlie the subsequent
proofs, first observing a reduction from UCQ evaluation on circumscribed
$\mathcal{ALCHIO}$ KBs to UCQ evaluation on circumscribed $\mathcal{ALCHI}$
KBs. Note that a nominal may be viewed as a (strictly) closed concept name
with a single instance. This reduction is a simple version of a reduction from
query evaluation with closed concept names to query evaluation on cKBs in the
proof of Theorem 2 below.

######  Proposition 1.

UCQ evaluation on circumscribed $\mathcal{ALCHIO}$ KBs can be reduced in
polynomial time to UCQ evaluation on circumscribed $\mathcal{ALCHI}$ KBs.

###### Proof.

Let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be an $\mathcal{ALCHIO}$ cKB, with
$\mathcal{K}=(\mathcal{T},\mathcal{A})$, and let $q(\bar{x})$ be a UCQ. Let
$N$ be the set of individual names $a$ such that the nominal $\\{a\\}$ is used
in $\mathcal{T}$. Introduce fresh concept names $A_{a},B_{a},D_{a}$ for every
$a\in N$. We obtain $\mathcal{T}^{\prime}$ from $\mathcal{T}$ by replacing
every $a\in N$ with $A_{a}$ and adding the CI $A_{a}\sqcap\neg
B_{a}\sqsubseteq D_{a}$, $\mathcal{A}^{\prime}$ from $\mathcal{A}$ by adding
$A_{a}(a)$ and $B_{a}(a)$ for every $a\in N$, and $q^{\prime}$ from $q$ by
adding the disjunct $\exists y\,D_{a}(y)$ for every $a\in N$.111Strictly
speaking, we need to adjust $\exists y\,D_{a}(y)$ so that it has the same
answer variables as the other CQs in $q$. This is easy by adding to
$\mathcal{T}^{\prime}$ a CI $\top\sqsubseteq T$ for a fresh concept name $T$
and extending $\exists y\,D_{a}(y)$ with atom $T(x)$ for every answer variable
$x$. Set $\mathcal{K}^{\prime}=(\mathcal{T}^{\prime},\mathcal{A}^{\prime})$.
The circumscription pattern ${\sf CP}^{\prime}$ is obtained from ${\sf CP}$ by
minimizing the concept names $B_{a}$ with higher preference than any other
concept name (and with no preferences between them). We show in the appendix
that ${\sf Circ_{\sf CP}}(\mathcal{K})\models q(\bar{a})$ iff ${\sf
Circ}_{{\sf CP}^{\prime}}(\mathcal{K}^{\prime})\models q^{\prime}(\bar{a})$
for all $\bar{a}\in{\sf ind}(\mathcal{A})^{|\bar{x}|}$. ∎

We are thus left with $\mathcal{ALCHI}$ KBs. We generally assume that TBoxes
are in _normal form_ , meaning that every concept inclusion in $\mathcal{T}$
has one of the following shapes:

$\begin{array}[]{r<EMAIL_ADDRESS>3.0pt plus 1.0pt minus 1.0pt\\\
{{A_{1}}}\sqcap{{A_{2}}}\sqsubseteq{{A}}&{{A}}\sqsubseteq{{\lnot B}}&{{\lnot
B}}\sqsubseteq{{A}}\end{array}$

where ${{A,A_{1},A_{2},B}}$ range over ${\sf N_{C}}$ and $r$ ranges over
roles. The set of concept names in $\mathcal{T}$ is denoted
$\mathsf{N_{C}}(\mathcal{T})$.

######  Lemma 1.

Every $\mathcal{ALCHI}$ TBox $\mathcal{T}$ can be transformed in linear time
into an $\mathcal{ALCHI}$ TBox $\mathcal{T}^{\prime}$ in normal form such that
for all cKBs ${\sf Circ_{\sf CP}}(\mathcal{T},\mathcal{A})$, UCQs $q(\bar{x})$
that do not use symbols from ${\sf sig}(\mathcal{T}^{\prime})\setminus{\sf
sig}(\mathcal{T})$, and $\bar{a}\in{\sf ind}(\mathcal{A})^{|\bar{x}|}$: ${\sf
Circ_{\sf CP}}(\mathcal{T},\mathcal{A})\models q(\bar{a})\text{ iff }{\sf
Circ_{\sf CP}}(\mathcal{T}^{\prime},\mathcal{A})\models q(\bar{a}).$

Let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be a cKB with
$\mathcal{K}=(\mathcal{T},\mathcal{A})$. A _type_ is a set of concept names
$t\subseteq\mathsf{N_{C}}(\mathcal{T})$. For an interpretation $\mathcal{I}$
and $d\in\Delta^{\mathcal{I}}$, we define
$\mathsf{tp}_{\mathcal{I}}({d})\coloneqq\\{{{A}}\in\mathsf{N_{C}}(\mathcal{T})\mid
d\in{{A}}^{\mathcal{I}}\\}.$ For a subset
$\Delta\subseteq\Delta^{\mathcal{I}}$, we set
$\mathsf{tp}_{\mathcal{I}}({\Delta})=\\{\mathsf{tp}_{\mathcal{I}}({d})\mid
d\in\Delta\\}$. We further write $\mathsf{TP}(\mathcal{I})$ for
$\mathsf{tp}_{\mathcal{I}}({\Delta^{\mathcal{I}}})$. Finally, we set

$\mathsf{TP}(\mathcal{T})\coloneqq\bigcup_{\mathcal{I}\text{ model of
}\mathcal{T}}\mathsf{TP}(\mathcal{I}).$

For a role $r$, we write $t\rightsquigarrow_{{r}}t^{\prime}$ if for all
${{A,B}}\in\mathsf{N_{C}}$:

  * •

${{B}}\in t^{\prime}$ and
$\mathcal{T}\models\exists{{r}}.{{B}}\sqsubseteq{{A}}$ implies ${{A}}\in t$
and

  * •

${{B}}\in t$ and $\mathcal{T}\models\exists{{r}}^{-}.{{B}}\sqsubseteq{{A}}$
implies ${{A}}\in t^{\prime}$.

We next show how to identify a ‘core’ part of a model $\mathcal{I}$ of
$\mathcal{K}$. These cores will play an important role in dealing with
circumscription in our upper bound proofs.

######  Definition 1.

Let $\mathcal{I}$ be a model of $\mathcal{K}$. We use ${\sf TP}_{{\sf
core}}(\mathcal{I})$ to denote the set of all types $t\in{\sf
TP}(\mathcal{I})$ such that

$|\\{d\in\Delta^{\mathcal{I}}\setminus{\sf ind}(\mathcal{A})\mid{\sf
tp}_{\mathcal{I}}(d)=t\\}|<|{\sf TP}(\mathcal{T})|$

and set ${\sf TP}_{\overline{{\sf core}}}(\mathcal{I})={\sf
TP}(\mathcal{I})\setminus{\sf TP}_{{\sf core}}(\mathcal{I})$ and

$\Delta^{\mathcal{I}}_{\sf core}=\\{d\in\Delta^{\mathcal{I}}\mid{\sf
tp}_{\mathcal{I}}(d)\in{\sf TP}_{{\sf core}}(\mathcal{I})\\}.$

So the core consists of all elements whose types are realized not too often,
except possibly in the ABox. A good way of thinking about cores is that if a
model $\mathcal{I}$ of $\mathcal{K}$ is minimal w.r.t. $<_{\sf CP}$, then all
instances of minimized concept names are in the core. This is, however not
strictly true since we may have $A\sqsubseteq B$ where $A$ is $\top$ or fixed,
and $B$ is minimized.

The following crucial lemma provides a sufficient condition for a model
$\mathcal{J}$ of $\mathcal{K}$ to be minimal w.r.t. $<_{\sf CP}$, relative to
a model $\mathcal{I}$ of $\mathcal{K}$ that is known to be minimal w.r.t.
$<_{\sf CP}$.

######  Lemma 2 (Core Lemma).

Let $\mathcal{I}$ be a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$ and let
$\mathcal{J}$ be a model of $\mathcal{K}$ with $\Delta^{\mathcal{I}}_{\sf
core}\subseteq\Delta^{\mathcal{J}}$. If

  1. 1.

${\sf tp}_{\mathcal{I}}(d)={\sf tp}_{\mathcal{J}}(d)$ for all
$d\in\Delta^{\mathcal{I}}_{\sf core}$ and

  2. 2.

${\sf tp}_{\mathcal{J}}(\Delta^{\mathcal{J}}\setminus\Delta^{\mathcal{I}}_{\sf
core})={\sf TP}_{\overline{{\sf core}}}(\mathcal{I})$,

then $\mathcal{J}$ is a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$.

We give a sketch of the proof of (the contrapositive of) Lemma 2. Assume that
$\mathcal{J}$ is not a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$. Then there
must be a model $\mathcal{J}^{\prime}$ of $\mathcal{K}$ with
$\mathcal{J}^{\prime}<_{\sf CP}\mathcal{J}$ and to obtain a contradiction it
suffices to construct from $\mathcal{J}^{\prime}$ a model
$\mathcal{I}^{\prime}$ of $\mathcal{K}$ with $\mathcal{I}^{\prime}<_{\sf
CP}\mathcal{I}$. Note that $\mathcal{I}$ and $\mathcal{J}$ may have domains of
different sizes. The elements of $\Delta^{\mathcal{I}}_{{\sf core}}$ receive
the same type in $\mathcal{I}^{\prime}$ as in $\mathcal{J}^{\prime}$. For each
non-core type $t$ in $\mathcal{I}$, we consider the set $S_{t}$ of types in
$\mathcal{J}^{\prime}$ of those elements that have type $t$ in $\mathcal{J}$.
Since $t$ is realized in $\mathcal{I}$ at least $|{\sf TP}(\mathcal{T})|$ many
times, we have enough room to realize in $\mathcal{I}^{\prime}$ exactly the
types from $S_{t}$ among those elements that had type $t$ in $\mathcal{I}$,
that is, within $(\mathsf{tp}_{\mathcal{I}})^{-1}(t)$. It is easy to see that
$\mathcal{I}^{\prime}$ is a model of $\mathcal{K}$: it satisfies $\mathcal{T}$
as it realizes the same types as $\mathcal{J}^{\prime}$ and it satisfies
$\mathcal{A}$ since $\mathcal{I}^{\prime}|_{{\sf
ind}(\mathcal{A})}=\mathcal{J}^{\prime}|_{{\sf ind}(\mathcal{A})}$. By
construction and since $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{J}$, it further
satisfies $\mathcal{I}^{\prime}<_{\sf CP}\mathcal{I}$.

We next use the core lemma to show that if ${\sf Circ_{\sf
CP}}(\mathcal{K})\not\models q(\bar{a})$ for any CQ $q$ and $\bar{a}\in{\sf
ind}(\mathcal{A})^{|\bar{x}|}$, then this is witnessed by a countermodel
$\mathcal{I}$ that has a regular shape. Here and in what follows, a
_countermodel_ is a model $\mathcal{I}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$
with $\mathcal{I}\not\models q(\bar{a})$. By regular shape, we mean that there
is a ‘base part’ that contains the ABox, the core of $\mathcal{I}$, as well as
some additional elements; all other parts of $\mathcal{I}$ are tree-shaped
with their root in the base part, and potentially with edges that go back to
the core (but not to other parts of the base!). We next make this precise.

Let $\mathcal{I}$ be a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$. Set
$\Omega=\\{rA\mid B\sqsubseteq\exists r.A\in\mathcal{T}\\}$ and fix a function
$f$ that chooses, for every $d\in\Delta^{\mathcal{I}}$ and $rA\in\Omega$ with
$d\in(\exists r.A)^{\mathcal{I}}$, an element $f(d,rA)=e\in A^{\mathcal{I}}$
such that $(d,e)\in r^{\mathcal{I}}$. Further choose, for every
$t\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$, a representative
$e_{t}\in\Delta^{\mathcal{I}}$ with ${\sf tp}_{\mathcal{I}}(e_{t})=t$. We
inductively define the set $\mathcal{P}$ of _paths through $\mathcal{I}$_
along with a mapping $h$ assigning to each $p\in\mathcal{P}$ an element of
$\Delta^{\mathcal{I}}$:

  * •

each element $d$ of the set

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

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

  * •

if $p\in\mathcal{P}$ with $h(p)=d$ and $rA\in\Omega$ with $f(d,rA)$ defined
and not from $\Delta^{\mathcal{I}}_{{\sf core}}$, then $p^{\prime}=prA$ is a
path in $\mathcal{P}$ and $h(p^{\prime})=f(d,rA)$.

For every role $r$, define

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

Now the _unraveling_ of $\mathcal{I}$ is defined by setting

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

for all concept names $A$ and role names $r$. It is easy to verify that $h$ is
a homomorphism from $\mathcal{I}^{\prime}$ to $\mathcal{I}$. This version of
unraveling is inspired by constructions from (?) where the resulting model is
called an _interlacing_.

######  Lemma 3.

Let $q(\bar{x})$ be a UCQ and $\bar{a}\in{\sf ind}(\mathcal{A})$. If
$\mathcal{I}$ is a countermodel against ${\sf Circ_{\sf
CP}}(\mathcal{K})\models q(\bar{a})$, then so is its unraveling
$\mathcal{I}^{\prime}$.

For some of our upper bound proofs, it will be important that the reference
model $\mathcal{I}$ in the core lemma is finite and sufficiently small. The
following lemma shows that we can always achieve this.

######  Lemma 4.

Let $\mathcal{I}$ be a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$. There
exists a model $\mathcal{J}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$ such that
$|\Delta^{\mathcal{J}}|\leq{\left|{\mathcal{A}}\right|}+2^{2{\left|{\mathcal{T}}\right|}}$,
$\mathcal{I}|_{\Delta_{\mathsf{core}}^{\mathcal{I}}}=\mathcal{J}|_{\Delta_{\mathsf{core}}^{\mathcal{J}}}$,
and
$\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})=\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{J})$.

In the proof of Lemma 4, we construct the desired model $\mathcal{J}$ by
starting from $\mathcal{I}|_{{\sf
ind}(\mathcal{A})\cup\Delta_{\mathsf{core}}^{\mathcal{I}}}$ and adding exactly
$m={\left|{\mathsf{TP}(\mathcal{T})}\right|}$ instances of each type from
$\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$.

###  3.2 Combined complexity

We show that in any DL between ${\cal EL}$ and $\mathcal{ALCHIO}$, the
evaluation of CQs and UCQs on cKBs is 2Exp-complete w.r.t. combined
complexity, starting with the upper bound.

######  Theorem 1.

UCQ evaluation on circumscribed $\mathcal{ALCHIO}$ KBs is in 2Exp w.r.t.
combined complexity.

By Proposition 1, it suffices to consider $\mathcal{ALCHI}$. Assume that we
are given as an input an $\mathcal{ALCHI}$ cKB ${\sf Circ_{\sf
CP}}(\mathcal{K})$ with $\mathcal{K}=(\mathcal{T},\mathcal{A})$, a UCQ
$q(\bar{x})$, and a tuple $\bar{a}\in{\sf ind}(\mathcal{A})^{|\bar{x}|}$. We
have to decide whether or not there is a countermodel $\mathcal{I}$ against
${\sf Circ_{\sf CP}}(\mathcal{K})\models q(\bar{a})$.

Fix a set $\Delta$ of size $|{\sf ind}(\mathcal{A})|+2^{2|\mathcal{T}|+1}$
such that ${\sf ind}(\mathcal{A})\subseteq\Delta$. Note that $\Delta$ is
sufficiently large so that we may assume the base domain
$\Delta^{\mathcal{I}}_{{\sf base}}$ of unraveled interpretations to be a
subset of $\Delta$. In an outer loop, our algorithm iterates over all triples
$(\mathcal{I}_{{\sf base}},\Delta_{{\sf core}},T_{\mathsf{\overline{core}}})$
such that the following conditions are satisfied:

  * •

$\mathcal{I}_{{\sf base}}$ is a model of $\mathcal{A}$ with $\Delta_{{\sf
core}}\subseteq\Delta^{\mathcal{I}_{{\sf base}}}\subseteq\Delta$;

  * •

$\mathsf{tp}_{\mathcal{I}_{\mathsf{base}}}({\Delta^{\mathcal{I}_{\mathsf{base}}}\setminus\Delta_{{\sf
core}}})=T_{\mathsf{\overline{core}}}$;

  * •

$\mathsf{tp}_{\mathcal{I}_{\mathsf{base}}}({\Delta_{{\sf core}}})\cap
T_{\mathsf{\overline{core}}}=\emptyset$.

For each triple $(\mathcal{I}_{{\sf base}},\Delta_{{\sf
core}},T_{\mathsf{\overline{core}}})$, we then check whether the following
additional conditions are satisfied:

(I)

$\mathcal{I}_{{\sf base}}$ can be extended to a model $\mathcal{I}$ of
$\mathcal{T}$ such that

  1. (a)

$\mathcal{I}|_{\Delta^{\mathcal{I}_{{\sf base}}}}=\mathcal{I}_{{\sf base}}$,

  2. (b)

${\sf tp}_{\mathcal{I}}(\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{{\sf
base}}})\subseteq T_{\mathsf{\overline{core}}}$, and

  3. (c)

$\mathcal{I}\not\models q(\bar{a})$;

(II)

there exists a model $\mathcal{J}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$ such
that $\mathcal{J}|_{\Delta^{\mathcal{J}}_{{\sf core}}}=\mathcal{I}_{{\sf
base}}|_{\Delta_{{\sf core}}}$ and
$\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{J})=T_{\mathsf{\overline{core}}}$.

We return ‘yes’ if all triples fail the check and ‘no’ otherwise.

If the checks succeed, then the model $\mathcal{I}$ of $\mathcal{K}$ from
Condition (I) is a countermodel against ${\sf Circ_{\sf
CP}}(\mathcal{K})\models q(\bar{a})$. In particular, we may apply Lemma 2,
using the model $\mathcal{J}$ from Condition (II) as the reference model, to
show that $\mathcal{I}$ is minimal w.r.t. $<_{{\sf CP}}$. Conversely, any
countermodel $\mathcal{I}_{0}$ against ${\sf Circ_{\sf
CP}}(\mathcal{K})\models q(\bar{a})$ can be unraveled into a countermodel
$\mathcal{I}$ from which we can read off a triple $(\mathcal{I}_{{\sf
base}},\Delta_{{\sf core}},T_{\mathsf{\overline{core}}})$ in the obvious way,
and then $\mathcal{I}$ witnesses Condition (I) and choosing
$\mathcal{J}=\mathcal{I}$ witnesses Condition (II).

Of course, we have to prove that Conditions (I) and (II) can be verified in
2Exp. This is easy for Condition (II): by Lemma 4, it suffices to consider
models $\mathcal{J}$ of size at most
${\left|{\mathcal{A}}\right|}+2^{2{\left|{\mathcal{T}}\right|}}$ and thus we
can iterate over all candidate interpretations $\mathcal{J}$ up to this size,
check whether $\mathcal{J}$ is a model of $\mathcal{K}$ with
$\mathcal{J}|_{\Delta^{\mathcal{J}}_{{\sf
core}}}=\mathcal{I}_{\mathsf{base}}|_{\Delta_{{\sf core}}}$ and
$\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{J})=T_{\mathsf{\overline{core}}}$,
and then iterate over all models $\mathcal{J}^{\prime}$ of $\mathcal{K}$ with
$\Delta^{\mathcal{J}^{\prime}}=\Delta^{\mathcal{J}}$ to check that
$\mathcal{J}$ is minimal w.r.t. $<_{{\sf CP}}$.

Condition (I) requires more work. We use a mosaic approach, that is, we
attempt to assemble the interpretation $\mathcal{I}$ from Condition (I) by
combining small pieces called _mosaics_. Each mosaic contains the base part of
$\mathcal{I}$ and at most two additional elements $e^{*}_{1},e^{*}_{2}$. We
trace partial homomorphisms from CQs in $q$ through the mosaics, as follows.

Fix a triple $(\mathcal{I}_{{\sf base}},\Delta_{{\sf
core}},T_{\mathsf{\overline{core}}})$. A _match triple_ for an interpretation
$\mathcal{J}$ takes the form $(p,\widehat{p},h)$ such that $p$ is a CQ in $q$,
$\widehat{p}\subseteq p$, and $h$ is a partial map from ${\sf
var}(\widehat{p})$ to $\Delta^{\mathcal{J}}$ that is a homomorphism from
$\widehat{p}|_{{\sf dom}(h)}$ to $\mathcal{J}$. Intuitively, $\mathcal{J}$ is
a mosaic and the triple $(p,\widehat{p},h)$ expresses that a homomorphism from
$\widehat{p}$ to $\mathcal{I}$ exists, with the variables in ${\sf dom}(h)$
being mapped to the current piece $\mathcal{J}$ and the variables in ${\sf
var}(\widehat{p})\setminus{\sf dom}(h)$ mapped to other mosaics. A match
triple is _complete_ if $\widehat{p}=p$ and _incomplete_ otherwise. To make
$\mathcal{I}$ a countermodel, we must avoid complete match triples. A
_specification_ for $\mathcal{J}$ is a set $S$ of match triples for
$\mathcal{J}$ and we call $S$ _saturated_ if the following conditions are
satisfied:

  * •

if $p$ is a CQ in $q$, $\widehat{p}\subseteq p$, and $h$ is a homomorphism
from $\widehat{p}$ to $\mathcal{J}$, then $(p,\widehat{p},h)\in S$;

  * •

if $(p,\widehat{p},h),(p,\widehat{p}^{\prime},h^{\prime})\in S$ and
$h(x)=h^{\prime}(x)$ is defined for all $x\in{\sf var}(\widehat{p})\cap{\sf
var}(\widehat{p}^{\prime})$, then
$(p,\widehat{p}\cup\widehat{p}^{\prime},h\cup h^{\prime})\in S$.

######  Definition 2.

A _mosaic_ for $(\mathcal{I}_{{\sf base}},\Delta_{{\sf
core}},T_{\mathsf{\overline{core}}})$ is a tuple $M=(\mathcal{J},S)$ where

  * •

$\mathcal{J}$ is an interpretation such that

    1. 1.

$\Delta^{\mathcal{I}_{{\sf
base}}}\subseteq\Delta^{\mathcal{J}}\subseteq\Delta^{\mathcal{I}_{{\sf
base}}}\uplus\\{e^{*}_{1},e^{*}_{2}\\}$;

    2. 2.

$\mathcal{J}|_{\Delta^{\mathcal{I}_{{\sf
base}}}}=\mathcal{I}_{\mathsf{base}}$;

    3. 3.

${\sf tp}_{\mathcal{J}}(e_{i}^{*})\in T_{\mathsf{\overline{core}}}$ if
$e_{i}^{*}\in\Delta^{\mathcal{J}}$, for $i\in\\{1,2\\}$;

    4. 4.

$\mathcal{J}$ satisfies all $\exists r.A\sqsubseteq B\in\mathcal{T}$ and all
$r\sqsubseteq s\in\mathcal{T}$.

  * •

$S$ is a saturated specification for $\mathcal{J}$ that contains only
incomplete match triples.

We use $\mathcal{J}_{M}$ to refer to $\mathcal{J}$ and $S_{M}$ to refer to
$S$.

Let $\mathcal{M}$ be a set of mosaics for $(\mathcal{I}_{{\sf
base}},\Delta_{{\sf core}},T_{\mathsf{\overline{core}}})$. We say that
$M\in\mathcal{M}$ is _good in_ $\mathcal{M}$ if for every
$e\in\Delta^{\mathcal{J}_{M}}$ and every $A\sqsubseteq\exists
r.B\in\mathcal{T}$ with $e\in(A\sqcap\neg\exists r.B)^{\mathcal{J}_{M}}$, we
find a mosaic $M^{\prime}\in\mathcal{M}$ such that the following conditions
are satisfied:

  1. 1.

${\sf tp}_{\mathcal{J}_{M}}(e)={\sf tp}_{\mathcal{J}_{M^{\prime}}}(e)$;

  2. 2.

$e\in(\exists r.B)^{\mathcal{J}_{M^{\prime}}}$;

  3. 3.

if $(p,\widehat{p},h^{\prime})\in S_{M^{\prime}}$, then $(p,\widehat{p},h)\in
S_{M}$ where $h$ is the restriction of $h^{\prime}$ to range
$\Delta^{\mathcal{I}_{{\sf base}}}\cup\\{e\\}$.

If $M$ is not good in $\mathcal{M}$, then it is _bad_. To verify Cond. (I), we
start with the set of all mosaics for $(\mathcal{I}_{{\sf base}},\Delta_{{\sf
core}},T_{\mathsf{\overline{core}}})$ and repeatedly and exhaustively
eliminate bad mosaics.

######  Lemma 5.

$\mathcal{I}_{{\sf base}}$ can be extended to a model $\mathcal{I}$ of
$\mathcal{T}$ that satisfies Conditions (a) to (c) iff at least one mosaic
survives the elimination process.

We provide a matching lower bound for Theorem 1. It is rather strong as it
already applies to CQs, to ${\cal EL}$ KBs, and uses a single minimized
concept name (and consequently no preferences) and no fixed concept names. It
is proved by a subtle reduction from CQ evaluation on ${\cal EL}$ KBs with
closed concept names, that is, with KBs $(\mathcal{T},\mathcal{A})$ enriched
with a set $\Sigma$ of closed concept names $A$ that have to be interpreted as
$A^{\mathcal{I}}=\\{a\mid A(a)\in\mathcal{A}\\}$ in all models $\mathcal{I}$.
This problem was proved to be 2Exp-hard in (?). The reduction also sheds some
light on the connection between circumscription and closing concept names.

######  Theorem 2.

CQ evaluation on circumscribed ${\cal EL}$ KBs is 2Exp-hard w.r.t. combined
complexity. This holds even with a single minimized concept name and no fixed
concept names.

###  3.3 Data complexity

We show that in any DL between ${\cal EL}$ and $\mathcal{ALCHIO}$, the
evaluation of CQs and UCQs on cKBs is $\Uppi^{\textrm{P}}_{2}$-complete w.r.t.
data complexity. We start with the upper bound.

######  Theorem 3.

UCQ evaluation on circumscribed $\mathcal{ALCHIO}$ KBs is in
$\Uppi^{\textrm{P}}_{2}$ w.r.t. data complexity.

We may again limit our attention to $\mathcal{ALCHI}$. To prove Theorem 3, we
show that if a countermodel exists, then there is one of polynomial size (with
TBox and query of constant size). Note that this is not a consequence of Lemma
4 since there is no guarantee that, if the model $\mathcal{I}$ from that lemma
is a countermodel, then so is $\mathcal{J}$. Once the size bound is in place,
we obtain the $\Uppi^{\textrm{P}}_{2}$ upper bound by a straightforward guess-
and-check procedure.

######  Lemma 6.

Let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be an $\mathcal{ALCHI}$ cKB,
$\mathcal{K}=(\mathcal{T},\mathcal{A})$, $q(\bar{x})$ a UCQ, and
$\bar{a}\in{\sf ind}(\mathcal{A})^{|\bar{x}|}$. If ${\sf Circ_{\sf
CP}}(\mathcal{K})\not\models q(\bar{a})$, then there exists a countermodel
$\mathcal{I}$ with
$|\Delta^{\mathcal{I}}|\leq({\left|{\mathcal{A}}\right|}+2^{\left|{\mathcal{T}}\right|})^{{\left|{\mathcal{T}}\right|}^{\left|{q}\right|}}$.

To prove Lemma 6, let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be an
$\mathcal{ALCHI}$ cKB, $\mathcal{K}=(\mathcal{T},\mathcal{A})$, and let
$\mathcal{I}$ be a model of ${\sf Circ_{\sf CP}}(\mathcal{K})$ with
$\mathcal{I}\not\models q(\bar{a})$. We construct a small countermodel by
starting from the unraveling ${\mathcal{I}}^{\prime}$ of $\mathcal{I}$ and
applying a quotient construction. The latter is based on a suitable
equivalence relation on $\Delta^{\mathcal{I}^{\prime}}$ which we define next.
Recall that $\mathcal{I}^{\prime}$ consists of a base part
$\Delta_{\mathsf{base}}^{\mathcal{I}}$ and a tree-part with backedges to
$\Delta_{\mathsf{base}}^{\mathcal{I}}$.

For $n\geq 0$ and
$d\in\Delta^{\mathcal{I}^{\prime}}\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$,
we use $\mathcal{N}_{n}(d)$ to denote the _$n$ -neighborhood_ of $d$ in
${\mathcal{I}^{\prime}}$ up to $\Delta_{\mathsf{base}}^{\mathcal{I}}$, that
is, the set of all elements
$e\in\Delta^{\mathcal{I}^{\prime}}\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$
such that the undirected graph

$G_{\mathcal{I}^{\prime}}=(\Delta^{\mathcal{I}^{\prime}},\\{\\{d,e\\}\mid(d,e)\in
r^{\mathcal{I}^{\prime}}\text{ for some }r\in{\sf N_{R}}\\})$

contains a path $d_{0},\dots,d_{k}$ with $d_{0}=d$,
$d_{0},\dots,d_{k-1}\notin\Delta_{\mathsf{base}}^{\mathcal{I}}$, and
$d_{k}=e$, $0\leq k\leq n$.

Recall that the elements of $\Delta^{\mathcal{I}^{\prime}}$ are paths through
$\mathcal{I}$, sequences $p=d_{0}r_{1}A_{1}\cdots r_{n}A_{n}$ with
$d_{0}\in\Delta_{\mathsf{base}}^{\mathcal{I}}$ and $r_{i}A_{i}\in\Omega$; the
_length_ of $p$, denoted by $|p|$, is $n$. By definition of
$\mathcal{I}^{\prime}$ and of neighborhoods, for every $n\geq 0$ and
$d\in\Delta^{\mathcal{I}^{\prime}}\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$,
there is a unique path $p_{d,n}\in\mathcal{N}_{n}(d)$ that is a prefix of all
paths in $\mathcal{N}_{n}(d)$, that is, all
$e\in\mathcal{N}_{n}(d)\setminus\Delta_{\mathsf{base}}^{\mathcal{I}}$ take the
form $p_{d,n}r_{1}A_{1}\cdots r_{k}A_{k}$.

For $n\geq 0$, the equivalence relation $\sim_{n}$ on
$\Delta^{\mathcal{I}^{\prime}}$ is defined by setting $d_{1}\sim_{n}d_{2}$ if
$d_{1}=d_{2}\in\Delta_{\mathsf{base}}^{\mathcal{I}}$ or
$d_{1},d_{2}\notin\Delta_{\mathsf{base}}^{\mathcal{I}}$ and the following
conditions are satisfied:

  1. 1.

$d_{1}=p_{d_{1},n}w$ and $d_{2}=p_{d_{2},n}w$ for some $w\in\Omega^{*}$;

  2. 2.

for every $w=r_{1}A_{1}\cdots r_{k}A_{k}\in\Omega^{*}$:

$p_{d_{1},n}w\in\mathcal{N}_{n}(d_{1})\text{ iff
}p_{d_{2},n}w\in\mathcal{N}_{n}(d_{2})$

and if $p_{d_{1},n}w\in\mathcal{N}_{n}(d_{1})$, then

    1. (a)

${\sf tp}_{\mathcal{I}^{\prime}}(p_{d_{1},n}w)={\sf
tp}_{\mathcal{I}^{\prime}}(p_{d_{2},n}w)$;

    2. (b)

$(p_{d_{1},n}w,e)\in r^{\mathcal{I}^{\prime}}$ iff $(p_{d_{2},n}w,e)\in
r^{\mathcal{I}^{\prime}}$ for all roles $r$ and
$e\in\Delta_{\mathsf{base}}^{\mathcal{I}}$.

  3. 3.

$|d_{1}|\equiv|d_{2}|\\!\\!\mod 2{\left|{q}\right|}+3$.

For an element $d\in\Delta^{\mathcal{I}^{\prime}}$, we use ${\overline{d}}$ to
denote the equivalence class of $d$ w.r.t. $\sim_{{\left|{q}\right|}+1}$. The
_quotient_ $\mathcal{I}^{\prime}/{\sim}_{{\left|{q}\right|}+1}$ of
$\mathcal{I}^{\prime}$ is the interpretation whose domain is the set of all
equivalence classes of $\sim_{{\left|{q}\right|}+1}$ and where

$\begin{array}[]{rcl}A^{\mathcal{I}^{\prime}/{\sim}_{{\left|{q}\right|}+1}}&=&\\{{\overline{d}}\mid
d\in A^{\mathcal{I}^{\prime}}\\}\\\\[2.84526pt]
r^{\mathcal{I}^{\prime}/{\sim}_{{\left|{q}\right|}+1}}&=&\\{({\overline{d}},{\overline{e}})\mid(d,e)\in
r^{\mathcal{I}^{\prime}}\\}\end{array}$

for all concept names $A$ and role names $r$. It can be verified that
$|\Delta^{\mathcal{I}^{\prime}/{\sim}_{{{\left|{q}\right|}+1}}}|\leq({\left|{\mathcal{A}}\right|}+2^{\left|{\mathcal{T}}\right|})^{{\left|{\mathcal{T}}\right|}^{\left|{q}\right|}}$,
as desired.

######  Lemma 7.

Let $q(\bar{x})$ be a UCQ and $\bar{a}\in{\sf
ind}(\mathcal{A})^{{\left|{\bar{x}}\right|}}$. If $\mathcal{I}$ is a
countermodel against ${\sf Circ_{\sf CP}}(\mathcal{K})\models q(\bar{a})$,
then so is $\mathcal{I}^{\prime}/{\sim_{{{\left|{q}\right|}+1}}}$.

It is in fact straightforward to show that
$\mathcal{I}^{\prime}/{\sim_{{{\left|{q}\right|}+1}}}$ is a model of
$\mathcal{K}$. Minimality w.r.t. $<_{\sf CP}$ is proved using Lemma 2. The
most subtle part of the proof of Lemma 7 is showing that
$\mathcal{I}^{\prime}/{\sim_{{{\left|{q}\right|}+1}}}\not\models q(\bar{a})$.
This is done by exhibiting suitable ‘local’ homomorphisms from
$\mathcal{I}^{\prime}/{\sim_{{{\left|{q}\right|}+1}}}$ back to
$\mathcal{I}^{\prime}$ so that from any homomorphism from a CQ $p$ in $q$ to
$\mathcal{I}^{\prime}/{\sim_{{{\left|{q}\right|}+1}}}$ with
$h(\bar{x})=\bar{a}$, we obtain a homomorphism from $p$ to $\mathcal{I}$ with
the same property by composition. This finishes the proof of Lemmas 7 and 6
and of Theorem 3.

We next provide a matching lower bound for Theorem 3. It already applies to
AQs and ${\cal EL}$ KBs, and when there is a single minimized concept name and
no fixed concept name. It is proved by a subtle reduction from the validity of
$\forall\exists{\sf 3SAT}$ sentences. Several non-obvious technical tricks are
needed to make the reduction work with a single minimized concept name. Our
result improves upon a known coNP lower bound from (?).

######  Theorem 4.

AQ evaluation on circumscribed ${\cal EL}$ KBs is
$\Uppi^{\textrm{P}}_{2}$-hard. This holds even with a single minimized concept
name and no fixed concept names.

##  4 DL-Lite

We consider the DL-Lite family of DLs. Without circumscription, these DLs
enjoy low complexity of query evaluation, typically NP-complete in combined
complexity and in AC0 in data complexity (depending on the dialect). With
circumscription, the complexity tends to still be very high, though in some
relevant cases it is lower than in $\mathcal{ALCHIO}$.

###  4.1 Combined complexity

Our first result shows that, when role inclusions are admitted, nothing is
gained from transitioning from $\mathcal{ALCHIO}$ to DL-Lite. The proof is a
variation of that of Theorem 2, but technically much simpler.

######  Theorem 5.

UCQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf core}^{\cal H}$ KBs is
2Exp-hard w.r.t. combined complexity. This holds even with a single minimized
concept name, no fixed concept names, and no disjointness constraints.

We now move to $\textrm{DL-Lite}_{\sf bool}$ as a very expressive DL-Lite
dialect without role inclusions and observe that the combined complexity
decreases.

######  Theorem 6.

UCQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf bool}$ KBs is in coNExp
w.r.t. combined complexity.

To prove Theorem 6, we first observe that we can refine the unraveling of
countermodels $\mathcal{I}$ from Section 3.1 such that each element outside of
the base part $\Delta_{\mathsf{base}}^{\mathcal{I}}$ has at most one successor
per role. This property allows us to simplify the notion of a neighborhood in
the quotient construction in Section 3.3. This, in turn, yields the following
result. Note that in contrast to Lemma 6, there is no double exponential
dependence on $|q|$.

######  Lemma 8.

Let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be a $\textrm{DL-Lite}_{\sf bool}$ cKB
with $\mathcal{K}=(\mathcal{T},\mathcal{A})$, $q(\bar{x})$ a UCQ, and
$\bar{a}\in{\sf ind}(\mathcal{A})^{|\bar{x}|}$. If ${\sf Circ_{\sf
CP}}(\mathcal{K})\not\models q(\bar{a})$, then there exists a countermodel
$\mathcal{I}$ with
$|\Delta^{\mathcal{I}}|\leq({\left|{\mathcal{A}}\right|}+2^{\left|{\mathcal{T}}\right|})^{{\left|{q}\right|}^{2}({\left|{\mathcal{T}}\right|}+1)}$.

Lemma 8 yields a $\textnormal{\sc coNExp}^{\textnormal{\sc NP}}$ upper bound
by a straightforward guess-and-check procedure: guess a model $\mathcal{I}$ of
$\mathcal{K}$ with $\mathcal{I}\not\models q(\bar{a})$ and
$|\Delta^{\mathcal{I}}|$ bounded as in Lemma 8, and use an oracle to check
that $\mathcal{I}$ is minimal w.r.t. $<_{\sf CP}$ where the oracle decides,
given a cKB ${\sf Circ_{\sf CP}}(\mathcal{K})$ and a model $\mathcal{I}$ of
${\sf Circ_{\sf CP}}(\mathcal{K})$, whether $\mathcal{I}$ is non-minimal
w.r.t. $<_{\sf CP}$ by guessing a model $\mathcal{J}<_{\sf CP}\mathcal{I}$ of
$\mathcal{K}$; such an approach was used also in (?).

To obtain a coNExp upper bound as desired, we replace the oracle with a more
efficient method to check whether a given model $\mathcal{I}$ of $\mathcal{K}$
is minimal w.r.t. $<_{\sf CP}$. The crucial observation is that instead of
guessing a model $\mathcal{J}<_{\sf CP}\mathcal{I}$ of $\mathcal{K}$, it
suffices to consider certain interpretations $\mathcal{I}^{\prime}$ of
polynomial size, derived from sub-interpretations of $\mathcal{I}$, and guess
models $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{I}^{\prime}$ of $\mathcal{K}$.
Intuitively, we decompose an expensive ‘global’ test into exponentially many
inexpensive ‘local’ tests. This even works in the presence of role inclusions,
that is, in $\textrm{DL-Lite}_{\sf bool}^{\mathcal{H}}$, which shall be useful
in Section 5.

Let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be a $\textrm{DL-Lite}_{\sf
bool}^{\mathcal{H}}$ cKB with $\mathcal{K}=(\mathcal{T},\mathcal{A})$ and
$\mathcal{I}$ a model of $\mathcal{K}$. For each role $r$ used in
$\mathcal{T}$ such that $r^{\mathcal{I}}\neq\emptyset$, we choose a witness
$w_{r}\in(\exists r^{-})^{\mathcal{I}}$. Every
$\mathcal{P}\subseteq\Delta^{\mathcal{I}}$ gives rise to an interpretation
$\mathcal{I}_{\mathcal{P}}$ as follows:

$\begin{array}[]{r@{\;}c@{\;}l}\Delta^{\mathcal{I}_{\mathcal{P}}}&=&\mathcal{P}\cup{\sf
ind}(\mathcal{A})\cup\\{w_{r}\mid r\text{ used in
}\mathcal{T},r^{\mathcal{I}}\neq\emptyset\\}\\\\[2.84526pt]
{{A}}^{\mathcal{I}_{\mathcal{P}}}&=&{{A}}^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}}\\\\[2.84526pt]
{{r}}^{\mathcal{I}_{\mathcal{P}}}&=&{{r}}^{\mathcal{I}}\cap({\sf
ind}(\mathcal{A})\times{\sf ind}(\mathcal{A}))\\\\[2.84526pt]
&&\cup\,\\{(e,w_{s})\mid e\in(\exists
s)^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}},\mathcal{T}\models
s\sqsubseteq r\\}\\\\[2.84526pt] &&\cup\,\\{(w_{s},e)\mid e\in(\exists
s)^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}},\mathcal{T}\models
s\sqsubseteq r^{-}\\}.\end{array}$

Note that $\mathcal{I}_{\mathcal{P}}$ is derived from the subinterpretation
$\mathcal{I}|_{\mathcal{P}\cup{\sf ind}(\mathcal{A})}$ by ‘rerouting’ some
role edges to elements $w_{r}$. We have
${\left|{\mathcal{I}_{\mathcal{P}}}\right|}\leq{\left|{\mathcal{A}}\right|}+{\left|{\mathcal{T}}\right|}+{\left|{\mathcal{P}}\right|}$
and will only consider sets $\mathcal{P}$ with
${\left|{\mathcal{P}}\right|}\leq 2{\left|{\mathcal{T}}\right|}+1$. It is not
difficult to show that $\mathcal{I}_{\mathcal{P}}$ is a model of
$\mathcal{K}$, for all $\mathcal{P}\subseteq\Delta^{\mathcal{I}}$. The next
lemma characterizes the (non)-minimality of $\mathcal{I}$ in terms of the
(non)-minimality of the interpretations $\mathcal{I}_{\mathcal{P}}$.

######  Lemma 9.

The following are equivalent:

  1. 1.

There exists a model $\mathcal{I}$ of $\mathcal{K}$ with $\mathcal{J}<_{\sf
CP}\mathcal{I}$;

  2. 2.

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

It should now be clear that we have established Theorem 5. After guessing the
model $\mathcal{I}$ of $\mathcal{K}$ with $\mathcal{I}\not\models q(\bar{a})$,
we check the complement of Point 2 of Lemma 9 in a brute-force way. More
precisely, we first iterate over all
$\mathcal{P}\subseteq\Delta^{\mathcal{I}}$ with
${\left|{\mathcal{P}}\right|}\leq 2{\left|{\mathcal{T}}\right|}+1$, then over
all interpretations $\mathcal{J}_{0}$ with
$\Delta^{\mathcal{J}_{0}}=\Delta^{\mathcal{I}_{\mathcal{P}}}$ (as candidates
for the common restriction of the models
$(\mathcal{J}_{e})_{e\in\Delta^{\mathcal{I}}}$ to
${\Delta^{\mathcal{I}_{\mathcal{P}}}}$), then over all
$e\in\Delta^{\mathcal{I}}$, and finally over all models $\mathcal{J}_{e}$ of
$\mathcal{K}$ with
$\mathcal{J}_{e}|_{\Delta^{\mathcal{I}_{\mathcal{P}}}}=\mathcal{J}_{0}$, and
test whether $\mathcal{J}_{e}<_{\sf CP}\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$.
We accept if for every $\mathcal{P}$ and $\mathcal{J}_{0}$, there is an $e$
such that for all $\mathcal{J}_{e}$ the final check fails. Overall, we obtain
a coNExp algorithm.

We provide a matching lower bound that holds even for $\textrm{DL-Lite}_{\sf
core}$ cKBs. It is proved by reduction from the complement of Succinct3COL,
which is known to be NExp-complete (?).

######  Theorem 7.

UCQ answering on circumscribed $\textrm{DL-Lite}_{\sf core}$ KBs is coNExp-
hard w.r.t. combined complexity. This holds even with a single minimized
concept name, no fixed concept names, and no disjointness constraints.

###  4.2 Data complexity

We now consider data complexity, where the landscape is less diverse. Indeed,
we obtain coNP-completeness for all DLs between $\textrm{DL-Lite}_{\sf
bool}^{\mathcal{H}}$ and $\textrm{DL-Lite}_{\sf core}$, and both for UCQs and
CQs.

######  Theorem 8.

UCQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf bool}^{\mathcal{H}}$
KBs is in coNP w.r.t. data complexity.

To prove Theorem 8, we again guess a model $\mathcal{I}$ of $\mathcal{K}$ with
$\mathcal{I}\not\models q(\bar{a})$ and $|\Delta^{\mathcal{I}}|$ bounded as in
Theorem 8, and then verify that $\mathcal{I}$ is minimal w.r.t. $<_{\sf CP}$.
For the latter, we introduce a variation of Lemma 9. The original version of
Lemma 9 is not helpful because its Point 2 involves deciding whether, given an
interpretation $\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$, there is a model
$\mathcal{J}_{e}<_{\sf CP}\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$ of
$\mathcal{K}$, and given that ${\sf
ind}(\mathcal{A})\subseteq\mathcal{I}_{\mathcal{P}\cup\\{e\\}}$ there is no
reason to believe that this can be done in polynomial time in data complexity.
We actually conjecture this problem to be coNP-complete. In the following, we
vary the definition of the interpretations $\mathcal{I}_{\mathcal{P}}$ so that
their size is independent of that of $\mathcal{A}$.

Let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be a $\textrm{DL-Lite}_{\sf
bool}^{\mathcal{H}}$ cKB with $\mathcal{K}=(\mathcal{T},\mathcal{A})$ and
$\mathcal{I}$ a model of $\mathcal{K}$. We assume $\mathcal{T}$ to be in
normal form. For an element $e\in\Delta^{\mathcal{I}}$, we define its _ABox
type_ to be

$\mathsf{tp}_{\mathcal{A}}({e})=\\{A\mid A\in\mathsf{N_{C}},\mathcal{K}\models
A(e)\\}.$

Note that $\mathsf{tp}_{\mathcal{A}}({e})$ actually needs not be a proper type
as defined in Section 3 due to the presence of disjunction in $\textrm{DL-
Lite}_{\sf bool}^{\mathcal{H}}$. If $e\notin{\sf ind}(\mathcal{A})$, which is
permitted, then $\mathsf{tp}_{\mathcal{A}}({e})$ is simply the set of all
concepts names $A$ with $\mathcal{K}\models\top\sqsubseteq A$.

For each pair $(t_{1},t_{2})$ such that $\mathsf{tp}_{\mathcal{A}}({e})=t_{1}$
and $\mathsf{tp}_{\mathcal{I}}({e})=t_{2}$ for some
$e\in\Delta^{\mathcal{I}}$, we choose such an element $e_{t_{1},t_{2}}$; we
use $E$ to denote the set of all elements chosen in this way. For each role
$r$ used in $\mathcal{T}$ such that $r^{\mathcal{I}}\neq\emptyset$, we choose
an element $w_{r}\in(\exists r^{-})^{\mathcal{I}}$. Now define, for every
$\mathcal{P}\subseteq\Delta^{\mathcal{I}}$, the interpretation
$\mathcal{I}_{\mathcal{P}}$ as follows:

$\displaystyle\Delta^{\mathcal{I}_{\mathcal{P}}}=\;$
$\displaystyle\mathcal{P}\cup E\cup\\{w_{r}\mid r\text{ used in
}\mathcal{T},r^{\mathcal{I}}\neq\emptyset\\}$
$\displaystyle{{A}}^{\mathcal{I}_{\mathcal{P}}}=\;$
$\displaystyle{{A}}^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}}$
$\displaystyle{{r}}^{\mathcal{I}_{\mathcal{P}}}=\;$
$\displaystyle\\{(e,w_{s})\mid e\in(\exists
s)^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}},\mathcal{T}\models
s\sqsubseteq r\\}$ $\displaystyle\cup\\{(w_{s},e)\mid e\in(\exists
s)^{\mathcal{I}}\cap\Delta^{\mathcal{I}_{\mathcal{P}}},\mathcal{T}\models
s\sqsubseteq r^{-}\\}$

Note that ${\left|{\mathcal{I}_{\mathcal{P}}}\right|}\leq
4^{\left|{\mathcal{T}}\right|}+{\left|{\mathcal{T}}\right|}+{\left|{\mathcal{P}}\right|}$.
We also define an ABox

$\mathcal{A}_{\mathcal{P}}=\\{A(a)\mid a\in{\sf
ind}(\mathcal{A})\cap\Delta^{\mathcal{I}_{\mathcal{P}}},A\in\mathsf{tp}_{\mathcal{A}}({a})\\}$

and set $\mathcal{K}_{\mathcal{P}}=(\mathcal{T},\mathcal{A}_{\mathcal{P}})$.
The ABoxes $\mathcal{A}_{\mathcal{P}}$ act as a decomposition of the ABox
$\mathcal{A}$, similarly to how the interpretations
$\mathcal{I}_{\mathcal{P}}$ act as a decomposition of the interpretation
$\mathcal{I}$. Note that $\bigcup_{\mathcal{P}}\mathcal{A}_{\mathcal{P}}$ does
not contain role assertions. This is compensated by the use of
$\mathsf{tp}_{\mathcal{A}}({a})$ in the definition of
$\mathcal{A}_{\mathcal{P}}$ and the fact that, since $\mathcal{T}$ is in
normal form, all relevant endpoints of role assertions are ‘visible’ in the
ABox types. Note that this fails in the case of ${\cal EL}$ where dropping
role assertions could result in CIs $\exists r.B\sqsubseteq A$ to be left
unsatisfied, and such CIs are crucial for proving
$\Uppi^{\textrm{P}}_{2}$-hardness in that case, see the proof of Theorem 4.

The following is the announced variation of Lemma 9.

######  Lemma 10.

The following are equivalent:

  1. 1.

$\mathcal{I}\models{\sf Circ_{\sf CP}}(\mathcal{K})$;

  2. 2.

$\mathcal{I}_{\mathcal{P}}\models{\sf Circ_{\sf
CP}}(\mathcal{K}_{\mathcal{P}})$ for all
$\mathcal{P}\subseteq\Delta^{\mathcal{I}}$ with
${\left|{\mathcal{P}}\right|}\leq 2{\left|{\mathcal{T}}\right|}+1$.

In the “$1\Rightarrow 2$” direction we use the witnesses $e_{t_{1},t_{2}}$ to
extend a potential model $\mathcal{J}^{\prime}<_{\sf
CP}\mathcal{I}_{\mathcal{P}}$ of some $\mathcal{K}_{\mathcal{P}}$ to a model
$\mathcal{J}<_{\sf CP}\mathcal{I}$ of $\mathcal{K}$, obtaining a
contradiction. In the “$2\Rightarrow 1$” direction, for a potential model
$\mathcal{J}<_{\sf CP}\mathcal{I}$ of $\mathcal{K}$, we can find a
$\mathcal{P}$ with ${\left|{\mathcal{P}}\right|}\leq
2{\left|{\mathcal{T}}\right|}+1$ so that we can construct from $\mathcal{J}$ a
model $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{I}_{\mathcal{P}}$ of
$\mathcal{K}_{\mathcal{P}}$.

To establish Theorem 8, it thus suffices to argue that checking Point 2 of
Lemma 10 can be implemented in time polynomial in $|\mathcal{A}|$. We iterate
over all polynomially many sets $\mathcal{P}$ with
${\left|{\mathcal{P}}\right|}\leq 2{\left|{\mathcal{T}}\right|}+1$ (recall
that $\mathcal{T}$ is fixed) and check whether
$\mathcal{I}_{\mathcal{P}}\models{\sf Circ_{\sf
CP}}(\mathcal{K}_{\mathcal{P}})$ in a brute force way. To verify the
minimality of $\mathcal{I}_{\mathcal{P}}$, we iterate over all models
$\mathcal{J}$ of $\mathcal{K}_{\mathcal{P}}$ with
$\Delta^{\mathcal{J}}=\Delta^{\mathcal{I}_{\mathcal{P}}}$ (of which there are
only polynomially many, thanks to the modified definition of
$\Delta^{\mathcal{I}_{\mathcal{P}}}$), and make sure that
$\mathcal{J}\not<_{\sf CP}\mathcal{I}_{\mathcal{P}}$ for any such
$\mathcal{J}$. Overall, we obtain a coNP algorithm.

The coNP upper bound turns out to be tight, even for $\textrm{DL-Lite}_{\sf
core}$ cKBs and CQs, and with very restricted circumscription patterns. We
reduce from 3-colorability.

######  Theorem 9.

CQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf core}$ KBs is coNP-hard
w.r.t. data complexity. This holds even with a single minimized concept name,
no fixed concept names, and no disjointness constraints.

##  5 Atomic Queries

We study the evaluation of atomic queries on circumscribed KBs, which is
closely related to concept satisfiability w.r.t. such KBs. In fact, the two
problems are mutually reducible in polynomial time. Our results from this
section, summarized in Table 2, can thus also be viewed as completing the
complexity landscape for concept satisfiability, first studied in (?; ?).

|  ${\cal EL}$, $\mathcal{ALCHIO}$ |  $\textrm{DL-Lite}_{\sf bool}$, $\textrm{DL-Lite}_{\sf bool}^{\cal H}$ |  $\textrm{DL-Lite}_{\sf core}$, $\textrm{DL-Lite}_{\sf horn}^{\cal H}$
---|---|---|---
Combined complexity |  $\textnormal{\sc coNExp}^{\textnormal{\sc NP}}$-c.(†) (Thm. 10, 11) |  coNExp-c.(Thm. 12, 13) |  $\Uppi^{\textrm{P}}_{2}$-c.(‡) (Thm. 14)
Data complexity |  $\Uppi^{\textup{P}}_{2}$-c.(Thm. 3, 4) | in PTime (Thm. 15) | in PTime (Thm. 15)
Table 2: Complexity of AQ evaluation on circumscribed KBs. (†): completeness
already known for $\mathcal{ALC}(\mathcal{I}\mathcal{O})$. (‡): hardness
already known.

###  5.1 Between $\mathcal{ALCHIO}$ and ${\cal EL}$

Concept satisfiability w.r.t. circumscribed ${\cal ALCIO}$ KBs was proved to
be $\textnormal{\sc coNExp}^{\textnormal{\sc NP}}$-complete in (?). The proof
of the upper bound can easily be extended to cover also role inclusions. We
thus obtain:

######  Theorem 10.

(?) AQ evaluation on circumscribed $\mathcal{ALCHIO}$ KBs is in
$\textnormal{\sc coNExp}^{\textnormal{\sc NP}}$ w.r.t. combined complexity.

An alternative way to obtain Theorem 10 for $\mathcal{ALCHI}$ is to use Lemma
6, which yields the existence of single exponentially large countermodels in
the special case where the query $q$ is of constant size (here
${\left|{q}\right|}=1$), and a straightforward guess-and-check procedure as
sketched in Section 4.1. This can be lifted to $\mathcal{ALCHIO}$ by a
variation of (the proof of) Proposition 1 tailored to AQs.

We next prove a matching lower bound for ${\cal EL}$, improving on an Exp
lower bound from (?).

######  Theorem 11.

AQ evaluation on circumscribed ${\cal EL}$ KBs is $\textnormal{\sc
coNExp}^{\textnormal{\sc NP}}$-hard w.r.t. combined complexity. This holds
even without fixed concept names and with an empty preference order.

This is proved by a reduction from AQ evaluation on $\mathcal{ALC}$ cKBs,
which is known to be $\textnormal{\sc coNExp}^{\textnormal{\sc NP}}$-hard (?).

Regarding data complexity, it suffices to recall that Theorem 4 applies even
to AQs and ${\cal EL}$ cKBs.

###  5.2 DL-Lite

Recall that in Section 4.1, we have proved that UCQ evaluation over
$\textrm{DL-Lite}_{\sf bool}$ cKBs is in coNExp w.r.t. combined complexity. We
started with a guess-and-check procedure that gives a $\textnormal{\sc
coNExp}^{\textnormal{\sc NP}}$ upper bound, relying on countermodels of single
exponential size as per Lemma 8, and then improved to coNExp using Lemma 9.
Here, we use the same algorithm. The only difference in the correctness proof
is that Lemma 8 is replaced with Lemma 6 as the former does not support role
inclusions and the latter delivers a single exponential upper bound for
queries of constant size.

######  Theorem 12.

AQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf bool}^{\cal H}$ KBs is
in coNExp w.r.t. combined complexity.

We match this upper bound even in the absence of role inclusions,
demonstrating that evaluating AQs and UCQs over $\textrm{DL-Lite}_{\sf bool}$
cKBs is equally difficult.

######  Theorem 13.

AQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf bool}$ KBs is coNExp-
hard w.r.t. combined complexity.

The proof is by reduction from the complement of the NExp-complete problem
Succinct-3COL and relies on fixed concept names.

The situation is more favorable if we restrict our attention to $\textrm{DL-
Lite}_{\sf horn}^{\cal H}$ cKBs, which is still a very expressive dialect of
the DL-Lite family. For $\textrm{DL-Lite}_{\sf horn}^{\cal H}$, we prove that
if there is a countermodel, then there is one of linear size, in drastic
contrast to the $\textrm{DL-Lite}_{\sf bool}$ case where the proof of Theorem
13 shows that exponentially large countermodels cannot be avoided.

######  Theorem 14.

AQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf horn}^{\cal H}$ KBs is
in $\Uppi^{\textup{P}}_{2}$ w.r.t. combined complexity.

A matching lower bound for $\textrm{DL-Lite}_{\sf core}$ cKBs can be found in
(?).

We now move to data complexity, where we obtain tractability even for the
maximally expressive $\textrm{DL-Lite}_{\sf bool}^{\cal H}$ dialect of DL-
Lite.

######  Theorem 15.

AQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf bool}^{\cal H}$ KBs is
in PTime w.r.t. data complexity.

We sketch the proof of Theorem 15. Let ${\sf Circ_{\sf CP}}(\mathcal{K})$ be a
$\textrm{DL-Lite}_{\sf bool}^{\cal H}$ cKB with
$\mathcal{K}=(\mathcal{T},\mathcal{A})$, $A_{0}(x)$ an AQ, and $a_{0}\in{\sf
Ind}(\mathcal{A})$. We construct an ABox $\mathcal{A}^{\prime}$ whose size is
independent of that of $\mathcal{A}$ and which can replace $\mathcal{A}$ when
deciding whether $a_{0}$ is an answer to $A_{0}$. The construction of
$\mathcal{A}^{\prime}$ may be viewed as a variation of the constructions that
we have used in the proofs of Theorems 6 and 8 to avoid an NP oracle. In
particular, it reuses the notion of ABox types from the latter. However, the
construction employed here works directly with ABoxes rather than with
countermodels.

Let ${\sf TP}(\mathcal{A})$ denote the set of all ABox types $t$ realized in
$\mathcal{A}$, that is, all $t$ such that ${\sf tp}_{\mathcal{A}}(a)=t$ for
some $a\in{\sf Ind}(\mathcal{A})$. For every $t\in{\sf TP}(\mathcal{A})$, set

$m_{t}=\min({\left|{\\{a\in{\sf
ind}(\mathcal{A})\mid\mathsf{tp}_{\mathcal{A}}({a})=t\\}}\right|},~{}4^{\left|{\mathcal{T}}\right|})$

and choose $m_{t}$ individuals $a_{t,1},\dots,a_{t,m_{t}}\in{\sf
ind}(\mathcal{A})$ such that ${\sf tp}_{\mathcal{A}}(a_{t,i})=t$ for $1\leq
i\leq m_{t}$. We assume that the individual $a_{0}$ of interest is among the
chosen ones. Let $W$ be the set of all chosen individuals, that is,
$W=\\{a_{t,i}\mid t\in{\sf TP}(\mathcal{A}),~{}1\leq i\leq m_{t}\\}$. Now
define an ABox

$\begin{array}[]{rcl}\mathcal{A}^{\prime}&=&\\{A(a)\mid a\in
W,A\in\mathsf{tp}_{\mathcal{A}}({a})\\}\end{array}$

and set $\mathcal{K}^{\prime}=(\mathcal{T},\mathcal{A}^{\prime})$. Note that
$|{\sf ind}(\mathcal{A}^{\prime})|\leq 8^{\left|{\mathcal{T}}\right|}$, and
thus the size of $\mathcal{A}^{\prime}$ depends only on the TBox
$\mathcal{T}$, but not on the original ABox $\mathcal{A}$. Also, note that,
just like the ABoxes $\mathcal{A}_{\mathcal{P}}$ from the proof of Theorem 8,
$\mathcal{A}^{\prime}$ no longer contains role assertions.

######  Lemma 11.

${\sf Circ_{\sf CP}}(\mathcal{K})\models A_{0}(a_{0})\\!$ iff ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})\models A_{0}(a_{0})$.

It is important for the ‘only if’ direction of Lemma 11 that we keep at least
$4^{|\mathcal{T}|}$ individuals of each ABox type $t$ (if existent). In fact,
this allows us to convert a model $\mathcal{I}^{\prime}$ of ${\sf Circ_{\sf
CP}}(\mathcal{K}^{\prime})$ into a model of $\mathcal{K}$ that is minimal
w.r.t. $<_{\sf CP}$, using arguments similar to those in the proof of Lemma 2.
A crucial point is that if $a\in{\sf ind}(\mathcal{A})\setminus{\sf
ind}(\mathcal{A}^{\prime})$ and $t={\sf tp}_{\mathcal{A}}(a)$, then
$m_{t}=4^{|\mathcal{T}|}$ which implies that there is a regular type
$t^{\prime}$ such that the combination $(t,t^{\prime})$ is realized at least
$2^{\left|{\mathcal{T}}\right|}$ many times in $\mathcal{I}^{\prime}$ among
the individuals from $\mathcal{A}^{\prime}$.

Lemma 11 gives PTime membership as the size of $\mathcal{A}^{\prime}$ is
bounded by a constant. We compute $\mathcal{K}^{\prime}$ in polynomial time
and check whether ${\sf Circ_{\sf CP}}(\mathcal{K}^{\prime})\models
A_{0}(a_{0})$, which can be decided in 2Exp by Theorem 1, that is, in constant
time w.r.t. data complexity. The correctness of this procedure immediately
follows from Lemma 11.

###  5.3 Negative role inclusions

DL-Lite is often defined to additionally include negative role inclusions of
the form $r\sqsubseteq\neg s$, with the obvious semantics. It is known that
these sometimes lead to increased computational complexity; see, for example,
(?). We close by observing that this is also the case for circumscription.
While querying circumscribed DL-Lite KBs (in all considered dialects) is coNP-
complete w.r.t. data complexity for (U)CQs and in PTime for AQs, adding
negative role inclusions results in a jump back to $\Uppi^{\textrm{P}}_{2}$.
We prove this by reduction from $\forall\exists{\sf 3SAT}$. Some ideas are
shared with the proof of Theorem 4, but the general strategy of the reduction
is different.

######  Theorem 16.

AQ evaluation on circumscribed $\textrm{DL-Lite}_{\sf core}^{\cal H}$ KBs with
negative role inclusions is $\Uppi^{\textrm{P}}_{2}$-hard. This holds even
without fixed concept names and with a single negative role inclusion.

##  6 Conclusion

We have provided a rather complete picture of the complexity of query
evaluation on circumscribed KBs. Some cases, however, remain open. For
example, the lower bounds in combined complexity for UCQ evaluation on DL-Lite
cKBs given in Theorems 5 and 7 cannot be improved in an obvious way to CQs,
for which the complexity remains open. Also, the lower bounds provided in
Theorems 13, 16 and the $\Uppi^{\textrm{P}}_{2}$ one from (?) rely on the
preference relation in circumscription patterns, and it remains open whether
the complexity decreases when the preference relation is forced to be empty.
Finally, it would be interesting to study query evaluation under ontologies
that are sets of existential rules or formulated in the guarded (negation)
fragment of first-order logic, extended with circumscription. We believe that
these problems are still decidable.

## Acknowledgments

The research reported in this paper has been supported by the German Research
Foundation DFG, as part of Collaborative Research Center
(Sonderforschungsbereich) 1320 Project-ID 329551904 “EASE - Everyday Activity
Science and Engineering”, University of Bremen (http://www.ease-crc.org/). The
research was conducted in subprojects “P02 – Ontologies with Abstraction” and
“P05-N – Principles of Metareasoning for Everyday Activities”.

The authors acknowledge the financial support by the Federal Ministry of
Education and Research of Germany and by the Sächsische Staatsministerium für
Wissenschaft Kultur und Tourismus in the program Center of Excellence for AI-
research “Center for Scalable Data Analytics and Artificial Intelligence
Dresden/Leipzig”, project identification number: ScaDS.AI

This work is partly supported by BMBF (Federal Ministry of Education and
Research) in DAAD project 57616814 (SECAI, School of Embedded Composite AI) as
part of the program Konrad Zuse Schools of Excellence in Artificial
Intelligence.

## References

  * Baader et al. 2017 Baader, F.; Horrocks, I.; Lutz, C.; and Sattler, U.  2017\.  An Introduction to Description Logic.  Cambridge University Press.
  * Baader, Brandt, and Lutz 2005 Baader, F.; Brandt, S.; and Lutz, C.  2005\.  Pushing the $\mathcal{EL}$ envelope.  In Proc. of IJCAI, 364–369.  Professional Book Center.
  * Bonatti and Samarati 2003 Bonatti, P. A., and Samarati, P.  2003\.  Logics for authorization and security.  In Logics for Emerging Applications of Databases, 277–323.  Springer.
  * Bonatti et al. 2015a Bonatti, P. A.; Faella, M.; Lutz, C.; Sauro, L.; and Wolter, F.  2015a.  Decidability of circumscribed description logics revisited.  In Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation - Essays Dedicated to Gerhard Brewka on the Occasion of His 60th Birthday, volume 9060 of LNCS, 112–124.  Springer.
  * Bonatti et al. 2015b Bonatti, P. A.; Faella, M.; Petrova, I. M.; and Sauro, L.  2015b.  A new semantics for overriding in description logics.  Artif. Intell. 222:1–48.
  * Bonatti, Faella, and Sauro 2011 Bonatti, P. A.; Faella, M.; and Sauro, L.  2011\.  Defeasible inclusions in low-complexity DLs.  J. Artif. Intell. Res. 42:719–764.
  * Bonatti, Lutz, and Wolter 2006 Bonatti, P.; Lutz, C.; and Wolter, F.  2006\.  Description logics with circumscription.  In Proc. of KR2006, 400–410.  AAAI Press.
  * Bonatti, Lutz, and Wolter 2009 Bonatti, P. A.; Lutz, C.; and Wolter, F.  2009\.  The complexity of circumscription in description logic.  J. Artif. Intell. Res. 35:717–773.
  * Bonatti 2021 Bonatti, P. A.  2021\.  Query answering in circumscribed OWL2 profiles.  Annals of Mathematics and Artificial Intelligence 89(12):1155–1173.
  * Casini and Straccia 2013 Casini, G., and Straccia, U.  2013\.  Defeasible inheritance-based description logics.  J. Artif. Intell. Res. 48:415–473.
  * Eiter and Gottlob 1993 Eiter, T., and Gottlob, G.  1993\.  Propositional circumscription and extended closed-world reasoning are $\Uppi^{\textrm{P}}_{2}$-complete.  Theor. Comput. Sci. 114(2):231–245.
  * Giordano et al. 2013 Giordano, L.; Gliozzi, V.; Olivetti, N.; and Pozzato, G. L.  2013\.  A non-monotonic description logic for reasoning about typicality.  Artif. Intell. 195:165–202.
  * Lifschitz 1985 Lifschitz, V.  1985\.  Closed-world databases and circumscription.  Artif. Intell. 27(2):229–235.
  * Lutz, Seylan, and Wolter 2013 Lutz, C.; Seylan, I.; and Wolter, F.  2013\.  Ontology-based data access with closed predicates is inherently intractable (sometimes).  In Proc. of IJCAI, 1024–1030.  IJCAI/AAAI.
  * Lutz, Seylan, and Wolter 2019 Lutz, C.; Seylan, I.; and Wolter, F.  2019\.  The data complexity of ontology-mediated queries with closed predicates.  Log. Methods Comput. Sci. 15(3).
  * Manière 2022 Manière, Q.  2022\.  Counting queries in ontology-based data access.  Ph.D. Dissertation, Université de Bordeaux.
  * Motik et al. 2009 Motik, B.; Grau, B. C.; Horrocks, I.; Wu, Z.; Fokoue, A.; and Lutz, C., eds.  2009\.  OWL 2 Web Ontology Language Profiles (Second Edition).  W3C Recommendation.  Available at https://www.w3.org/TR/owl2-profiles/.
  * Ngo, Ortiz, and Simkus 2016 Ngo, N.; Ortiz, M.; and Simkus, M.  2016\.  Closed predicates in description logics: Results on combined complexity.  In Proc. of KR, 237–246.  AAAI Press.
  * Papadimitriou and Yannakakis 1986 Papadimitriou, C. H., and Yannakakis, M.  1986\.  A note on succinct representations of graphs.  Information and Control 71(3):181–185.
  * Pensel and Turhan 2018 Pensel, M., and Turhan, A.  2018\.  Reasoning in the defeasible description logic $\mathcal{EL}$ \- computing standard inferences under rational and relevant semantics.  Int. J. Approx. Reason. 103:28–70.
  * Rector 2004 Rector, A. L.  2004\.  Defaults, context, and knowledge: Alternatives for OWL-indexed knowledge bases.  In Proc. of the Pac. Symp. in Biocomp., 226–237.  World Scientific.
  * Reiter 1977 Reiter, R.  1977\.  On closed world data bases.  In Symposium on Logic and Databases, Advances in Database Theory, 55–76.  New York: Plemum Press.
  * Stefano, Ortiz, and Simkus 2022 Stefano, F. D.; Ortiz, M.; and Simkus, M.  2022\.  Pointwise circumscription in description logics.  In Proc. of DL2022, volume 3263 of CEUR Workshop Proceedings.  CEUR-WS.org.
  * Stevens et al. 2007 Stevens, R.; Aranguren, M. E.; Wolstencroft, K.; Sattler, U.; Drummond, N.; Horridge, M.; and Rector, A. L.  2007\.  Using OWL to model biological knowledge.  Int. J. Hum. Comput. Stud. 65(7):583–594.
  * Stockmeyer 1976 Stockmeyer, L. J.  1976\.  The polynomial-time hierarchy.  Theoretical Computer Science 3(1):1–22.

##  Appendix A Proofs for Section 3.1

To complete the proof of Proposition 1, it suffices to show the following.

######  Lemma 12.

${\sf Circ_{\sf CP}}(\mathcal{K})\models q(\bar{a})$ iff ${\sf Circ}_{{\sf
CP}^{\prime}}(\mathcal{K}^{\prime})\models q^{\prime}(\bar{a})$ for all
$\bar{a}\in{\sf ind}(\mathcal{A})$.

###### Proof.

First assume that ${\sf Circ_{\sf CP}}(\mathcal{K})\not\models q(\bar{a})$.
Then there is a model $\mathcal{I}$ of ${\sf Circ_{\sf CP}}(\mathcal{K})$ such
that $\mathcal{I}\not\models q(\bar{a})$. Let $\mathcal{I}^{\prime}$ be
defined like $\mathcal{I}$ except that
$A_{a}^{\mathcal{I}^{\prime}}=B_{a}^{\mathcal{I}^{\prime}}=\\{a\\}$ and
$D_{a}^{\mathcal{I}^{\prime}}=\emptyset$ for all $a\in N$. It is readily
checked that $\mathcal{I}^{\prime}$ is a model of ${\sf Circ}_{{\sf
CP}^{\prime}}(\mathcal{K}^{\prime})$ and that $\mathcal{I}^{\prime}\not\models
q^{\prime}(\bar{a})$.

Now assume that ${\sf Circ}_{{\sf
CP}^{\prime}}(\mathcal{K}^{\prime})\not\models q^{\prime}(\bar{a})$. Then
there is a model $\mathcal{I}^{\prime}$ of ${\sf Circ}_{{\sf
CP}^{\prime}}(\mathcal{K}^{\prime})$ with $\mathcal{I}^{\prime}\not\models
q^{\prime}(\bar{a})$. Since $\mathcal{I}^{\prime}$ is a model of
$\mathcal{A}^{\prime}$, we have $a\in B_{a}^{\mathcal{I}^{\prime}}$ for all
$a\in N$. Moreover, if $\\{a\\}\subsetneq B_{a}^{\mathcal{I}^{\prime}}$, then
we can find a model $\mathcal{J}^{\prime}$ of ${\sf Circ}_{{\sf
CP}^{\prime}}(\mathcal{K}^{\prime})$ with $\mathcal{J}^{\prime}<_{{\sf
CP}^{\prime}}\mathcal{I}^{\prime}$ by setting
$B_{a}^{\mathcal{J}^{\prime}}=\\{a\\}$ and
$D_{a}^{\mathcal{J}^{\prime}}=A_{a}^{\mathcal{I}^{\prime}}\setminus\\{a\\}$.
This contradicts the minimality of $\mathcal{I}^{\prime}$, and, consequently,
we must have $B_{a}^{\mathcal{I}^{\prime}}=\\{a\\}$. But then also
$A_{a}^{\mathcal{I}^{\prime}}=\\{a\\}$ since $A(a)\in\mathcal{A}^{\prime}$,
$A_{a}\sqcap\neg B_{a}\sqsubseteq D_{a}\in\mathcal{T}^{\prime}$, and the
disjunct $\exists y\,D_{a}(y)$ is not satisfied in $\mathcal{I}^{\prime}$. It
can be verified that, consequently, $\mathcal{I}^{\prime}$ is also a model of
${\sf Circ_{\sf CP}}(\mathcal{K})$, and we are done. ∎

See 1 We omit a proof of the above lemma, which is entirely standard. The same
normal form was used for $\mathcal{ALCHI}$, e.g., in (?).

See 2

###### Proof.

Assume to the contrary that $\mathcal{J}$ is not a model of ${\sf Circ_{\sf
CP}}(\mathcal{K})$. As $\mathcal{J}$ is a model of $\mathcal{K}$ by
prerequisite, there is thus a model $\mathcal{J}^{\prime}$ of $\mathcal{K}$
with $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{J}$. To derive a contradiction,
we construct a model $\mathcal{I}^{\prime}$ of $\mathcal{K}$ with
$\Delta^{\mathcal{I}^{\prime}}=\Delta^{\mathcal{I}}$ and show that
$\mathcal{I}^{\prime}<_{\sf CP}\mathcal{I}$. For each type $t\in{\sf
TP}_{\overline{{\sf core}}}(\mathcal{I})$, let

$\begin{array}[]{rcl}D_{t}&=&\\{d\in\Delta^{\mathcal{I}}\setminus{\sf
ind}(\mathcal{A})\mid{\sf tp}_{\mathcal{I}}(d)=t\\}\\\\[2.84526pt]
S_{t}&=&\\{{\sf tp}_{\mathcal{J}^{\prime}}(d)\mid
d\in\Delta^{\mathcal{J}}:{\sf tp}_{\mathcal{J}}(d)=t\\}.\end{array}$

We have

  * •

$|D_{t}|\geq|{\sf TP}(\mathcal{T})|$ by definition of
$\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$ and

  * •

$|S_{t}|\leq|{\sf TP}(\mathcal{T})|$, by definition of $S_{t}$.

Moreover, the ‘$\supseteq$’ direction of Point 2 implies $S_{t}\neq\emptyset$.
We can thus find a surjective function $\pi_{t}:D_{t}\rightarrow S_{t}$.

Let $\pi$ be the function that is obtained as the union of the (domain
disjoint) functions $\pi_{t}$, for all $t\in{\sf TP}_{\overline{{\sf
core}}}(\mathcal{I})$. By definition of $\pi$ and of
$\Delta^{\mathcal{I}}_{\sf core}$, the domain of $\pi$ is

$\Delta^{\mathcal{I}}\setminus\big{(}\Delta^{\mathcal{I}}_{\sf core}\cup{\sf
ind}(\mathcal{A})\big{)}.$

Now consider the range of $\pi$. By Point 1 and the ‘$\subseteq$’ direction of
Point 2, ${\sf tp}_{\mathcal{J}}(d)\in{\sf TP}_{\overline{{\sf
core}}}(\mathcal{I})$ iff $d\notin\Delta^{\mathcal{I}}_{\sf core}$. By
definition, the range of $\pi$ is thus

$\\{{\sf tp}_{\mathcal{J}^{\prime}}(d)\mid
d\in\Delta^{\mathcal{J}}\setminus\Delta^{\mathcal{I}}_{\sf core}\\}.$

Extend $\pi$ to domain $\Delta^{\mathcal{I}}$ by setting $\pi(d)={\sf
tp}_{\mathcal{J}^{\prime}}(d)$ for all $d\in\Delta^{\mathcal{I}}_{\sf
core}\cup{\sf ind}(\mathcal{A})$. It is easy to see that now, $\pi$ is a
surjective function from $\Delta^{\mathcal{I}}$ to ${\sf
TP}(\mathcal{J}^{\prime})$. We construct an interpretation
$\mathcal{I}^{\prime}$ as follows:

$\displaystyle\Delta^{\mathcal{I}^{\prime}}$
$\displaystyle=\Delta^{\mathcal{I}}$
$\displaystyle{{A}}^{\mathcal{I}^{\prime}}$
$\displaystyle=\\{d\in\Delta^{\mathcal{I}^{\prime}}\mid{{A}}\in\pi(d)\\}$
$\displaystyle{{r}}^{\mathcal{I}^{\prime}}$
$\displaystyle=\\{(d,e)\in\Delta^{\mathcal{I}^{\prime}}\times\Delta^{\mathcal{I}^{\prime}}\mid\pi(d)\rightsquigarrow_{{r}}\pi(e)\\}$

for all concept names $A$ and role names $r$. Notice that
$\mathsf{tp}_{\mathcal{I}^{\prime}}({d})=\pi(d)$, hence
$\mathsf{TP}(\mathcal{I}^{\prime})\subseteq\mathsf{TP}(\mathcal{J}^{\prime})$.
We first show that $\mathcal{I}^{\prime}$ is a model of $\mathcal{K}$ by
considering each possible shape of assertions and inclusion (recall that
$\mathcal{T}$ is in normal form):

  * •

${{A}}(a)$. Since $\mathcal{J}^{\prime}$ is a model of $\mathcal{K}$, we have
$a\in{{A}}^{\mathcal{J}^{\prime}}$, hence
${{A}}\in\mathsf{tp}_{\mathcal{J}^{\prime}}({a})$. By definition of $\pi$, we
have $\pi(a)=\mathsf{tp}_{\mathcal{J}^{\prime}}({a})$, hence ${{A}}\in\pi(a)$.
The definition of ${{A}}^{\mathcal{I}^{\prime}}$ yields
$a\in{{A}}^{\mathcal{I}^{\prime}}$.

  * •

${{r}}(a,b)$. Since $\mathcal{J}^{\prime}$ is a model of $\mathcal{K}$, we
have $(a,b)\in{{r}}^{\mathcal{J}^{\prime}}$, hence
$\mathsf{tp}_{\mathcal{J}^{\prime}}({a})\rightsquigarrow_{{r}}\mathsf{tp}_{\mathcal{J}^{\prime}}({b})$.
By definition of $\pi$, we have
$\pi(a)=\mathsf{tp}_{\mathcal{J}^{\prime}}({a})$ and
$\pi(b)=\mathsf{tp}_{\mathcal{J}^{\prime}}({b})$. The definition of
${{r}}^{\mathcal{I}^{\prime}}$ yields $(a,b)\in{{r}}^{\mathcal{I}^{\prime}}$.

  * •

Satisfaction of CIs of shape $\top\sqsubseteq{{A}}$,
${{A_{1}}}\sqcap{{A_{2}}}\sqsubseteq{{A}}$, ${{A}}\sqsubseteq{{\lnot B}}$ and
${{\lnot B}}\sqsubseteq{{A}}$ immediately follows from
$\mathsf{TP}(\mathcal{I}^{\prime})\subseteq\mathsf{TP}(\mathcal{J}^{\prime})$
and $\mathcal{J}^{\prime}$ being a model of $\mathcal{T}$.

  * •

${{A}}\sqsubseteq\exists{{r}}.{{B}}$. Let $d\in{{A}}^{\mathcal{I}^{\prime}}$.
Then ${{A}}\in\pi(d)$. Since $\pi(d)\in\mathsf{TP}(\mathcal{J}^{\prime})$,
there exists $d^{\prime}\in\Delta^{\mathcal{J}^{\prime}}$ such that
$\mathsf{tp}_{\mathcal{J}^{\prime}}({d^{\prime}})=\pi(d)$. Since
$\mathcal{J}^{\prime}$ is a model of $\mathcal{T}$, there exists
$e^{\prime}\in{{B}}^{\mathcal{J}^{\prime}}$ such that
$(d^{\prime},e^{\prime})\in{{r}}^{\mathcal{J}^{\prime}}$. In particular,
${{B}}\in\mathsf{tp}_{\mathcal{J}^{\prime}}({e^{\prime}})$ and
$\mathsf{tp}_{\mathcal{J}^{\prime}}({d^{\prime}})\rightsquigarrow_{{r}}\mathsf{tp}_{\mathcal{J}^{\prime}}({e^{\prime}})$.
It follows from $\pi$ being surjective that there exists
$e\in\Delta^{\mathcal{I}^{\prime}}$ with
$\pi(e)=\mathsf{tp}_{\mathcal{J}^{\prime}}({e^{\prime}})$. Then
$e\in{{B}}^{\mathcal{I}^{\prime}}$ and $(d,e)\in{{r}}^{\mathcal{I}^{\prime}}$
by definition of $\mathcal{I}^{\prime}$, hence
$d\in(\exists{{r}}.{{B}})^{\mathcal{I}^{\prime}}$.

  * •

$\exists{{r}}.{{B}}\sqsubseteq{{A}}$. Let
$d\in(\exists{{r}}.{{B}})^{\mathcal{I}^{\prime}}$. Then there exists
$e\in{{B}}^{\mathcal{I}^{\prime}}$ such that
$(d,e)\in{{r}}^{\mathcal{I}^{\prime}}$. By definition of
${{r}}^{\mathcal{I}^{\prime}}$, we have $\pi(d)\rightsquigarrow_{{r}}\pi(e)$.
Since ${{B}}\in\mathsf{tp}_{\mathcal{I}^{\prime}}({e})=\pi(e)$ and
$\exists{{r}}.{{B}}\sqsubseteq{{A}}$, the definition of
$\rightsquigarrow_{{r}}$ yields
${{A}}\in\pi(d)=\mathsf{tp}_{\mathcal{I}^{\prime}}({d})$. Thus
$d\in{{A}}^{\mathcal{I}^{\prime}}$.

  * •

$r\sqsubseteq s$. Let $(d,e)\in{{r}}^{\mathcal{I}^{\prime}}$. Then
$\pi(d)\rightsquigarrow_{{r}}\pi(e)$. Since $\mathcal{T}\models r\sqsubseteq
s$, it is immediate that $\pi(d)\rightsquigarrow_{{s}}\pi(e)$. Therefore the
definition of ${{s}}^{\mathcal{I}^{\prime}}$ yields
$(d,e)\in{{s}}^{\mathcal{I}^{\prime}}$.

It remains to show that $\mathcal{I}^{\prime}<_{\sf CP}\mathcal{I}$. We make
use of the following claim.

######  Claim 1.

$A^{\mathcal{I}^{\prime}}\odot A^{\mathcal{I}}$ iff
$A^{\mathcal{J}^{\prime}}\odot A^{\mathcal{J}}$, for each concept name $A$ and
$\odot\in\\{\subseteq,\supseteq\\}$.

Let $A$ be a concept name. We prove the claim for $\odot=\;\subseteq$ only;
for $\odot=\;\supseteq$, the arguments are similar.

“$\Rightarrow$”. Let $A^{\mathcal{I}^{\prime}}\subseteq A^{\mathcal{I}}$ and
$d\in A^{\mathcal{J}^{\prime}}$; we need to show that $d\in A^{\mathcal{J}}$.
First assume that $d\in\Delta_{\sf core}^{\mathcal{I}}$. Then ${\sf
tp}_{\mathcal{I}}(d)={\sf tp}_{\mathcal{J}}(d)$ and ${\sf
tp}_{\mathcal{I}^{\prime}}(d)={\sf tp}_{\mathcal{J}^{\prime}}(d)$. So
$A^{\mathcal{I}^{\prime}}\subseteq A^{\mathcal{I}}$ clearly implies $d\in
A^{\mathcal{J}}$, as required. Now assume that $d\notin\Delta_{\sf
core}^{\mathcal{I}}$. Let $t={\sf tp}_{\mathcal{J}}(d)$. Then ${\sf
tp}_{\mathcal{J}^{\prime}}(d)\in S_{t}$ and consequently we find a
$d^{\prime}\in D_{t}$ with $\pi(d^{\prime})={\sf
tp}_{\mathcal{J}^{\prime}}(d)$. This implies ${\sf
tp}_{\mathcal{I}^{\prime}}(d^{\prime})={\sf tp}_{\mathcal{J}^{\prime}}(d)$.
Since $d^{\prime}\in D_{t}$, we have ${\sf tp}_{\mathcal{I}}(d)=t={\sf
tp}_{\mathcal{J}}(d)$. So again, $A^{\mathcal{I}^{\prime}}\subseteq
A^{\mathcal{I}}$ implies $d\in A^{\mathcal{J}}$, as required.

“$\Leftarrow$”. Let $A^{\mathcal{J}^{\prime}}\subseteq A^{\mathcal{J}}$ and
$d\in A^{\mathcal{I}^{\prime}}$; we need to show $d\in A^{\mathcal{I}}$. First
assume that $d\in\Delta_{\sf core}^{\mathcal{I}}$. Then ${\sf
tp}_{\mathcal{I}}(d)={\sf tp}_{\mathcal{J}}(d)$ and ${\sf
tp}_{\mathcal{I}^{\prime}}(d)={\sf tp}_{\mathcal{J}^{\prime}}(d)$. So
$A^{\mathcal{J}^{\prime}}\subseteq A^{\mathcal{J}}$ clearly implies $d\in
A^{\mathcal{I}}$, as required. Now assume that $d\notin\Delta_{\sf
core}^{\mathcal{I}}$ and let $t^{\prime}={\sf tp}_{\mathcal{I}^{\prime}}(d)$.
By definition of $\mathcal{I}^{\prime}$, we have $t^{\prime}=\pi(d)$. By
definition of $\pi$, there is a $t\in{\sf TP}_{\overline{{\sf
core}}}(\mathcal{I})$ such that $t^{\prime}=\pi_{t}(d)$. Then $d\in D_{t}$ and
$t^{\prime}\in S_{t}$. The former yields ${\sf tp}_{\mathcal{I}}(d)=t$ and due
to the latter, there is a $d^{\prime}$ such that ${\sf
tp}_{\mathcal{J}}(d)=t={\sf tp}_{\mathcal{I}}(d)$ and ${\sf
tp}_{\mathcal{J}^{\prime}}(d)=t^{\prime}={\sf tp}_{\mathcal{I}^{\prime}}(d)$.
So again, $A^{\mathcal{J}^{\prime}}\subseteq A^{\mathcal{J}}$ implies $d\in
A^{\mathcal{I}}$, as required.

It is easy to see that since $\mathcal{I}^{\prime}<_{\sf CP}\mathcal{I}$, the
claim implies $\mathcal{J}^{\prime}<_{\sf CP}\mathcal{J}$. We have derived a
contradiction and conclude that $\mathcal{J}$ is a model of ${\sf Circ_{\sf
CP}}(\mathcal{K})$, as desired. ∎

See 3

###### Proof.

Let $\mathcal{I}$ be a countermodel against ${\sf Circ_{\sf
CP}}(\mathcal{K})\models q(\bar{a})$. It is clear that
$\mathcal{I}^{\prime}\not\models q[\bar{a}]$ since any homomorphism $g$ from
$q$ to $\mathcal{I}^{\prime}$ with $g(\bar{x})=\bar{a}$ could be composed with
the homomorphism $h$ from $\mathcal{I}^{\prime}$ to $\mathcal{I}$ to show that
$\mathcal{I}\models q[\bar{a}]$. It is also straightforward to verify that

  * ($*$)

${\sf tp}_{\mathcal{I}^{\prime}}(d)={\sf tp}_{\mathcal{I}}(h(d))$ for all
$d\in\Delta^{\mathcal{I}^{\prime}}$.

Using this and the definition of role extensions in $\mathcal{I}^{\prime}$, it
can be verified that $\mathcal{I}^{\prime}$ is a model of $\mathcal{K}$. Let
us consider each possible shape of assertions and axioms in our normal form:

  * •

Assertions from $\mathcal{A}$ are clearly satisfied as $\mathcal{I}$ is a
model of $\mathcal{A}$ and $\mathcal{I}^{\prime}$ preserves
$\mathcal{I}|_{\Delta_{\mathsf{base}}^{\mathcal{I}}}$ (recall ${\sf
ind}(\mathcal{A})\subseteq\Delta_{\mathsf{base}}^{\mathcal{I}}$).

  * •

Satisfaction of CIs with shape $\top\sqsubseteq{{A}}$,
${{A_{1}}}\sqcap{{A_{2}}}\sqsubseteq{{A}}$, ${{A}}\sqsubseteq{{\lnot B}}$ and
${{\lnot B}}\sqsubseteq{{A}}$ follows from remark ($*$) on types.

  * •

${{A}}\sqsubseteq\exists{{r}}.{{B}}$. Let $d\in{{A}}^{\mathcal{I}^{\prime}}$.
Thus $h(d)\in{{A}}^{\mathcal{I}}$, and since $\mathcal{I}$ models
$\mathcal{K}$, $d^{\prime}=f(h(d),r.B)$ is defined. If
$d^{\prime}\in\Delta_{\mathsf{core}}^{\mathcal{I}}$, then definition of
$\mathcal{I}^{\prime}$ yields $(d,d^{\prime})\in r^{\mathcal{I}^{\prime}}$ and
$d^{\prime}\in B^{\mathcal{I}^{\prime}}$. Otherwise, $dr.B$ is a path through
$\mathcal{I}$, and, by definition of $\mathcal{I}^{\prime}$, we have in this
case $(d,dr.B)\in r^{\mathcal{I}^{\prime}}$ and $dr.B\in
B^{\mathcal{I}^{\prime}}$. In both cases, $d\in(\exists
r.B)^{\mathcal{I}^{\prime}}$.

  * •

$\exists{{r}}.{{B}}\sqsubseteq{{A}}$. Let
$d\in(\exists{{r}}.{{B}})^{\mathcal{I}^{\prime}}$. That is, there exists
$e\in{{B}}^{\mathcal{I}^{\prime}}$ such that
$(d,e)\in{{r}}^{\mathcal{I}^{\prime}}$. Therefore $h(e)\in{{B}}^{\mathcal{I}}$
and $(h(d),h(e))\in{{r}}^{\mathcal{I}}$, ie
$h(d)\in(\exists{{r}}.{{B}})^{\mathcal{I}}$. From $\mathcal{I}$ being a model
of $\mathcal{K}$, it follows $h(d)\in A^{\mathcal{I}}$, thus $d\in
A^{\mathcal{I}^{\prime}}$.

  * •

Axioms with shape $r\sqsubseteq s$ are clearly satisfied from the definition
of $s^{\mathcal{I}^{\prime}}$.

It remains to prove that $\mathcal{I}^{\prime}$ is minimal w.r.t. $<_{\sf
CP}$. We use Lemma 2 with $\mathcal{I}$ as the reference model, and it
suffices to show that the preconditions of that lemma are satisfied. Clearly,
$\Delta_{\mathsf{core}}^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}^{\prime}}$.
Moreover, $(*)$ and the fact that $h(d)=d$ for all
$d\in\Delta_{\mathsf{core}}^{\mathcal{I}}$ implies that Condition 1 of Lemma 2
is satisfied. We next verify that Condition 2 is also satisfied. First, let
$d\in\Delta^{\mathcal{J}}\setminus\Delta_{\mathsf{core}}^{\mathcal{I}}$. We
have to show that ${\sf
tp}_{\mathcal{J}}(d)\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$.
If $d\in\Delta_{\mathsf{base}}^{\mathcal{I}}$, then $h(d)=d$. From
$d\notin\Delta_{\mathsf{core}}^{\mathcal{I}}$, we get ${\sf
tp}_{\mathcal{I}}(d)\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$
and it remains to apply ($*$). If
$d\notin\Delta_{\mathsf{base}}^{\mathcal{I}}$, then
$h(d)\notin\Delta_{\mathsf{core}}^{\mathcal{I}}$ and again we may use ($*$).
Conversely, let $t\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$. We
have to show that there is a
$d\in\Delta^{\mathcal{J}}\setminus\Delta_{\mathsf{core}}^{\mathcal{I}}$ with
${\sf tp}_{\mathcal{J}}(d)=t$. But that $d$ is $e_{t}$ since $h(e_{t})=e_{t}$
and by ($*$). ∎

See 4

###### Proof.

Let $\mathcal{K}=(\mathcal{T},\mathcal{A})$ and let $\mathcal{I}$ be a model
of ${\sf Circ_{\sf CP}}(\mathcal{K})$. Assume that
$t_{i}\notin\Delta^{\mathcal{I}}$, for every
$t\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$ and $1\leq i\leq m$.
Define $\mathcal{J}$ by setting

$\begin{array}[]{r@{~}c@{~}l}\Delta^{\mathcal{J}}~{}&=\hfil~{}&{\sf
ind}(\mathcal{A})\cup\Delta_{\mathsf{core}}^{\mathcal{I}}\cup\\{t_{i}\mid
t\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I}),1\leq i\leq m\\}\vskip
6.0pt plus 2.0pt minus 2.0pt\\\
{{A}}^{\mathcal{J}}~{}&=\hfil~{}&({{A}}^{\mathcal{I}}\cap\Delta^{\mathcal{J}})\cup\\{t_{i}\mid{{A}}\in
t,1\leq i\leq m\\}\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
{{r}}^{\mathcal{J}}~{}&=\hfil~{}&({{r}}^{\mathcal{I}}\cap(\Delta^{\mathcal{J}}\times\Delta^{\mathcal{J}}))\hfill\text{(i)}\vskip
3.0pt plus 1.0pt minus 1.0pt\\\ ~{}&\hfil~{}&\cup\,\\{(e,t_{i})\mid
e\in\Delta^{\mathcal{I}},\mathsf{tp}_{\mathcal{I}}({e})\rightsquigarrow_{{{r}}}t,1\leq
i\leq m\\}\hfill\text{(ii)}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
~{}&\hfil~{}&\cup\,\\{(t_{i},e)\mid
e\in\Delta^{\mathcal{I}},t\rightsquigarrow_{{{r}}}\mathsf{tp}_{\mathcal{I}}({e}),1\leq
i\leq m\\}\hfill\text{(iii)}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
~{}&\hfil~{}&\cup\,\\{(t_{i},t^{\prime}_{j})\mid
t\rightsquigarrow_{{{r}}}t^{\prime},1\leq i,j\leq
m\\}\hfill\text{(iv)}\end{array}$

for all concept names $A$ and role names $r$. It is easy to see that
$\mathsf{tp}_{\mathcal{J}}({e})=\mathsf{tp}_{\mathcal{I}}({e})$ for all
$e\in\Delta^{\mathcal{I}}\cap\Delta^{\mathcal{J}}$ and
$\mathsf{tp}_{\mathcal{J}}({t_{i}})=t$ for all $t\in\mathsf{TP}(\mathcal{T})$
and $1\leq i\leq m$. This implies that
$\mathcal{I}_{\mid\Delta_{\mathsf{core}}^{\mathcal{I}}}=\mathcal{J}_{\mid\Delta_{\mathsf{core}}^{\mathcal{J}}}$
and
$\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})=\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{J})$
as desired. It also implies that Conditions 1 and 2 from Lemma 2 are
satisfied. To show that $\mathcal{J}$ is a model of ${\sf Circ_{\sf
CP}}(\mathcal{K})$, it thus suffices to show that $\mathcal{J}$ is a model of
$\mathcal{K}$. It is clear by construction that $\mathcal{J}$ is a model of
$\mathcal{A}$. For $\mathcal{T}$, we consider all different forms of axioms:

  * •

Satisfaction of CIs of the form$\top\sqsubseteq{{A}}$,
${{A_{1}}}\sqcap{{A_{2}}}\sqsubseteq{{A}}$, ${{A}}\sqsubseteq{{\lnot B}}$ and
${{\lnot B}}\sqsubseteq{{A}}$ immediately follows from
$\mathsf{TP}(\mathcal{J})\subseteq\mathsf{TP}(\mathcal{I})$ and $\mathcal{I}$
being a model of $\mathcal{T}$. We distinguish two cases:

  * •

${{A}}\sqsubseteq\exists{{r}}.{{B}}$. Let $d\in{{A}}^{\mathcal{J}}$.

    * –

If $d\in\Delta^{\mathcal{I}}$, then we have $d\in{{A}}^{\mathcal{I}}$. Since
$\mathcal{I}$ is a model of $\mathcal{T}$, there exists
$e\in{{B}}^{\mathcal{I}}$ such that $(d,e)\in{{r}}^{\mathcal{I}}$. If
$e\in\Delta^{\mathcal{I}}$, then $(d,e)\in{{r}}^{\mathcal{J}}$ due to Case (i)
in the definition of $r^{\mathcal{J}}$. Otherwise
$t:=\mathsf{tp}_{\mathcal{I}}({e})\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$.
In particular, ${{B}}\in t$ and
$\mathsf{tp}_{\mathcal{I}}({d})\rightsquigarrow_{{r}}t$. Therefore
$t_{1}\in{{B}}^{\mathcal{J}}$ and $(d,t_{1})\in{{r}}^{\mathcal{J}}$ due to
Case (ii), proving $d\in(\exists{{r}}.{{B}})^{\mathcal{J}}$.

    * –

If $d\notin\Delta^{\mathcal{I}}$, then $d=t_{i}$ for some
$t\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$ and $1\leq i\leq m$.
By definition of $\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$, there
exists $d^{\prime}\in\Delta^{\mathcal{I}}$ s.t.
$\mathsf{tp}_{\mathcal{I}}({d^{\prime}})=t=\mathsf{tp}_{\mathcal{J}}({d})$.
From $d\in{{A}}^{\mathcal{J}}$, we get $A\in t$. Therefore
$d^{\prime}\in{{A}}^{\mathcal{I}}$, and since $\mathcal{I}$ is a model of
$\mathcal{T}$, there exists $e\in{{B}}^{\mathcal{I}}$ such that
$(d^{\prime},e)\in{{r}}^{\mathcal{I}}$. In particular,
${{B}}\in\mathsf{tp}_{\mathcal{I}}({e})$ and
$t\rightsquigarrow_{{r}}\mathsf{tp}_{\mathcal{I}}({e})$. If
$e\in\Delta^{\mathcal{J}}$, then $e\in B^{\mathcal{J}}$ and Case (iii) in the
definition of ${{r}}^{\mathcal{J}}$ ensures $(d,e)\in{{r}}^{\mathcal{J}}$,
which gives $d\in(\exists{{r}}.{{B}})^{\mathcal{J}}$. If
$e\notin\Delta^{\mathcal{J}}$, then
$t^{\prime}=\mathsf{tp}_{\mathcal{I}}({e})\in\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})$.
Let $e^{\prime}=t^{\prime}_{j}$ for some $j$ with $1\leq j\leq m$. Case (iv)
in the definition of ${{r}}^{\mathcal{J}}$ yields
$(d,e^{\prime})\in{{r}}^{\mathcal{J}}$, which again gives
$d\in(\exists{{r}}.{{B}})^{\mathcal{J}}$.

  * •

$\exists{{r}}.{{B}}\sqsubseteq{{A}}$. Let
$d\in(\exists{{r}}.{{B}})^{\mathcal{J}}$. Then there exists
$e\in{{B}}^{\mathcal{J}}$ such that $(d,e)\in{{r}}^{\mathcal{J}}$. From each
case in definition of ${{r}}^{\mathcal{J}}$, we easily get
$\mathsf{tp}_{\mathcal{J}}({d})\rightsquigarrow_{{r}}\mathsf{tp}_{\mathcal{J}}({e})$.
Since $e\in{{B}}^{\mathcal{J}}$ we have in particular
${{B}}\in\mathsf{tp}_{\mathcal{J}}({e})$. Combined with
$\mathcal{T}\models\exists{{r}}.{{B}}\sqsubseteq{{A}}$ and the definition of
$\mathsf{tp}_{\mathcal{J}}({d})\rightsquigarrow_{{r}}\mathsf{tp}_{\mathcal{J}}({e})$,
we obtain ${{A}}\in\mathsf{tp}_{\mathcal{J}}({d})$, that is
$d\in{{A}}^{\mathcal{J}}$.

  * •

$r\sqsubseteq s$. Let $(d,e)\in{{r}}^{\mathcal{J}}$. If this is due to Case
(i) in the definition of ${{r}}^{\mathcal{J}}$, then
$(d,e)\in{{s}}^{\mathcal{J}}$ since $\mathcal{I}$ is a model of $\mathcal{T}$.
For all other three cases, it suffices to note that, due to $r\sqsubseteq
s\in\mathcal{T}$, $t_{1}\rightsquigarrow_{{r}}t_{2}$ implies
$t_{1}\rightsquigarrow_{{s}}t_{2}$ for all types $t_{1},t_{2}$.

Finally, we remark that the size of $\Delta^{\mathcal{J}}$ is bounded by
${\left|{{\sf
ind}(\mathcal{A})}\right|}+{\left|{\Delta_{\mathsf{core}}^{\mathcal{I}}}\right|}+m\cdot{\left|{\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})}\right|}$.
From ${\left|{\Delta_{\mathsf{core}}^{\mathcal{I}}}\right|}\leq
m\cdot{\left|{\mathsf{TP}_{\mathsf{core}}(\mathcal{I})}\right|}$ and
${\left|{\mathsf{TP}_{\mathsf{core}}(\mathcal{I})}\right|}+{\left|{\mathsf{TP}_{\mathsf{\overline{core}}}(\mathcal{I})}\right|}={\left|{\mathsf{TP}(\mathcal{I})}\right|}\leq
m$ we obtain
${\left|{\Delta^{\mathcal{J}}}\right|}\leq{\left|{\mathcal{A}}\right|}+m^{2}$.
Recalling $m={\left|{\mathsf{TP}(\mathcal{T})}\right|}\leq
2^{\left|{\mathcal{T}}\right|}$, we obtain
$|\Delta^{\mathcal{J}}|\leq{\left|{\mathcal{A}}\right|}+2^{2{\left|{\mathcal{T}}\right|}}$
as required. ∎

##  Appendix B Proofs for Section 3.2

See 5

To prove the “$\Leftarrow$” direction of Lemma 5, assume we are given a good
mosaic $M_{0}$. We aim to extend $\mathcal{J}_{M_{0}}$, hence
$\mathcal{I}_{\mathsf{base}}$, into a model $\mathcal{I}$ of $\mathcal{T}$
that satisfies Conditions (a) to (c). For each good mosaic $M$, each
$e\in(A\sqcap\neg\exists r.B)^{\mathcal{J}_{M}}$ for some $A$ such that
$A\sqsubseteq\exists r.B\in\mathcal{T}$, we choose a good mosaic $M^{\prime}$
such that:

  1. 1.

${\sf tp}_{\mathcal{J}_{M}}(e)={\sf tp}_{\mathcal{J}_{M^{\prime}}}(e)$;

  2. 2.

$e\in(\exists r.B)^{\mathcal{J}_{M^{\prime}}}$;

  3. 3.

if $(p,\widehat{p},h)\in S_{M}$, then $(p,\widehat{p},h^{\prime})\in
S_{M^{\prime}}$ where $h^{\prime}$ is the restriction of $h$ to range
$\Delta^{\mathcal{I}_{{\sf base}}}\cup\\{e\\}$.

We use $\mathsf{ch}^{{{r}}.{{B}}}_{M,e}$ to denote this chosen $M^{\prime}$.
Then, starting from $M_{0}$, we build a tree-shaped set of words which
witnesses the acceptance of $M_{0}$.

######  Definition 3.

The mosaic tree $M_{0}^{+}$ is the smallest set of words such that:

  * •

$(M_{0},\emptyset,\emptyset)\in M_{0}^{+}$;

  * •

If $w\cdot(M,\\_,\\_)\in M_{0}^{+}$ and $e\in(A\sqcap\neg\exists
r.B)^{\mathcal{J}_{M}}$ for some $A$ such that $A\sqsubseteq\exists
r.B\in\mathcal{T}$, then
$w\cdot(M,\\_,\\_)\cdot(\mathsf{ch}^{{{r}}.{{B}}}_{M,e},{{r}}.{{B}},e)\in
M_{0}^{+}$.

It remains to ‘glue’ together the interpretations $\mathcal{J}_{M}$ according
to the structure of $M_{0}^{+}$. Since a mosaic $M$ may occur more than once,
we create a copy of $\mathcal{J}_{M}$ for each node in $M_{0}^{+}$ of the form
$w\cdot(M,\\_,\\_)$. We do not duplicate however elements from
$\mathcal{I}_{\mathsf{base}}$ as they precisely are those we want to reuse.
Hence only the two special elements $e^{*}_{1}$ and $e^{*}_{2}$ may be
duplicated. When a node
$w\cdot(M_{1},r_{1}.B_{1},e_{1})\cdot(M_{2},r_{2}.B_{2},e_{2})$ is
encountered, we merge element $e_{2}$ from $M_{2}$ with the already-existing
$e_{2}$ from $M_{1}$, which is indicated with a superscript
$w\cdot(M_{1},r_{1}.B_{1},e_{1})$ as follows
$e_{2}^{w\cdot(M_{1},r_{1}.B_{1},e_{1})}$. Other elements from
$\Delta^{\mathcal{J}_{M_{2}}}\setminus\Delta^{\mathcal{I}_{\mathsf{base}}}$
are considered freshly introduced by this node, which is indicated with a
matching superscript, that is:
$e^{w\cdot(M_{1},r_{1}.B_{1},e_{1})\cdot(M_{2},r_{2}.B_{2},e_{2})}$. Formally,
the copying and merging of elements is achieved by the following duplicating
functions, defined for each $w\cdot(M,r.B,e)\in M_{0}^{+}$.

$\begin{array}[]{r@{~}l}\lambda_{w\cdot(M,r.B,e)}:\Delta^{\mathcal{J}_{M}}\rightarrow\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{(e_{i}^{*})^{w},(e_{i}^{*})^{w\cdot(M,r.B,e)}\\}~{}\\\
d\mapsto\left\\{\begin{array}[]{ll}d&\text{if
}d\in\Delta^{\mathcal{I}_{\mathsf{base}}}\\\ d^{w}&\text{if
}d=e\notin\Delta^{\mathcal{I}_{\mathsf{base}}}\\\
d^{w\cdot(M,r.B,e)}&\text{otherwise}\end{array}\right.~{}\end{array}$

The desired model ${\mathcal{I}}$ can then be defined as:

${\mathcal{I}}=\bigcup_{\begin{subarray}{c}w\cdot(M,r.B,e)\in
M_{0}^{+}\end{subarray}}\lambda_{w\cdot(M,r.B,e)}({\mathcal{J}_{M}}),$

that is the domain (resp. the interpretation of each concept name and each
role name) of $\mathcal{I}$ is the union across all $w\cdot(M,r.B,e)\in
M_{0}^{+}$ of the image by $\lambda_{w\cdot(M,r.B,e)}$ of the domain (resp.
the interpretation of each concept name and each role name) of
$\mathcal{J}_{M}$.

By definition, each $\lambda_{w\cdot(M,r.B,e)}$ is a homomorphism from
$\mathcal{J}_{M}$ to ${\mathcal{I}}$. Due to Condition 1 in the definition of
good mosaics, if the range of two duplicating functions overlap, then the
common element satisfies the same concepts, so concept membership in
${\mathcal{I}}$ transfers back to $\mathcal{J}_{M}$. More formally:

######  Lemma 13.

For all $w\cdot(M,r.B,e)\in M_{0}^{+}$, all $d\in\Delta^{\mathcal{J}_{M}}$ and
all ${{A}}\in\mathsf{N_{C}}$, it holds that
$\lambda_{w\cdot(M,r.B,e)}({d})\in{{A}}^{{\mathcal{I}}}$ iff
$d\in{{A}}^{\mathcal{J}_{M}}$.

###### Proof.

Let $u_{1}=w_{1}\cdot(M_{1},r_{1}.B_{1},e_{1})\in M_{0}^{+}$ be a node from
the mosaic tree, $d_{1}$ an element from $\Delta^{\mathcal{J}_{M_{1}}}$ and
${{A}}\in\mathsf{N_{C}}$.
“$\Leftarrow$”. This is the easy direction. Assume
$d_{1}\in{{A}}^{\mathcal{J}_{M_{1}}}$. It follows from the definition of
${{A}}^{\mathcal{I}}$ that $\lambda_{u_{1}}({d_{1}})\in{{A}}^{{\mathcal{I}}}$.
“$\Rightarrow$”. Assume $\lambda_{u_{1}}({d_{1}})\in{{A}}^{{\mathcal{I}}}$. By
definition of ${{A}}^{{\mathcal{I}}}$ there exists a node
$u_{2}=w_{2}\cdot(M_{2},r_{2}.B_{2},e_{2})$ from the mosaic tree, and an
element $d_{2}\in{{A}}^{\mathcal{J}_{M_{2}}}$ such that
$\lambda_{u_{1}}({d_{1}})=\lambda_{u_{2}}({d_{2}})$. We refer to this equality
as $(*)$ and distinguish 5 cases.

  1. 1.

$d_{1}\in\Delta^{\mathcal{I}_{\mathsf{base}}}$ or
$d_{2}\in\Delta^{\mathcal{I}_{\mathsf{base}}}$.
$(*)$ yields $d_{1}=d_{2}$. Interpretation $\mathcal{J}_{M_{2}}$ preserves
$\mathcal{I}_{\mathsf{base}}$, hence
$d_{2}\in{{A}}^{\mathcal{I}_{\mathsf{base}}}$. Interpretation
$\mathcal{J}_{M_{1}}$ preserves $\mathcal{I}_{\mathsf{base}}$, hence
$d_{1}\in{{A}}^{\mathcal{J}_{M_{1}}}$.

_In the remaining cases, we thus assume
$d_{1},d_{2}\notin\Delta^{\mathcal{I}_{\mathsf{base}}}$. _

  2. 2.

$d_{1}=e_{1}$ and $d_{2}=e_{2}$.
$(*)$ yields $M_{1}=M_{2}$ and $d_{1}=d_{2}$.

  3. 3.

$d_{1}\neq e_{1}$ and $d_{2}=e_{2}$.
$(*)$ yields $w_{1}=w_{2}\cdot(M_{2},r_{2}.B_{2},e_{2})$ and $d_{1}=d_{2}$. In
particular, $M_{1}=\mathsf{ch}^{r_{2},B_{2}}_{M_{2},e_{2}}$. From Condition 1
in the definition of good mosaics, we obtain
$d_{1}\in{{A}}^{\mathcal{J}_{M_{1}}}$.

  4. 4.

$d_{1}=e_{1}$ and $d_{2}\neq e_{2}$.
The same arguments as for Case 3 but this time with
$M_{2}=\mathsf{ch}^{r_{1},B_{1}}_{M_{1},e_{1}}$.

  5. 5.

$d_{1}\neq e_{1}$ and $d_{2}\neq e_{2}$.
$(*)$ yields the existence of $w\cdot(M,r.B,e)$ such that
$w_{1}=w_{2}=w\cdot(M,r.B,e)$. It follows that $M_{1}=\mathsf{ch}^{r,B}_{M,e}$
and $M_{2}=\mathsf{ch}^{r,B}_{M,e}$. Using the same arguments as in Cases 3
and 4, we obtain $d_{1}\in{{A}}^{\mathcal{J}_{M_{1}}}$. ∎

With Lemma 13 in hand, we are ready to show that ${\mathcal{I}}$ is a model of
$\mathcal{K}$.

######  Lemma 14.

${\mathcal{I}}$ is a model of $\mathcal{K}$.

###### Proof.

We consider each possible shape of assertion and axiom in $\mathcal{K}$ w.r.t.
the normal form from Lemma 1.

  * •

Assertions ${{A}}(a)$ and ${{p}}(a,b)$ from $\mathcal{A}$ are satisfied in
$\mathcal{I}_{\mathsf{base}}$, which is preserved in $\mathcal{J}_{M_{0}}$
(Condition 2 in the definition of a mosaic), hence are also satisfied in
${\mathcal{I}}$.

  * •

Axioms with shapes ${\top}\sqsubseteq{A}$, ${A_{1}\sqcap
A_{2}}\sqsubseteq{A}$, ${{A}}\sqsubseteq{{\lnot B}}$ and ${{\lnot
B}}\sqsubseteq{{A}}$ are satisfied from Lemma 13 and the fact every mosaic is
only allowed to give proper types to its element.

  * •

Axioms with shapes $\exists{r}.A_{1}\sqsubseteq A_{2}$ and ${p}\sqsubseteq{r}$
are satisfied from Lemma 13 and Condition 4 in the definition of mosaics,
precisely requiring those to hold.

  * •

Axioms with shape ${A_{1}}\sqsubseteq\exists r.A_{2}$ are those that really
involve the mosaics. Let $d_{1}\in{{a}}_{1}^{{\mathcal{I}}}$. By definition of
${{a_{1}}}^{{\mathcal{I}}}$, there exist a node $u=w\cdot(M,\\_,\\_)\in
M_{0}^{+}$ and an element $d_{1}^{\prime}\in\Delta^{\mathcal{J}_{M}}$ such
that $d_{1}^{\prime}\in{{a_{1}}}^{\mathcal{J}_{M}}$ and
$\lambda_{u}({d_{1}^{\prime}})=d_{1}$. If $d_{1}^{\prime}\in(\exists
r.A_{2})^{\mathcal{J}_{M}}$, then we pick $d_{2}^{\prime}\in
A_{2}^{\mathcal{J}_{M}}$ and $(d_{1}^{\prime},d_{2}^{\prime})\in
r^{\mathcal{J}_{M}}$. It then follows immediately that
$\lambda_{u}({d_{2}^{\prime}})\in A_{2}^{{\mathcal{I}}}$ and
$(\lambda_{u}({d_{1}^{\prime}}),\lambda_{u}({d_{2}^{\prime}}))\in
r^{{\mathcal{I}}}$, ensuring $d_{1}\in(\exists r.A_{2})^{\mathcal{I}}$.
Otherwise $d_{1}^{\prime}\notin(\exists r.A_{2})^{\mathcal{J}_{M}}$, thus we
have $u_{0}=u\cdot(M_{0},r.A_{2},d_{1}^{\prime})\in M_{0}^{+}$ with
$M_{0}=\mathsf{ch}^{r.A_{2}}_{M,d_{1}^{\prime}}$. Notice
$\lambda_{u}({d_{1}^{\prime}})=\lambda_{u_{0}}({d_{1}^{\prime}})$. From
Condition 2 in the definition of good mosaics, we get
$d_{1}^{\prime}\in(\exists r.A_{2})^{\mathcal{J}_{M_{0}}}$ hence we pick
$d_{2}^{\prime}\in A_{2}^{\mathcal{J}_{M_{0}}}$ and
$(d_{1}^{\prime},d_{2}^{\prime})\in r^{\mathcal{J}_{M_{0}}}$. It then follows
immediately that $\lambda_{u_{0}}({d_{2}^{\prime}})\in A_{2}^{{\mathcal{I}}}$
and $(\lambda_{u_{0}}({d_{1}^{\prime}}),\lambda_{u_{0}}({d_{2}^{\prime}}))\in
r^{{\mathcal{I}}}$, ensuring $d_{1}\in(\exists r.A_{2})^{\mathcal{I}}$.

∎

This proves $\mathcal{I}_{\mathsf{base}}$ can indeed by extended into a model
of $\mathcal{T}$. Notice that Condition (a) is clearly satisfied due to
Condition 2 in the definition of mosaics. Similarly, Condition (b) is clearly
satisfied from Condition 3 in the definition of mosaics joint with Lemma 13.
It remains to verify Condition (c), that is for all $p\in q$, there is no
homomorphism from $p$ in ${\mathcal{I}}$.

By contradiction, assume there exists a CQ $p\in q$ and a homomorphism
$\pi:p\rightarrow{\mathcal{I}}$. Notice that for each $v\in\mathsf{var}(p)$
s.t. $\pi(v)\notin\Delta^{\mathcal{I}_{\mathsf{base}}}$, we thus have $w$ such
that $\pi(v)=d^{w}$ for some $d\in\\{e^{*}_{1},e^{*}_{2}\\}$. To identify from
which nodes the facts of $\pi(p)$ come involving $d^{w}$, we notice the
following consequence of the definition of functions $\lambda_{w}$ for $w\in
M_{0}^{+}$.

######  Remark 1.

Let $w\in M_{0}^{+}$ and $d\in\\{e^{*}_{1},e^{*}_{2}\\}$. For all
$w^{\prime}\cdot(M,r.B,e)\in M_{0}^{+}$, we have
$d^{w}\in\lambda_{w^{\prime}\cdot(M,r.B,e)}({\Delta^{\mathcal{J}_{M}}})$ iff
one of the two following conditions holds:

  * •

$w=w^{\prime}\cdot(M,r.B,e)$;

  * •

$w=w^{\prime}$ and $d=e$.

It follows that, for each $v\in\mathsf{var}(p)$ s.t.
$\pi(v)\notin\Delta^{\mathcal{I}_{\mathsf{base}}}$, the set of nodes
$W_{v}=\\{w^{\prime}\cdot(M,r.B,e)\in
M_{0}^{+}\mid\pi(v)\in\lambda_{w^{\prime}\cdot(M,r.B,e)}({\Delta^{\mathcal{J}_{M}}})\\}$
is finite. On $M_{0}^{+}$, we consider the order given by the prefix relation,
that for all $w_{1},w_{2}\in M_{0}^{+}$, we define $w_{1}\leq w_{2}$ iff
$w_{1}$ is a prefix of $w_{2}$. We now denote $W_{p}$ the prefix closure of
$\bigcup_{v}W_{v}$, where $v$ ranges over $v\in\mathsf{var}(p)$ s.t.
$\pi(v)\notin\Delta^{\mathcal{I}_{\mathsf{base}}}$. In particular,
$(M_{0},\emptyset,\emptyset)\in W_{p}$. For every $w\in M_{0}^{+}$, we define
the interpretation:

$\mathcal{I}_{w}=\bigcup_{\begin{subarray}{c}w^{\prime}\cdot(M,r.B,e)\in
M_{0}^{+}\\\ w\leq
w^{\prime}\cdot(M,r.B,e)\end{subarray}}\lambda_{w^{\prime}\cdot(M,r.B,e)}({\mathcal{J}_{M}}).$

We further set $p_{w}\subseteq p$ consisting of those atoms from $p$ that are
mapped by $\pi$ in $\mathcal{I}_{w}$, and $\pi_{w}$ the subsequent
homomorphism, that is the restriction of $\pi$ that maps to $\mathcal{I}_{w}$,
i.e.:

$\pi_{w}=\pi|_{\pi^{-1}(\Delta^{\mathcal{I}_{w}})}.$

In particular $p_{(M_{0},\emptyset,\emptyset)}=p$ and
$\pi_{(M_{0},\emptyset,\emptyset)}=\pi$. We now claim the following:

######  Lemma 15.

For all nodes $u=w\cdot(M,r.B,e)\in W_{p}$, we have $(p,p_{u},\pi^{\prime})\in
S_{M}$ where $\pi^{\prime}=(\lambda_{u})^{-1}\circ\pi_{u}|_{\Delta}$ with
$\Delta=\pi_{u}^{-1}(\lambda_{u}({\Delta^{\mathcal{J}_{M}}}))$.

###### Proof.

We proceed by induction on elements of $W_{p}$, starting from its finitely
many maximal elements w.r.t. $\leq$.

Base case. Assume $u=w\cdot(M,r.B,e)\in W_{p}$ is maximal for $\leq$. that is
for all $u^{\prime}\in M_{0}^{+}$ s.t. $u\leq u^{\prime}$, we have
$u^{\prime}\notin W_{p}$. In particular, for all $v\in\mathsf{var}(p)$,
$\pi(v)\in\lambda_{u^{\prime}}({{\mathcal{J}_{M^{\prime}}}})$, where
$M^{\prime}$ is the mosaic of node $u^{\prime}$, implies
$\pi(v)\in\Delta^{\mathcal{I}_{\mathsf{base}}}$. Therefore
$\pi_{u}^{-1}(\lambda_{u}({\Delta^{\mathcal{J}_{M}}}))=\mathsf{var}(p_{u})$
and, since $\mathcal{I}_{\mathsf{base}}$ is preserved in every mosaic
(Condition 2 in the definition), it follows that $p_{u}$ fully embeds in
$\lambda_{u}({\mathcal{J}_{M}})$ via $\pi_{u}$. From $S_{M}$ being saturated,
we thus have $(p,p_{u},(\lambda_{u})^{-1}\circ\pi_{u})$ which is the desired
triple.

Induction case. Consider $u=w\cdot(M,r.B,e)\in W_{p}$ and assume the property
holds for all $u\in W_{p}$ with $u\leq u^{\prime}$. We cover $p_{u}$ by the
set of all $p_{u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})}$ s.t.
$u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})\in W_{p}$ and by the
remaining atoms $p_{=u}$ from $p_{u}$. Notice that this is not a partition of
$p_{u}$ as those subqueries may overlap. In particular, two distinct
subqueries $p_{u\cdot(M_{1},r_{1}.B_{1},e_{1})}$ and
$p_{u\cdot(M_{2},r_{2}.B_{2},e_{2})}$ may only share those variables which are
mapped to $\Delta^{\mathcal{I}_{\mathsf{base}}}$ and, if $e_{1}=e_{2}$, on
$e_{1}$ (that is also $e_{2}$ in this case). Respectively,
$p_{u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})}$ and $p_{=u}$ may
only share variables that are mapped either on
$\Delta^{\mathcal{I}_{\mathsf{base}}}$ or on $e^{\prime}$. We cover as well
the homomorphism $\pi_{u}$ by all
$\pi_{u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})}$ s.t.
$u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})\in W_{p}$ and by the
homomorphism $\pi_{=u}$ which is defined as the restriction of $\pi_{u}$ to
variables from $p_{=u}$. Notice that from $S_{M}$ being saturated, we obtain
$(p,p_{=u},(\lambda_{u})^{-1}\circ\pi_{=u})\in S_{M}$. We further apply the
induction hypothesis on each
$u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})\in W_{p}$, which provides
corresponding triples
$(p,p_{u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})},\pi^{\prime})$ in
each $S_{M^{\prime}}$. From Condition 3 in the definition of good mosaics, if
follows that each
$(p,p_{u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})},\pi^{\prime\prime})$
belongs to $S_{M}$, where $\pi^{\prime\prime}$ denotes the restriction of
$\pi^{\prime}$ to range
$\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{e^{\prime}\\}$. It remains to form
the union (in the sense given in the definition of a saturated mosaic) of all
those subsequent triples, along with
$(p,p_{=u},(\lambda_{u})^{-1}\circ\pi_{=u})$, to obtain the desired triple.
Let us first focus on two triples
$(p,p_{u\cdot(M_{1},r_{1}.B_{1},e_{1})},\pi_{1}^{\prime\prime})$ and
$(p,p_{u\cdot(M_{2},r_{2}.B_{2},e_{2})},\pi_{2}^{\prime\prime})$ and consider
$v\in\mathsf{var}(p_{u\cdot(M_{1},r_{1}.B_{1},e_{1})})\cap\mathsf{var}(p_{u\cdot(M_{2},r_{2}.B_{2},e_{2})})$.
From our covering of $p_{u}$, we have seen that either
$\pi_{u}(v)\in\Delta^{\mathcal{I}_{\mathsf{base}}}$, or, if $e_{1}=e_{2}$,
that $\pi(v)=e_{1}$. In any case, restricting $\pi_{1}^{\prime}$ and
$\pi_{2}^{\prime}$ to ${\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{e_{1}\\}}$
preserved $\pi_{1}^{\prime\prime}$ and $\pi_{2}^{\prime\prime}$ being defined
on $v$, and, since issuing from the same $\pi_{u}$, equal. Let us now move to
a triple
$(p,p_{u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})},\pi^{\prime\prime})$
and the triple $(p,p_{=u},(\lambda_{u})^{-1}\circ\pi_{=u})$. Let
$v\in\mathsf{var}(p_{u\cdot(M^{\prime},r^{\prime}.B^{\prime},e^{\prime})})\cap\mathsf{var}(p_{=u})$.
From our covering of $p_{u}$, we know
$\pi_{u}(v)\in\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{e^{\prime}\\}$. Again
restricting to ${\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{e^{\prime}\\}}$
preserved $\pi^{\prime\prime}$ being defined on $v$ and, since issuing from
the same $\pi_{u}$, equal to $\pi_{=u}$ on $v$. Therefore, we can form the
union of all those triples, since they are 2-by-2 compatible, which provides
the desired triple in $S_{M}$. ∎

This concludes the proof of the “$\Leftarrow$” direction of Lemma 5, as
existence of such a homomorphism $p$ then yields a complete triple in
$S_{M_{0}}$, contradicting $M_{0}$ being a mosaic.

We now turn to the “$\Rightarrow$” direction. Assume that $\mathcal{I}_{{\sf
base}}$ can be extended to a model $\mathcal{I}$ of $\mathcal{T}$ that
satisfies Conditions (a) to (c). Up to introducing
${\left|{\mathsf{TP}(\mathcal{T})}\right|}$ copies of each element from
$\Delta^{\mathcal{I}}\setminus\Delta^{\mathcal{I}_{\mathsf{base}}}$, we can
safely assume
$\Delta_{\mathsf{base}}^{\mathcal{I}}=\Delta^{\mathcal{I}_{\mathsf{base}}}$.
Indeed, the resulting interpretations is still a model of $\mathcal{K}$ and
still satisfies Conditions (a) to (c).

Set $\mathcal{J}_{M_{0}}:=\mathcal{I}_{\mathsf{base}}$ and
$S_{M_{0}}:=\\{(p,\widehat{p},h|_{\Delta^{\mathcal{I}_{\mathsf{base}}}})\mid
p\in q,\widehat{p}\subseteq p,h:\widehat{p}\rightarrow\mathcal{I}\text{ is a
homomorphism}\\}$. Condition (c) ensures in particular that $S_{M_{0}}$ only
contains incomplete triples. We denote
$M_{0}:=(\mathcal{J}_{M_{0}},S_{M_{0}})$ this initial mosaic.

Starting from $\mathcal{M}:=\\{M_{0}\\}$, we extend $\mathcal{M}$ into a set
of mosaics in which each mosaic $M\in\mathcal{M}$ is good in $\mathcal{M}$ and
_realized in $\mathcal{I}$_, meaning that $\mathcal{J}_{M}$ homomorphically
embeds into $\mathcal{I}$. Notice $M_{0}$ is indeed realized in $\mathcal{I}$,
but may not be good in $\\{M_{0}\\}$. To pursue the construction, given a
mosaic $M\in\mathcal{M}$ being realized in $\mathcal{I}$ and some
$e\in(A\sqcap\lnot\exists r.B)^{\mathcal{J}_{M}}$ with $A\sqsubseteq\exists
r.B\in\mathcal{T}$, we show how to extract from $\mathcal{I}$ another mosaic
$N$ to succeed to $M$, and we add $N$ to $\mathcal{M}$. Since the number of
mosaics is finite, the construction of $\mathcal{M}$ terminates. We further
check that all mosaics in the resulting $\mathcal{M}$ set are good in
$\mathcal{M}$ (and in particular $M_{0}$).

To formalize the construction, we introduce along each mosaic $M$ a function
$\tau_{M}$ being a homomorphism $\mathcal{J}_{M}\rightarrow\mathcal{I}$. We
also assume chosen, for every ${{r}}.{{A}}\in\Omega$, a function
$\mathsf{succ}^{\mathcal{I}}_{{{r}}.{{A}}}$ that maps every element
$e\in(\exists{r.A})^{\mathcal{I}}$ to an element
$e^{\prime}\in\Delta^{\mathcal{I}}$ such that
$(e,e^{\prime})\in{{r}}^{\mathcal{I}}$ and $e^{\prime}\in{{A}}^{\mathcal{I}}$.

######  Definition 4.

We define $\mathcal{M}$ as the smallest set such that:

  * •

$M_{0}\in\mathcal{M}$ and we set
$\tau_{M_{0}}=\mathsf{Id}_{\mathcal{J}_{M_{0}}\rightarrow\mathcal{I}}$, where
$\mathsf{Id}_{\mathcal{J}_{M_{0}}\rightarrow\mathcal{I}}$ denotes the identity
function.

  * •

For each $M_{1}\in\mathcal{M}$ and for each $e_{1}\in(A\sqcap\lnot\exists
r.B)^{\mathcal{J}_{M_{1}}}$ with $A\sqsubseteq\exists r.B\in\mathcal{T}$, we
denote $\tau_{1}:=\tau_{M_{1}}$ and set $e_{1}^{\prime}:=\tau_{1}(e_{1})$.
Since $\tau_{1}$ is a homomorphism and $\mathcal{I}$ is a model of
$\mathcal{T}$, we obtain $e_{1}^{\prime}\in(\exists{r.B})^{\mathcal{I}}$ and
can set
$e_{2}^{\prime}:=\mathsf{succ}^{\mathcal{I}}_{{{r}}.{{B}}}(e_{1}^{\prime})$.
If $e_{2}^{\prime}\in\Delta^{\mathcal{I}_{\mathsf{base}}}$, then we set
$e_{2}:=e_{2}^{\prime}$, otherwise we set $e_{2}$ to either $e^{*}_{1}$ or
$e^{*}_{2}$ such that $e_{1}\neq e_{2}$. We let $\tau_{2}$ be the function
that maps elements of $\Delta^{\mathcal{I}_{\mathsf{base}}}$ to themselves,
$e_{1}$ to $e_{1}^{\prime}$ and $e_{2}$ to $e_{2}^{\prime}$. We now define a
new mosaic $M_{2}$. Its domain is
$\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{e_{1},e_{2}\\}$. Its
interpretation $\mathcal{J}_{M_{2}}$ is given by:

$\begin{array}[]{rcl}\Delta^{\mathcal{J}_{M_{2}}}&=&\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{e_{1},e_{2}\\}\\\
{{C}}^{\mathcal{J}_{M_{2}}}&=&{{C}}^{\mathcal{J}_{M_{0}}}\cup\\{e_{k}\mid
e_{k}^{\prime}\in{{C}}^{\mathcal{I}},k=1,2\\}\\\
{{p}}^{\mathcal{J}_{M_{2}}}&=&{{p}}^{\mathcal{J}_{M_{0}}}\cup\\{(e_{1},e_{2})\mid\mathcal{T}\models{r}\sqsubseteq{p}\\}\\\
&&\phantom{{{p}}^{\mathcal{J}_{M_{0}}}}\cup\\{(e_{2},e_{1})\mid\mathcal{T}\models{r^{-}}\sqsubseteq{p}\\}\end{array}$

Its specification is $S_{M_{2}}=\\{(p,\widehat{p},\tau_{2}^{-1}\circ
h|_{\Delta^{\mathcal{I}_{\mathsf{base}}}\cup\\{e_{1}^{\prime},e_{2}^{\prime}\\}})\mid
p\in q,\widehat{p}\subseteq p,h:\widehat{p}\rightarrow\mathcal{I}\text{ is a
homomorphism}\\}$. We now add $M_{2}\in\mathcal{M}$, and if $\tau_{M_{2}}$ is
not already defined, then we set $\tau_{M_{2}}:=\tau_{2}$.

Recalling that $\mathcal{I}$ is a model of $\mathcal{K}$ it is then
straightforward to verify that $M_{2}$, from the induction case, is a mosaic
satisfying all conditions to succeed to $M_{1}$ for $e$ and
$A\sqsubseteq\exists r.B$, and that $\tau_{2}$ (thus $\tau_{M_{2}}$) is a
homomorphism. These properties are verified by the next two lemmas.

######  Lemma 16.

Each $M\in\mathcal{M}$ is a well-defined mosaic. Furthermore, $\tau_{M}$ is a
homomorphism from $\mathcal{J}_{M}$ to $\mathcal{I}$.

###### Proof.

The base case consisting of verifying that $M_{0}$ is a mosaic is trivial, and
$\mathsf{Id}_{\mathcal{J}_{M_{0}}\rightarrow\mathcal{I}}$ is indeed a
homomorphism.

We move to the induction case. Consider $M_{2}$ and $\tau_{2}$ as obtained
from some $M_{1}\in\mathcal{M}$ and $e_{1}\in(A\sqcap\lnot\exists
r.B)^{\mathcal{J}_{M_{1}}}$ with $A\sqsubseteq\exists r.B\in\mathcal{T}$. By
induction hypothesis, $M_{1}$ is a mosaic and $\tau_{1}:=\tau_{M_{1}}$ is a
homomorphism from $\mathcal{J}_{M_{1}}$ to $\mathcal{I}$.

We first verify that $\tau_{2}$ is a homomorphism:

  * •

Let $u\in{{A}}^{\mathcal{J}_{M_{2}}}$. If $u\in{{A}}^{\mathcal{J}_{M_{0}}}$,
then in particular $u\in\Delta^{\mathcal{I}_{\mathsf{base}}}$ hence
$\tau_{2}(u)=u\in{{A}}^{\mathcal{J}_{M_{0}}}\subseteq{{A}}^{\mathcal{I}}$.
Otherwise, $u=e_{k}$ for $k=1$ or $k=2$ with
$e_{k}^{\prime}\in{{A}}^{\mathcal{I}}$. In that case, notice
$\tau_{2}(u)=e_{k}^{\prime}$ which concludes.

  * •

Let $(u,v)\in{{p}}^{\mathcal{J}_{M_{2}}}$. If
$(u,v)\in{{p}}^{\mathcal{J}_{M_{0}}}$, then in particular
$u,v\in\Delta^{\mathcal{I}_{\mathsf{base}}}$, hence
$(\tau_{2}(u),\tau_{2}(v))=(u,v)\in{{p}}^{\mathcal{J}_{M_{0}}}\subseteq{{p}}^{\mathcal{I}}$.
Otherwise, if $(u,v)=(e_{1},e_{2})$ with
$\mathcal{T}\models{r}\sqsubseteq{p}$, then notice that
$(\tau_{2}(u),\tau_{2}(v))=(e_{1}^{\prime},e_{2}^{\prime})$. Since
$e_{2}^{\prime}$ is the successor of $e_{1}^{\prime}$ for ${{r}}.{{B}}$ in
$\mathcal{I}$, and $\mathcal{I}$ models $\mathcal{T}$, we obtain
$(e_{1}^{\prime},e_{2}^{\prime})\in{{p}}^{\mathcal{I}}$ as desired. Otherwise
we have $(u,v)=(e_{2},e_{1})$ with $\mathcal{T}\models{r^{-}}\sqsubseteq{p}$,
then notice that $(\tau_{2}(u),\tau_{2}(v))=(e_{1}^{\prime},e_{1}^{\prime})$.
Since $e_{2}^{\prime}$ is the successor of $e_{1}^{\prime}$ for ${{r}}.{{B}}$
in $\mathcal{I}$, and $\mathcal{I}$ models $\mathcal{T}$, we have
$(e_{2}^{\prime},e_{1}^{\prime})\in{{p}}^{\mathcal{I}}$ as desired.

We now verify that $M_{2}$ is a well-defined mosaic.

  * •

Regarding $\mathcal{J}_{M_{2}}$:

    1. 1.

By definition, we have $\Delta^{\mathcal{I}_{{\sf
base}}}\subseteq\Delta^{\mathcal{J}_{M_{2}}}\subseteq\Delta^{\mathcal{I}_{{\sf
base}}}\uplus\\{e^{*}_{1},e^{*}_{2}\\}$ as desired;

    2. 2.

Also by definition, we have $\mathcal{J}_{M_{2}}|_{\Delta^{\mathcal{I}_{{\sf
base}}}}=\mathcal{I}_{\mathsf{base}}$;

    3. 3.

From interpretations of concepts being inherited from $\mathcal{I}$ that
satisfies Condition (b), it follows that indeed ${\sf
tp}_{\mathcal{J}_{M_{2}}}(e_{i}^{*})\in T_{\mathsf{\overline{core}}}$ if
$e_{i}^{*}\in\Delta^{\mathcal{J}_{M_{2}}}$, for $i\in\\{1,2\\}$;

    4. 4.

From $\mathcal{I}$, being a model of $\mathcal{K}$, it follows that
$\mathcal{J}_{M_{2}}$ satisfies in particular all $\exists r.A\sqsubseteq
B\in\mathcal{T}$ and all $r\sqsubseteq s\in\mathcal{T}$.

  * •

Regarding $S_{M_{2}}$, it is the restriction of a saturated specification (up
to $\tau_{2}$, which essentially rename elements), and hence is also
saturated. From $\mathcal{I}$ satisfying Condition (c), we obtain that
$S_{M_{2}}$ doesn’t contain any complete triple. ∎

######  Lemma 17.

For all $M\in\mathcal{M}$, the mosaic $M$ is good in $\mathcal{M}$.

###### Proof.

Let $M_{1}\in\mathcal{M}$ and $e_{1}\in(A\sqcap\lnot\exists
r.B)^{\mathcal{J}_{M_{1}}}$ with $A\sqsubseteq\exists r.B\in\mathcal{T}$.
Consider $M_{2}$ as obtained from the induction case of Definition 4. We have
$M_{2}\in\mathcal{M}$ and verify the three additional conditions:

  1. 1.

Interpretations of concepts names being directly imported from $\mathcal{I}$,
we immediately have ${\sf tp}_{\mathcal{J}_{M_{1}}}(e_{1})={\sf
tp}_{\mathcal{J}_{M_{2}}}(e_{1})$;

  2. 2.

Since we set
$e_{2}^{\prime}:=\mathsf{succ}^{\mathcal{I}}_{{{r}}.{{B}}}(e_{1}^{\prime})$ in
the construction of $M_{2}$, it follows naturally that $e\in(\exists
r.B)^{\mathcal{J}_{M_{2}}}$;

  3. 3.

This is immediate as any partial homomorphism from either $S_{M_{1}}$ (resp.
$S_{M_{2}}$) is the restriction to $\Delta^{\mathcal{J}_{M_{1}}}$ (resp.
$\Delta^{\mathcal{J}_{M_{2}}}$) of a complete homomorphism to $\mathcal{I}$,
which can in turn be restricted to $\Delta^{\mathcal{J}_{M_{2}}}$ (resp.
$\Delta^{\mathcal{J}_{M_{1}}}$). In fact, this proves: if
$(p,\widehat{p},h)\in S_{M_{2}}$, then $(p,\widehat{p},h^{\prime})\in
S_{M_{1}}$ where $h^{\prime}$ is the restriction of $h$ to range
$\Delta^{\mathcal{I}_{{\sf base}}}\cup\\{e_{1}\\}$, but also “the converse”,
that is: if $(p,\widehat{p},h)\in S_{M_{1}}$, then
$(p,\widehat{p},h^{\prime})\in S_{M_{2}}$ where $h^{\prime}$ is the
restriction of $h$ to range $\Delta^{\mathcal{I}_{{\sf
base}}}\cup\\{e_{1}\\}$. ∎

See 2

###### Proof.

We give a polynomial time reduction from (Boolean) CQ evaluation on ${\cal
EL}$ KBs with closed concept names, which is 2Exp-hard (?). A _KB with closed
concept names_ takes the form $\mathcal{K}_{\Sigma}$ with $\mathcal{K}$ a KB
and $\Sigma\subseteq{\sf N_{C}}$ a set of closed concept names. We say that an
interpretation $\mathcal{I}$ _respects_ $\Sigma$ if for all $A\in\Sigma$,
$d\in A^{\mathcal{I}}$ implies $A(d)\in\mathcal{A}$. Moreover, $\mathcal{I}$
is a _model_ of $\mathcal{K}_{\Sigma}$ if $\mathcal{I}$ is a model of
$\mathcal{K}$ and $\mathcal{I}$ respects $\Sigma$. Thus, the only instances of
a closed concept name are those that are explicitly asserted in the ABox. Now
the problem proved to be 2Exp-hard in (?) is: given a KB with closed concept
names $\mathcal{K}_{\Sigma}$ and a Boolean CQ $q$, decide whether
$\mathcal{K}_{\Sigma}\models q$. We remark that the formalism in (?) also
admits closed role names, but these are not used in the hardness proof.

Let $\mathcal{K}_{\Sigma}$ be an ${\cal EL}$ KB with closed concept names,
$\mathcal{K}=(\mathcal{T},\mathcal{A})$, and $q$ a Boolean CQ. Specializing to
${\cal EL}$ the normal form presented in Section 2, we assume every concept
inclusion in $\mathcal{T}$ to have one of the following shapes:

$\begin{array}[]{r@{\qquad}l<EMAIL_ADDRESS>
where ${{A,A_{1},A_{2},B}}$ range over ${\sf N_{C}}$ and $r$ ranges over ${\sf
N_{R}}$. We construct a circumscribed ${\cal EL}$ KB ${\sf Circ}_{\sf
CP}(\mathcal{K}^{\prime})$ with
$\mathcal{K}^{\prime}=(\mathcal{T}^{\prime},\mathcal{A}^{\prime})$, and a CQ
$q^{\prime}$ such that $\mathcal{K}_{\Sigma}\models q$ iff ${\sf Circ}_{\sf
CP}(\mathcal{K}^{\prime})\models q^{\prime}$.

A natural first attempt is to use use $\mathcal{K}^{\prime}=\mathcal{K}$ and
$q^{\prime}=q$, and to minimize the concept names in $\Sigma$ while letting
all other concept names vary. Apart from using more than a single minimized
concept name, this does not work since the extension of closed concept names
may be too large. As a simple example, consider the empty ABox and the TBox
$\top\sqsubseteq\exists r.A$ with $A\in\Sigma$. This KB is unsatisfiable when
$A$ is closed, but satisfiable when $A$ is minimized. We thus use a more
refined approach.

Let ${\sf CP}$ be the circumscription pattern that minimizes the fresh concept
name $M$ and lets all other symbols vary. In what follows, we assemble
$\mathcal{T}^{\prime}$ and $\mathcal{A}^{\prime}$ and define $q^{\prime}$. For
$\mathcal{A}^{\prime}$, we start from $\mathcal{A}$ and extend with additional
assertions. $\mathcal{T}^{\prime}$ contains the CIs from $\mathcal{T}$ in a
modified form, as well as additional CIs, see below for details.

We start with connecting the concept names in $\Sigma$ to the minimized
concept name $M$:

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

Much of the reduction is concerned with preventing non-asserted instances $d$
of closed concept names $A\in\Sigma$, that is, elements $d$ that satisfy $A$
but are not an individual from ${\sf ind}(\mathcal{A})$ such that
$A(d)\in\mathcal{A}$. There are three cases to be distinguished.

We first consider the case that $d=a\in{\sf ind}(\mathcal{A})$, but
$A(d)\notin\mathcal{A}$. We mark such $a$ with a fresh concept name $L$:

$\displaystyle\overline{A}(a)$ $\displaystyle\quad\text{for all }a\in{\sf
ind}(\mathcal{A})\text{ with }A(a)\not\in\mathcal{A}$ (2) $\displaystyle
A\sqcap\overline{A}\sqsubseteq L$ $\displaystyle\quad\text{for all
}A\in\Sigma.$ (3)

where $\overline{A}$ is a fresh concept name for each $A\in\Sigma$.

We next want to achieve that any model $\mathcal{I}$ that satisfies $a\in
L^{\mathcal{I}}$ for some ABox individual $a$ also satisfies
$\mathcal{I}\models q$ and is thus ruled out as a countermodel against the
query being entailed. To this end, we add a copy of $q$ to
$\mathcal{A}^{\prime}$:

$\displaystyle A(x)$ $\displaystyle\quad\text{for all }A(x)\in\varphi$ (4)
$\displaystyle r(x,y)$ $\displaystyle\quad\text{for all }r(x,y)\in\varphi$ (5)

assuming w.l.o.g. that ${\sf var}(q)\cap{\sf ind}(\mathcal{A})=\emptyset$.

We want the copy of $q$ in $\mathcal{A}^{\prime}$ to only become ‘active’ when
the concept name $L$ is made true at some individual from ${\sf