=Paper=
{{Paper
|id=Vol-3263/paper-15
|storemode=property
|title=More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions
|pdfUrl=https://ceur-ws.org/Vol-3263/paper-15.pdf
|volume=Vol-3263
|authors=Jean Christoph Jung,Andrea Mazzullo,Frank Wolter
|dblpUrl=https://dblp.org/rec/conf/dlog/JungMW22
}}
==More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions==
https://ceur-ws.org/Vol-3263/paper-15.pdf
More on Interpolants and Explicit Definitions for
Description Logics with Nominals and/or Role
Inclusions
Jean Christoph Jung1 , Andrea Mazzullo2 and Frank Wolter3
1
University of Hildesheim
2
Free University of Bozen-Bolzano
3
University of Liverpool
Abstract
It is known that the problems of deciding the existence of Craig interpolants and of explicit definitions
of concepts are both 2ExpTime-complete for standard description logics with nominals and/or role
inclusions. These complexity results depend on the presence of an ontology. In this article, we first
consider the case without ontologies (or, in the case of role inclusions, ontologies only containing
role inclusions) and show that both the existence of Craig interpolants and of explicit definitions of
concepts become coNExpTime-complete for DLs such as ๐โ๐๐ช and ๐โ๐โ. Secondly, we make a few
observations regarding the size and computation of interpolants and explicit definitions.
Keywords
Craig interpolants, Explicit definitions, Beth definability property, Description logics
1. Introduction
Craig interpolants and explicit definitions have many potential applications in ontology engi-
neering and ontology-based information systems. Examples include the extraction of equivalent
acyclic TBoxes from ontologies [1, 2], the computation of referring expressions (or definite
descriptions) for individuals [3], concept separability and learning [4, 5], the equivalent rewrit-
ing of ontology-mediated queries into concepts or formulas [6, 7, 8, 9, 10], the construction
of alignments between ontologies [11], and the decomposition of ontologies [12]. For logics
enjoying the Craig interpolation property (CIP) the existence of a Craig interpolant follows from
the validity of the defining subsumption and for logics enjoying the projective Beth definability
property (PBDP) the existence of an explicit definition of a concept follows from its implicit
definability. For such logics, deciding the existence of a Craig interpolant or an explicit definition
of a concept are therefore not harder than subsumption and can be decided in ExpTime for DLs
such as ๐โ๐, ๐โ๐โ, ๐โ๐๐ฌโ (which enjoy the CIP/PBDP [2]) if an ontology is present, and in
PSpace without ontology.
This paper is a part of a research program with the goal of understanding Craig interpolants
and explicit definitions for logics that do not enjoy the CIP/PBDP [13, 14]. The two most basic
DL 2022: 35th International Workshop on Description Logics, August 7โ10, 2022, Haifa, Israel
$ jungj@uni-hildesheim.de (J. C. Jung); mazzullo@inf.unibz.it (A. Mazzullo); wolter@liverpool.ac.uk (F. Wolter)
ยฉ 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
constructors that lead to DLs without the CIP and PBDP are nominals and role inclusions.
In fact, it is known that the complexity of deciding the existence of Craig interpolants and
explicit definitions are both 2ExpTime complete for standard DLs containing ๐โ๐๐ช or ๐โ๐โ
and contained in the extension of ๐โ๐โโ๐ช with the universal role, in the presence of an
ontology [15]. The case without ontology remained open. Note that nothing interesting happens
for DLs containing the universal role or both nominals and inverse roles as it is known that then
the ontology can be โinternalizedโ, and thus there is no difference between the case with and
without ontology. For DLs such as ๐โ๐๐ช, ๐โ๐โ, and ๐โ๐โโ, however, this is not the case.
In fact, it is known that subsumption checking becomes PSpace-complete without ontology
while it is ExpTime-complete with ontology. In the first part of this paper we investigate the
complexity of deciding the existence of Craig interpolants and explicit definitions without
ontologies for these DLs and show that it becomes coNExpTime-complete. Hence we observe
again a significant increase in complexity compared to subsumption checking. Note that for
๐โ๐โ and ๐โ๐โโ we assume an ontology containing role inclusions only as otherwise they
cannot be introduced and are not relevant.
In practice, of course, one is interested in the actual interpolants or the explicit definition.
Unfortunately, the decision procedures for the existence problems provided in this paper and
in [15] are non-constructive in the sense that they do not return an interpolant (an explicit
definition) in case it exists. To address this problem, we (slightly) modify the decision procedure
from [15] and show how to read off interpolants / explicit definitions from a run of the procedure,
at least for DLs with role inclusions. In doing so, we take inspiration from a recent note on a
type elimination based computation of interpolants in modal logic [16] which was originally
provided for the guarded fragment [17].
For a discusson of further related work on interpolation, Beth definability, interpolant exis-
tence, and explicit definition existence we refer the reader to [13, 15]. Detailed proofs for this
article are provided in the full version [18].
2. Preliminaries
We first introduce standard DL definitions and notation [19]. Let NC , NR , and NI be mutually
disjoint and countably infinite sets of concept, role, and individual names. A role is a role name ๐
or an inverse role ๐ โ , with ๐ a role name and (๐ โ )โ = ๐ . We use ๐ข to denote the universal role.
A nominal takes the form {๐}, with ๐ โ NI . An ๐โ๐โ๐ช๐ข -concept is defined by the syntax rule
๐ถ, ๐ท ::= โค | ๐ด | {๐} | ยฌ๐ถ | ๐ถ โ ๐ท | โ๐.๐ถ
where ๐ โ NI , ๐ด โ NC , and ๐ is a role. We use ๐ถ โ ๐ท as abbreviation for ยฌ(ยฌ๐ถ โ ยฌ๐ท), ๐ถ โ ๐ท
for ยฌ๐ถ โ ๐ท, and โ๐.๐ถ for ยฌโ๐.ยฌ๐ถ. We also consider the following fragments of ๐โ๐โ๐ช๐ข :
๐โ๐โ๐ช, obtained by dropping the universal role; ๐โ๐๐ช๐ข , obtained by dropping inverse roles;
๐โ๐๐ช, obtained from ๐โ๐๐ช๐ข by dropping the universal role; and ๐โ๐, obtained from ๐โ๐๐ช
by dropping nominals. If โ is any of the DLs defined above, then an โ-concept inclusion (โ-CI)
takes the form ๐ถ โ ๐ท, with ๐ถ and ๐ท โ-concepts. An โ-ontology is a finite set of โ-CIs. We
also consider DLs with role inclusions (RIs), expressions of the form ๐ โ ๐ , where ๐ and ๐ are
roles. As usual, the addition of RIs is indicated by adding the letter โ to the name of the DL,
where inverse roles occur in RIs only if the DL admits inverse roles. Thus, for example, ๐โ๐โ-
ontologies are finite sets of ๐โ๐-CIs and RIs not using inverse roles and ๐โ๐โโ๐ช๐ข -ontologies
are finite sets of ๐โ๐โ๐ช๐ข -CIs and RIs. In the following, we use DLnr to denote the set of DLs
๐โ๐๐ช, ๐โ๐โ๐ช, ๐โ๐โ, ๐โ๐โ๐ช, ๐โ๐โโ๐ช, and their extensions with the universal role.
To simplify notation we do not drop the letter โ when speaking about the concepts and CIs
of a DL with RIs. Thus, for example, we sometimes use the expressions ๐โ๐โ๐ช-concept and
๐โ๐โ๐ช-CI to denote ๐โ๐๐ช-concepts and CIs, respectively.
The semantics is given in terms of interpretations โ = (ฮโ , ยทโ ), defined as usual [19]. An
interpretation โ satisfies an โ-CI ๐ถ โ ๐ท if ๐ถ โ โ ๐ทโ and an RI ๐ โ ๐ if ๐โ โ ๐ โ . We say
that โ is a model of an ontology ๐ช if it satisfies all inclusions in it. We say that an inclusion
๐ผ follows from an ontology ๐ช, in symbols ๐ช |= ๐ผ, if every model of ๐ช satisfies ๐ผ. We write
๐ช |= ๐ถ โก ๐ท if ๐ช |= ๐ถ โ ๐ท and ๐ช |= ๐ท โ ๐ถ. We write |= ๐ถ โ ๐ท if ๐ช |= ๐ถ โ ๐ท for the
empty ontology ๐ช. A concept ๐ถ is satisfiable w.r.t. an ontology ๐ช if there is a model โ of ๐ช
with ๐ถ โ ฬธ= โ
.
A signature ฮฃ is a set of symbols, i.e., concept, role, and individual names. As standard in the
literature, the universal role is not regarded as a symbol, but as a logical connective, and as such
it is not contained in any signature. We use sig(๐) to denote the set of symbols used in any
syntactic object ๐ such as a concept or an ontology. An โ(ฮฃ)-concept is an โ-concept ๐ถ with
sig(๐ถ) โ ฮฃ, and a ฮฃ-role is a role ๐ such that ๐ or ๐โ is in ฮฃ.
We require a model-theoretic characterization of when nodes are indistinguishable by โ(ฮฃ)-
concepts. A pair โ, ๐ with โ an interpretation and ๐ โ ฮโ is called a pointed interpretation. For
pointed interpretations โ, ๐ and ๐ฅ , ๐ and a signature ฮฃ, we write โ, ๐ โกโ,ฮฃ ๐ฅ , ๐ and say that
โ, ๐ and ๐ฅ , ๐ are โ(ฮฃ)-equivalent if ๐ โ ๐ถ โ iff ๐ โ ๐ถ ๐ฅ , for all โ(ฮฃ)-concepts ๐ถ. An โ(ฮฃ)-
bisimulation ๐ is a relation ๐ โ ฮโ ร ฮ๐ฅ satisfying the standard back-and-forth conditions
required by the constructors of โ, we refer the reader to [20, 21]. We write โ, ๐ โผโ,ฮฃ ๐ฅ , ๐ and
call โ, ๐ and ๐ฅ , ๐ โ(ฮฃ)-bisimilar if there exists an โ(ฮฃ)-bisimulation ๐ such that (๐, ๐) โ ๐.
Then the following holds for all ๐-saturated interpretations โ and ๐ฅ (for the โifโ-direction, the
๐-saturatedness condition can be dropped):1 โ, ๐ โกโ,ฮฃ ๐ฅ , ๐ if and only if โ, ๐ โผโ,ฮฃ ๐ฅ , ๐.
3. Basic Notions and Results
Let โ be a DL, let ๐ช1 , ๐ช2 be โ-ontologies, and let ๐ถ1 , ๐ถ2 be โ-concepts. We set sig(๐ช, ๐ถ) =
sig(๐ช) โช sig(๐ถ), for any ontology ๐ช and concept ๐ถ. Following [2], an โ-concept ๐ท is called
an โ-interpolant for ๐ถ1 โ ๐ถ2 under ๐ช1 โช ๐ช2 if: (๐) sig(๐ท) โ sig(๐ช1 , ๐ถ1 ) โฉ sig(๐ช2 , ๐ถ2 ); (๐๐)
๐ช1 โช ๐ช2 |= ๐ถ1 โ ๐ท; (๐๐๐) ๐ช1 โช ๐ช2 |= ๐ท โ ๐ถ2 . โ-interpolant existence is the problem to
decide the existence of an interpolant for ๐ถ1 โ ๐ถ2 under ๐ช1 โช ๐ช2 . In logics with the Craig
Interpolation Property (CIP) (such as, for instance, ๐โ๐ and ๐โ๐โ [2]) the existence of an
โ-interpolant for ๐ถ1 โ ๐ถ2 under ๐ช1 โช ๐ช2 is equivalent to the entailment ๐ช1 โช ๐ช2 |= ๐ถ1 โ ๐ถ2
and thus reduces to standard subsumption checking (which is, for instance, ExpTime-complete
for ๐โ๐ and ๐โ๐โ). This is not the case for the DLs considered here; in fact the following
increase in complexity by one exponential is shown in [15].
1
See [22] for the definition of ๐-saturated interpretations.
Theorem 1. Let โ โ DLnr . Then โ-interpolant existence is 2ExpTime-complete.
In this article we consider interpolant existence with either empty ontologies or ontologies
containing RIs only. In detail, ontology-free โ-interpolant existence is the problem to decide
โ-interpolant existence for empty ontologies. Note that for logics with the CIP ontology-free
interpolant existence reduces to checking |= ๐ถ1 โ ๐ถ2 and hence is PSpace-complete for DLs
such as ๐โ๐ and ๐โ๐โ. If โ admits RIs, then we consider ontology-free โ-interpolant existence
with RIs, the problem to decide โ-interpolant existence for ontologies containing RIs only. We
observe that DLs in DLnr do not enjoy the CIP, even without ontologies (ontologies containing
RIs only, respectively).
Example 1. Consider ๐ถ1 = {๐} โ โ๐.{๐} and ๐ถ2 = {๐} โ โ๐.{๐}. Then |= ๐ถ1 โ ๐ถ2 but there
does not exist any ๐โ๐๐ช-interpolant for ๐ถ1 โ ๐ถ2 (see Example 5 for a proof). An example using
RIs instead of nominals can be constructed from Example 3 below.
We next introduce explicit definitions. We call an โ(ฮฃ)-concept ๐ท an explicit โ(ฮฃ)-definition
of ๐ถ0 under an ontology ๐ช if ๐ช |= ๐ถ0 โก ๐ท. โ-explicit definition is the problem to decide
the existence of an โ(ฮฃ)-definition of an โ-concept under an โ-ontology. In logics with the
appropriate projective Beth Definability Property (PBDP) [2, 15] the existence of an explicit
โ(ฮฃ)-definition of a concept follows from its implicit definability according to which the
extension of the concept is determined by the extension of symbols in ฮฃ. The latter condition
can be decided using subsumption checking and is therefore ExpTime-complete for DLs with
the PBDP such as ๐โ๐ and ๐โ๐โ [2]. Similarly to the interpolant existence problem, this is
not the case for the DLs considered here and we have again an increase in complexity by one
exponential [15].
Theorem 2. Let โ โ DLnr . Then explicit definition existence is 2ExpTime-complete.
In this article we consider explicit definition existence without ontologies and ontologies
containing RIs only. If ๐ถ and ๐ถ0 are concepts and ฮฃ a signature, then we call ๐ท an explicit
โ(ฮฃ)-definition of ๐ถ0 under ๐ถ if |= ๐ถ โ (๐ถ0 โ ๐ท).
Remark 2. Explicit definitions under a concept ๐ถ can be regarded as a โlocalโ version of explicit
definitions under ontologies. If ๐ช is an ontology, then let ๐๐ be the concept stating that ๐ช is true
in all nodes reachable in at most ๐ steps. Then a concept ๐ท is an โ(ฮฃ)-definition of ๐ถ0 under ๐ช
iff there exists an ๐ โฅ 0 such that ๐ท is an โ(ฮฃ)-definition of ๐ถ0 under ๐๐ .
Then ontology-free โ-definition existence is the problem to decide for โ-concepts ๐ถ and ๐ถ0 ,
and a signature ฮฃ whether there exists an explicit โ(ฮฃ)-definition of ๐ถ0 under ๐ถ. If โ admits
RIs, then ontology-free โ-definition existence with RIs is the problem to decide for an ontology ๐ช
containing RIs only, โ-concepts ๐ถ and ๐ถ0 , and a signature ฮฃ whether there exists an explicit
โ(ฮฃ)-definition ๐ท of ๐ถ0 under ๐ช and ๐ถ, that is ๐ช |= ๐ถ โ (๐ถ0 โ ๐ท). For DLs with the PBDP
such as ๐โ๐ and ๐โ๐โ ontology-free โ-definition existence reduces to subsumption checking
without ontologies and is thus PSpace-complete. We next observe that the DLs in DLnr do not
enjoy the PBDP without ontologies (ontologies containing RIs only).
Example 3. Consider ๐ช = {๐ โ ๐1 , ๐ โ ๐2 } and let ๐ถ be the conjunction of (ยฌโ๐.โค โ โ๐1 .๐ด) โ
โ๐2 .ยฌ๐ด and (ยฌโ๐.โค โ โ๐1 .ยฌ๐ด) โ โ๐2 .๐ด. Let ฮฃ = {๐1 , ๐2 }. Then there does not exist an
explicit ๐โ๐(ฮฃ)-definition of โ๐.โค under ๐ช and ๐ถ (see Example 6 below for a proof). The concept
โ๐1 โฉ ๐2 .โค, however, is an explicit definition of โ๐.โค under ๐ช and ๐ถ in the extension of ๐โ๐
with role intersection (with semantics defined in the obvious way). As any concept with an explicit
definition in FO is implicitly definable, โ๐.โค is implicitly definable.
We conclude this section with a few observations on the relationship between the existence
problems introduced above. It has been observed in [15] already that โ-explicit definition
existence is polyomial time reducible to โ-interpolant existence. This also holds for the ontology-
free versions.
Lemma 3. Let โ โ DLnr . Then ontology-free โ-definition existence (with RIs) can be reduced in
polynomial time to ontology-free โ-interpolant existence (with RIs).
By applying a standard encoding of ontologies into concepts one can show that for DLs in
DLnr containing the universal role or both inverse roles and nominals dropping the ontology
does not affect the complexity of explicit definition existence.
Lemma 4. Let โ โ DLnr contain the universal role or both inverse roles and nominals. Then
โ-explicit definition existence can be reduced in polynomial time to ontology-free โ-definition
existence (with RIs if โ admits RIs).
We obtain the following complexity result as a consequence of Theorems 1-2 and Lemmas 3-4.
Theorem 5. Let โ โ DLnr contain the universal role or both inverse roles and nominals. Then
ontology-free interpolant existence (with RIs) and ontology-free explicit definition existence (with
RIs) are both 2ExpTime-complete.
4. Joint Consistency
The first main concern of the present paper is to study the computational complexity of the
ontology-free interpolant and explicit definition existence problems. We show the upper bound
for a generalization of interpolant existence. Generalized โ-interpolant existence is the problem
to decide for an โ ontology ๐ช, โ-concepts ๐ถ1 , ๐ถ2 and signature ฮฃ whether there exists an
โ(ฮฃ)-interpolant for ๐ถ1 โ ๐ถ2 under ๐ช, that is, an โ(ฮฃ)-concept ๐ท such that ๐ช |= ๐ถ1 โ ๐ท
and ๐ช |= ๐ท โ ๐ถ2 . The ontology-free version and the version with ontologies containing RIs
only are defined in the obvious way. Note that โ-interpolant existence is indeed a special case of
generalized โ-interpolant existence by setting ๐ช = ๐ช1 โช๐ช2 and ฮฃ = sig(๐ช1 , ๐ถ1 )โฉsig(๐ช2 , ๐ถ2 ).
As a preliminary step, we provide model-theoretic characterizations in terms of bisimulations
as captured in the following central notion.
Definition 4 (Joint consistency). Let โ โ DLnr , ๐ช be an โ-ontology, ๐ถ1 , ๐ถ2 be โ-concepts, and
ฮฃ โ sig(๐ช, ๐ถ1 , ๐ถ2 ) be a signature. Then ๐ถ1 , ๐ถ2 are called jointly consistent under ๐ช modulo
โ(ฮฃ)-bisimulations if there exist pointed models โ1 , ๐1 and โ2 , ๐2 such that โ๐ is a model of ๐ช,
๐๐ โ ๐ถ๐โ๐ , for ๐ = 1, 2, and โ1 , ๐1 โผโ,ฮฃ โ2 , ๐2 .
The associated decision problem, joint consistency modulo โ-bisimulations, is defined in the
expected way. The following result characterizes the existence of interpolants using joint
consistency modulo โ(ฮฃ)-bisimulations and is proved in [15].
Theorem 6. Let โ โ DLnr . Let ๐ช be an โ-ontology, ๐ถ1 , ๐ถ2 be โ-concepts, and ฮฃ โ
sig(๐ช, ๐ถ1 , ๐ถ2 ). Then the following conditions are equivalent:
1. there is no โ(ฮฃ)-interpolant for ๐ถ1 โ ๐ถ2 under ๐ช;
2. ๐ถ1 , ยฌ๐ถ2 are jointly consistent under ๐ช modulo โ(ฮฃ)-bisimulations.
Example 5. From Example 1, let ๐ถ1 = {๐} โ โ๐.{๐}, ๐ถ2 = {๐} โ โ๐.{๐}, ฮฃ = {๐}. Interpreta-
tions โ1 , โ2 below show that ๐ถ1 and ยฌ๐ถ2 are jointly consistent modulo ๐โ๐๐ช(ฮฃ)-bisimulations.
โผ๐โ๐๐ช,ฮฃ
๐
โ1 โ2
๐
๐
๐ ๐ โผ๐โ๐๐ช,ฮฃ ๐
๐ถ1 ยฌ๐ถ2 ๐ ๐
The existence of explicit definitions can be characterized as follows.
Theorem 7. Let โ โ DLnr . Let ๐ช be an โ-ontology, ๐ถ and ๐ถ0 โ-concepts, and ฮฃ โ sig(๐ช, ๐ถ) a
signature. Then the following conditions are equivalent:
1. there is no explicit โ(ฮฃ)-definition of ๐ถ0 under ๐ช and ๐ถ;
2. ๐ถ โ ๐ถ0 and ๐ถ โ ยฌ๐ถ0 are jointly consistent under ๐ช modulo โ(ฮฃ)-bisimulations.
Example 6. Consider ๐ช, ๐ถ, and ฮฃ from Example 3. The interpretations โ1 , โ2 depicted below show
that ๐ถ โ โ๐.โค and ๐ถ โ ยฌโ๐.โค are jointly consistent under ๐ช modulo ๐โ๐โ(ฮฃ)-bisimulations.
โผ๐โ๐โ,ฮฃ
๐ด โฒ
โ1 ๐1 ๐2 ๐2 โ2
๐, ๐1 , ๐2 โผ๐โ๐โ,ฮฃ ๐1 ๐2
๐1 ๐2
โผ๐โ๐โ,ฮฃ
๐ถ โ โ๐.โค ๐ถ โ ยฌโ๐.โค
5. Complexity
We formulate our main complexity result about the problem of deciding the existence of
interpolants and explicit definitions.
Theorem 8. Let โ โ DLnr not contain the universal role and not contain both inverse roles
and nominals simultaneously. Then ontology-free generalized โ-interpolant existence (with RIs),
ontology-free โ-interpolant existence (with RIs), and ontology-free โ-definition existence (with RIs)
are all coNExpTime-complete.
We show the upper bound for generalized โ-interpolant existence by proving that joint
consistency is in NExpTime (Theorem 6) and we show the lower bound by proving NExpTime-
hardness for the version of joint consistency formulated in Theorem 7 (with empty ontology or,
respectively, ontologies containing RIs only).
To show these results, we first require the following definitions. The depth of a concept ๐ถ is
the number of nestings of restrictions in ๐ถ. For instance, a concept name ๐ต has depth 0 and
โ๐.โ๐.๐ต has depth 2. Given an ontology ๐ช and concepts ๐ถ1 , ๐ถ2 , let ฮ = sub(๐ช, ๐ถ1 , ๐ถ2 ) denote
the closure under single negation of the set of subconcepts of concepts in ๐ช, ๐ถ1 , ๐ถ2 . A ฮ-type
๐ก is a subset of ฮ such that there exists an interpretation โ and ๐ โ ฮโ with ๐ก = tpฮ (โ, ๐),
where tpฮ (โ, ๐) = {๐ถ โ ฮ | ๐ โ ๐ถ โ } is the ฮ-type realized at ๐ in โ. For a signature
ฮฃ โ sig(๐ช, ๐ถ1 , ๐ถ2 ) and ๐ โ {1, 2}, the mosaic defined by ๐ โ ฮโ๐ in โ1 , โ2 is the pair
(๐1 (๐), ๐2 (๐)) such that ๐๐ (๐) = {tpฮ (โ๐ , ๐) | ๐ โ ฮโ๐ , โ๐ , ๐ โผโ,ฮฃ โ๐ , ๐}, for ๐ = 1, 2. We
say that a pair (๐1 , ๐2 ) of sets ๐1 , ๐2 of types is a mosaic defined by โ1 , โ2 if there exists
๐ โ ฮโ1 โช ฮโ2 such that (๐1, ๐2 ) = (๐1 (๐), ๐2 (๐)).
Example 7. From Example 5, consider ๐ถ1 , ๐ถ2 , as well as โ1 , โ2 . The set ฮ consists of the concepts
{๐}, โ๐.{๐}, {๐}, โ๐.{๐}, ๐ถ1 , ๐ถ2 , and negations thereof. We have that:
โข tpฮ (โ1 , ๐โ1 ) = {{๐}, โ๐.{๐}, ยฌ{๐}, ยฌโ๐.{๐}, ๐ถ1 , ๐ถ2 };
โข tpฮ (โ2 , ๐โ2 ) = {ยฌ{๐}, ยฌโ๐.{๐}, {๐}, ยฌโ๐.{๐}, ยฌ๐ถ1 , ยฌ๐ถ2 };
โข tpฮ (โ2 , ๐) = {ยฌ{๐}, ยฌโ๐.{๐}, ยฌ{๐}, ยฌโ๐.{๐}, ยฌ๐ถ1 , ๐ถ2 }.
The mosaic defined by ๐โ1 in โ1 , โ2 is (๐1 (๐โ1 ), ๐2 (๐โ1 )), where ๐1 (๐โ1 ) = {tpฮ (โ1 , ๐โ1 )} and
๐2 (๐โ1 ) = {tpฮ (โ2 , ๐โ2 ), tpฮ (โ2 , ๐)}.
A mosaic is nominal generated if some type in it contains a nominals. Consider ๐ =
(๐1 (๐), ๐2 (๐)) and ๐ = (๐1 (๐โฒ ), ๐2 (๐โฒ )) such that there exists a role name ๐ โ ฮฃ with
(๐, ๐โฒ ) โ ๐โ๐ , for some ๐ โ {1, 2}. Then define, for every role name ๐ and ๐ โ {1, 2}, re-
๐ ,๐ ๐ ,๐
lations ๐
๐,๐ โ ๐๐ (๐) ร ๐๐ (๐โฒ ) by setting (๐ก, ๐กโฒ ) โ ๐
๐,๐ if there exist ๐, ๐โฒ realizing ๐ก and ๐กโฒ ,
respectively, with (๐1 (๐), ๐2 (๐)) = ๐ and (๐1 (๐โฒ ), ๐2 (๐โฒ )) = ๐, such that (๐, ๐โฒ ) โ ๐ โ๐ .
The upper bound follows from the following exponential size model property result.
Lemma 9. Let โ โ DLnr not contain the universal role and not contain both inverse roles and
nominals simultaneously. Let ๐ช be a set of RIs , ๐ถ1 , ๐ถ2 โ-concepts, and ฮฃ a signature. If ๐ถ1
and ยฌ๐ถ2 are jointly consistent under ๐ช modulo โ(ฮฃ)-bisimulations, then there exist models of
exponential size witnessing this; in more detail, there exist pointed models โ, ๐ and ๐ฅ , ๐ of ๐ช of at
most exponential size such that ๐ โ ๐ถ1โ , ๐ ฬธโ ๐ถ2๐ฅ , and โ, ๐ โผโ,ฮฃ ๐ฅ , ๐.
Proof. Assume that ๐ถ1 and ยฌ๐ถ2 are jointly consistent under ๐ช modulo โ(ฮฃ)-bisimulations.
By definition, there exist pointed models โ1 , ๐1 and โ2 , ๐2 of ๐ช such that ๐1 โ ๐ถ1โ1 , ๐2 ฬธโ ๐ถ2โ2 ,
and โ1 , ๐1 โผโ,ฮฃ โ2 , ๐2 . Let ๐ be the maximum depth of ๐ถ1 , ๐ถ2 .
We consider the case involving nominals and without inverse roles. We construct exponential
size ๐ฅ1 , ๐ฅ2 with the same properties of โ1 , โ2 above. Let โฌ be some minimal set of mosaics
defined by โ1 , โ2 such that: (๐) all nominal generated mosaics are in โฌ; (๐๐) for every type ๐ก
realized in โ๐ there exists (๐1 , ๐2 ) โ โฌ with ๐ก โ ๐๐ ; (๐๐๐) (๐1 (๐1 ), ๐2 (๐1 )) โ โฌ. Observe that the
size of โฌ is at most exponential in the size of ๐ช, ๐ถ1 , ๐ถ2 . Now select, for any mosaic ๐ = (๐1 , ๐2 )
defined by โ1 , โ2 and any โ๐ .๐ถ โ ๐ก โ ๐๐ such that there exists ๐ โ ฮฃ with ๐ช |= ๐ โ ๐, a mosaic
๐ ,๐
๐ = (๐1โฒ , ๐2โฒ ) such that (๐ก, ๐กโฒ ) โ ๐
๐,๐ and ๐ถ โ ๐กโฒ , and denote the resulting set by ๐ฎ(๐). Form the
set ๐ฏ of sequences ๐ = ๐0 ยท ยท ยท ๐๐ = (๐10 , ๐20 ) ยท ยท ยท (๐1๐ , ๐2๐ ), with ๐ โค ๐, ๐0 โ โฌ and ๐๐+1 โ ๐ฎ(๐๐ )
for ๐ < ๐. Let tail(๐) = ๐๐ and tail๐ (๐) = ๐๐๐ . We next define the domain of ๐ฅ1 and ๐ฅ2 as
ฮ๐ฅ๐ = {(๐ก, ๐) | ๐ก โ tail๐ (๐), ๐ โ โฌ} โช {(๐ก, ๐) | ๐ โ ๐ฏ , ๐ก โ tail๐ (๐), |๐| > 1, ๐ก has no nominal}.
We define interpretations ๐ฅ1 , ๐ฅ2 in the expected way. It can be shown that they are as required.
โข For any individual name ๐ and (๐1 , ๐2 ) โ โฌ with {๐} โ ๐ก โ ๐๐ , we set ๐๐ฅ๐ = (๐ก, (๐1 , ๐2 )).
โข For any concept name ๐ด, (๐ก, ๐) โ ๐ด๐ฅ๐ iff ๐ด โ ๐ก.
โข Let ๐ be a role name. Then, we let for ๐๐ โ ๐ฏ :
๐,๐
โ ((๐ก, ๐), (๐กโฒ , ๐๐)) โ ๐๐ฅ๐ if (๐ก, ๐กโฒ ) โ ๐
tail(๐),๐ and ๐กโฒ contains no nominal;
๐,๐
โ ((๐ก, ๐), (๐กโฒ , ๐)) โ ๐๐ฅ๐ if (๐ก, ๐กโฒ ) โ ๐
tail(๐),๐ and ๐กโฒ contains a nominal.
Next assume that tail(๐) = (๐1 , ๐2 ) and ๐ has length ๐. If tail(๐ โฒ ) = (๐1 , ๐2 ) for
some |๐ โฒ | < ๐, then choose as ๐-successors of any node of the form (๐ก, ๐) exactly the
๐-successors of (๐ก, ๐ โฒ ) defined above. If no such ๐ โฒ exists, then all nodes of the form
(๐ก, tail(๐)) have distance exactly ๐ from the roots (since no nominal occurs in any type in
any mosaic in ๐) and no successors are added.
It remains to consider existential restrictions โ๐.๐ถ for the role names ๐ not entailing any
role name in ฮฃ. If ๐ โ ๐ฏ , โ๐.๐ถ โ ๐ก โ ๐๐ with tail๐ (๐) = ๐๐ and ๐ช ฬธ|= ๐ โ ๐ for any ๐ โ ฮฃ,
we add ((๐ก, ๐), (๐กโฒ , ๐)) to ๐๐ฅ๐ (and all ๐ ๐ฅ๐ with ๐ช |= ๐ โ ๐ ) for some ๐ = (๐1โฒ , ๐2โฒ ) โ โฌ
and ๐กโฒ โ ๐๐โฒ with ๐ถ โ ๐กโฒ such that there are ๐, ๐โฒ realizing ๐ก, ๐กโฒ in โ๐ and (๐, ๐โฒ ) โ ๐โ๐ .
A similar construction can be used for the case with inverse roles, but without nominals. โ
The following example illustrates the construction of ๐ฅ1 , ๐ฅ2 from the proof above, in the case
with nominals and without inverse roles, using the interpretations โ1 , โ2 from Example 5.
Example 8. Let ๐ก0 = tpฮ (โ1 , ๐โ1 ), ๐ก1 = tpฮ (โ2 , ๐โ2 ), ๐ก2 = tpฮ (โ2 , ๐). We ignore the types
realized by ๐โ1 in โ1 and by ๐โ2 in โ2 as not relevant for understanding the construction. Then
only the mosaic ๐ = (๐1 , ๐2 ), with ๐1 = {๐ก0 }, ๐2 = {๐ก1 , ๐ก2 }, remains. ๐ฅ1 , ๐ฅ2 are depicted below.
๐
๐ฅ1 ๐ ๐ ๐ฅ2
(๐ก2 , ๐) (๐ก2 , ๐)
๐ ๐
(๐ก0 , ๐) (๐ก1 , ๐) (๐ก2 , ๐)
For the lower bound, we show that it is NExpTime-hard to decide joint consistency of โ-
concepts ๐ถ โ ๐ถ0 and ๐ถ โ ยฌ๐ถ0 (under an ontology containing RIs) modulo โ(ฮฃ)-bisimulations
and then employ Theorem 7. The proof is via an encoding of an (exponential torus) tiling problem,
known to be NExpTime-complete.
6. The Computation Problem
Unfortunately, the algorithms for deciding the existence of interpolants do not immediately
give rise to a way of computing interpolants in case they exist. Intuitively, this is due to the fact
that compactness is used in the proof of the model-theoretic characterization in Theorem 6. In
this section, we address the computation problem for DLs that do not contain nominals.
Theorem 10. Let โ be a DL in DLnr that does not contain nominals, and let ๐ช be an โ-ontology,
๐ถ1 , ๐ถ2 be โ-concepts, and ฮฃ be a signature. Then, if there is an โ(ฮฃ)-interpolant for ๐ถ1 โ ๐ถ2
๐(๐)
under ๐ช, we can compute the DAG representation of an โ(ฮฃ)-interpolant in time 22 where ๐ is
a polynomial and ๐ = ||๐ช|| + ||๐ถ1 || + ||๐ถ2 ||.
Note that this implies that the DAG representation is also of double exponential size, and
that a formula representation of the interpolant can be computed in triple exponential time.
Moreover, this also allows us to compute explicit definitions since, given ๐ช, ๐ถ, and ฮฃ, any
โ(ฮฃ)-interpolant for ๐ถฮฃ โ ๐ถ under ๐ช โช ๐ชฮฃ is an explicit โ(ฮฃ)-definition of ๐ถ under ๐ช, where
๐ชฮฃ and ๐ถฮฃ are obtained from ๐ช and ๐ถ by replacing all symbols not in ฮฃ by fresh symbols.
Let โ, ๐ช, ๐ถ1 , ๐ถ2 , and ฮฃ be as in Theorem 10. The computation of the โ(ฮฃ)-interpolant (if
it exists) is based on a mosaic elimination procedure for deciding joint consistency, which is a
simplified variant of a procedure that was presented in [15] and which decides a slightly more
general variant of joint consistency. As in Section 5, a mosaic is a pair (๐1 , ๐2 ) with ๐1 , ๐2 sets
of ฮ-types, where ฮ = sub(๐ช, ๐ถ1 , ๐ถ2 ). We denote with Tp(ฮ) the set of all ฮ-types. The aim
of the mosaic elimination procedure is to determine all pairs (๐1 , ๐2 ) โ 2Tp(ฮ) ร 2Tp(ฮ) such
that all ๐ก โ ๐1 โช ๐2 can be realized in mutually โ(ฮฃ)-bisimilar elements of models of ๐ช. In
order to formulate the elimination conditions, we need some preliminary notions. Throughout
the rest of the section, we treat the universal role ๐ข as a role name contained in ฮฃ, in case โ
allows the universal role. Note that ๐ขโ is equivalent to ๐ข, and that ๐ช |= ๐ โ ๐ข, for every role ๐.
Let ๐ก1 , ๐ก2 be ฮ-types. We call ๐ก1 , ๐ก2 ๐ข-equivalent if for every โ๐ข.๐ถ โ ฮ, we have โ๐ข.๐ถ โ ๐ก1
iff โ๐ข.๐ถ โ ๐ก2 . This condition is trivial if โ does not use allow the universal role. For a role
๐, we call ๐ก1 , ๐ก2 ๐-coherent for ๐ช, in symbols ๐ก1 โ๐,๐ช ๐ก2 , if ๐ก1 , ๐ก2 are ๐ข-equivalent and the
following conditions hold for all roles ๐ with ๐ช |= ๐ โ ๐ : (1) if ยฌโ๐ .๐ถ โ ๐ก1 , then ๐ถ ฬธโ ๐ก2 and
(2) if ยฌโ๐ โ .๐ถ โ ๐ก2 , then ๐ถ ฬธโ ๐ก1 . Note that ๐ก โ๐,๐ช ๐กโฒ iff ๐กโฒ โ๐โ ,๐ช ๐ก. We lift the definition of
๐-coherence from types to mosaics (๐1 , ๐2 ), (๐1โฒ , ๐2โฒ ). We call (๐1 , ๐2 ), (๐1โฒ , ๐2โฒ ) ๐-coherent, in
symbols (๐1 , ๐2 ) โ๐ (๐1โฒ , ๐2โฒ ), if for ๐ = 1, 2, (i) for every ๐ก โ ๐๐ there exists a ๐กโฒ โ ๐๐โฒ such that
๐ก โ๐,๐ช ๐กโฒ , and (ii) if โ allows for inverse roles, then for every ๐กโฒ โ ๐๐โฒ , there is a ๐ก โ ๐๐ such that
๐ก โ๐,๐ช ๐กโฒ . Note that (๐1 , ๐2 ) โ๐ (๐1โฒ , ๐2โฒ ) iff (๐1โฒ , ๐2โฒ ) โ๐โ (๐1 , ๐2 ) if โ allows for inverses.
Let ๐ฎ โ 2Tp(ฮ) ร2Tp(ฮ) . We call (๐1 , ๐2 ) โ ๐ฎ bad if it violates one of the following conditions.
1. ฮฃ-concept name coherence: ๐ด โ ๐ก iff ๐ด โ ๐กโฒ , for every concept name ๐ด โ ฮฃ and any
๐ก, ๐กโฒ โ ๐1 โช ๐2 ;
2. Existential saturation: for ๐ = 1, 2 and โ๐.๐ถ โ ๐ก โ ๐๐ , there exists (๐1โฒ , ๐2โฒ ) โ ๐ฎ such that
(1) there exists ๐กโฒ โ ๐๐โฒ with ๐ถ โ ๐กโฒ and ๐ก โ๐,๐ช ๐กโฒ and (2) if ๐ช |= ๐ โ ๐ for a ฮฃ-role ๐ ,
then (๐1 , ๐2 ) โ๐ (๐1โฒ , ๐2โฒ ).
The mosaic elimination procedure is now as follows. We start with the set ๐ฎ0 of all mosaics
(๐1 , ๐2 ) โ 2Tp(ฮ) ร 2Tp(ฮ) such that, for ๐ = 1, 2, ๐๐ contains only types that are realizable in
some model of ๐ช. Then obtain, for ๐ โฅ 0, ๐ฎ๐+1 from ๐ฎ๐ by eliminating all mosaics (๐1 , ๐2 ) that
are bad in ๐ฎ๐ . Let ๐ฎ * be where the sequence stabilizes. This elimination procedure decides joint
consistency (and thus interpolant existence via Theorem 6) since the following are equivalent:
(A) ๐ถ1 , ยฌ๐ถ2 are jointly consistent under ๐ช modulo โ(ฮฃ)-bisimulations;
(B) there exists (๐1 , ๐2 ) โ ๐ฎ * and ฮ-types ๐ก1 โ ๐1 , ๐ก2 โ ๐2 with ๐ถ1 โ ๐ก1 and ยฌ๐ถ2 โ ๐ก2 .
We will show how to read off interpolants from the run of the elimination procedure, but we
need one more notion. For a set ๐ of ฮ-types, an interpretation โ, and a family ๐๐ก , ๐ก โ ๐ of
domain elements of โ, we say that โ and ๐๐ก , ๐ก โ ๐ jointly realize ๐ modulo โ(ฮฃ)-bisimulations
if, for all ๐ก, ๐กโฒ โ ๐ , tpฮ (โ, ๐๐ก ) = ๐ก and โ, ๐๐ก โผโ,ฮฃ โ, ๐๐กโฒ . The elimination procedure decides
joint realizability since ๐ is jointly realizable modulo โ(ฮฃ)-bisimulations iff a mosaic (๐, โ
)
survives elimination. In what follows, let Real denote the set of all sets of types ๐ which are
jointly realizable modulo โ(ฮฃ)-bisimulations.
Lemma 11. Let ๐1 , ๐2 โ Real. If (๐1 , ๐2 ) is eliminated in the elimination procedure, then we can
compute an โ(ฮฃ)-concept ๐ผ๐1 ,๐2 such that:
1. for all models โ of ๐ช and elements ๐๐ก , ๐ก โ ๐1 that realize ๐1 modulo โ(ฮฃ)-bisimulations,
๐๐ก โ ๐ผ๐โ1 ,๐2 for some (equivalently: all) ๐ก โ ๐1 ;
2. for all models โ of ๐ช and elements ๐๐ก , ๐ก โ ๐2 that realize ๐2 modulo โ(ฮฃ)-bisimulations,
/ ๐ผ๐โ1 ,๐2 for some (equivalently: all) ๐ก โ ๐2 .
๐๐ก โ
The concepts ๐ผ๐1 ,๐2 are computed inductively in the order in which the (๐1 , ๐2 ) got eliminated
in the elimination procedure. We distinguish cases why (๐1 , ๐2 ) got eliminated.
Suppose first that (๐1 , ๐2 ) was eliminated because of (failing) ฮฃ-concept name coherence.
Since ๐1 , ๐2 are both jointly realizable, there are two cases:
(a) There is an ๐ด โ ฮฃ with ๐ด โ ๐ก for all ๐ก โ ๐1 , but ๐ด โ
/ ๐ก, for all ๐ก โ ๐2 . Then ๐ผ๐1 ,๐2 = ๐ด.
(b) There is an ๐ด โ ฮฃ with ๐ด โ ๐ก for all ๐ก โ ๐2 , but ๐ด โ
/ ๐ก, for all ๐ก โ ๐1 . Then ๐ผ๐1 ,๐2 = ยฌ๐ด.
Now, suppose that (๐1 , ๐2 ) was eliminated due to (failing) existential saturation from ๐ฎ๐
during the elimination. Since ๐1 , ๐2 are both jointly realizable, there are two cases:
(a) There exist ๐ก โ ๐1 , โ๐.๐ถ โ ๐ก, and a ฮฃ-role ๐ with ๐ช |= ๐ โ ๐ , such that there is no
(๐1โฒ , ๐2โฒ ) โ ๐ฎ๐ such that (i) (๐1 , ๐2 ) โ๐ (๐1โฒ , ๐2โฒ ) and (ii) there is ๐กโฒ โ ๐1โฒ with ๐ถ โ ๐กโฒ and
๐ก โ๐,๐ช ๐กโฒ . Then, take
l
๐ผ๐1 ,๐2 = โ๐ .( โฒ
โ ๐ผ๐1โฒ ,๐2โฒ )
๐1 โReal, โฒ
๐1 โ๐ ๐1โฒ ,๐กโ๐,๐ช ๐กโฒ ,๐ถโ๐กโฒ โ๐1โฒ ๐2 โReal,
๐2 โ๐ ๐2โฒ
(b) There exist ๐ก โ ๐2 , โ๐.๐ถ โ ๐ก, and a ฮฃ-role ๐ with ๐ช |= ๐ โ ๐ , such that there is no
(๐1โฒ , ๐2โฒ ) โ ๐ฎ such that (i) (๐1 , ๐2 ) โ๐ (๐1โฒ , ๐2โฒ ) and (ii) there is ๐กโฒ โ ๐2โฒ with ๐ถ โ ๐กโฒ and
๐ก โ๐,๐ช ๐กโฒ . Then, take
l
๐ผ๐1 ,๐2 = โ๐ .( โฒ โ ๐ผ๐1โฒ ,๐2โฒ )
๐1 โReal,
๐1 โ๐ ๐1โฒ ๐2โฒ โReal,
๐2 โ๐ ๐2โฒ ,๐กโ๐,๐ช ๐กโฒ ,๐ถโ๐กโฒ โ๐2โฒ
We show in the long version that the ๐ผ๐1 ,๐2 are as required. Observe that we can represent
the ๐ผ๐1 ,๐2 in DAG shape by using a single node for every ๐ผ๐1 ,๐2 (plus some auxiliary nodes
connecting them). Overall, we obtain double exponentially many nodes in the DAG and the
DAG can be constructed in double exponential time (both in ๐(||๐ช|| + ||๐ถ1 || + ||๐ถ2 ||)).
Given Lemma 11 it is relatively straightforward to construct the desired interpolants.
Lemma 12. Suppose the result ๐ฎ * of the elimination procedure does not contain a pair (๐1 , ๐2 ) โ
Real ร Real such that ๐ถ1 โ ๐ก1 and ยฌ๐ถ2 โ ๐ก2 for some types ๐ก1 โ ๐1 and ๐ก2 โ ๐2 . Then,
l
๐ถ= โ ๐ผ๐1 ,๐2
๐1 โReal:
there is ๐ก1 โ ๐1 with ๐ถ1 โ ๐ก1 ๐2 โReal:
there is ๐ก2 โ ๐2 with ยฌ๐ถ2 โ ๐ก2
is an โ(ฮฃ)-interpolant for ๐ถ1 โ ๐ถ2 under ๐ช. Moreover, a DAG representation of ๐ถ can be
๐(๐)
computed in time 22 , for some polynomial ๐ and ๐ = ||๐ช|| + ||๐ถ1 || + ||๐ถ2 ||.
To conclude, we give an intuition as to why the proof of Theorem 10 cannot be easily adapted
to logics from DLnr that allow for nominals. Observe that in any two interpretations โ1 , โ2 ,
every nominal ๐ is realized (modulo bisimulation) in exactly one mosaic. Thus, for the mosaic
elimination procedure to work (in the sense of the equivalence between (A) and (B) above) one
has to โguessโ for every ๐ exactly one mosaic that describes ๐ [15]. Then, there is an interpolant
for ๐ถ1 โ ๐ถ2 under ๐ช iff the runs of the mosaic elimination procedure for all possible guesses
of the nominal mosaics in ๐ฎ0 lead to an ๐ฎ * which does not satisfy (B). It is, however, unclear
how to combine these different runs in proving analogues of Lemmas 11 and 12.
7. Conclusion and Future Work
We have determined tight complexity bounds for the problem of deciding the existence of
interpolants and explicit definitions in standard DLs with nominals and/or role inclusions, with
and without ontologies. It would be of interest to investigate these decision problems also for
DLs with additional constructors (such as number restrictions and transitive closure) and for
acyclic ontologies.
We have also performed first steps in the analysis of the computation problem, but many
interesting problems remain to be addressed. First, note that our analysis only applies to the
case with ontologies and we expect interpolants in the ontology free case to be one exponential
smaller (if the universal role is not present). Second, we have provided only upper bounds on the
size of interpolants and it remains to see whether the construction is optimal (we conjecture it
to be). Finally, it is of great interest to compute interpolants also in the presence of nominals. An
alternative approach might be to derive them from a suitably constrained proof of ๐ช |= ๐ถ1 โ ๐ถ2
in an appropriate proof system, see e.g. [23].
References
[1] B. ten Cate, W. Conradie, M. Marx, Y. Venema, Definitorially Complete Description Logics,
in: Proc. of KR, 2006, pp. 79โ89.
[2] B. ten Cate, E. Franconi, I. Seylan, Beth definability in expressive description logics, J.
Artif. Intell. Res. 48 (2013) 347โ414.
[3] A. Artale, A. Mazzullo, A. Ozaki, F. Wolter, On Free Description Logics with Definite
Descriptions, in: Proc. of KR, 2021.
[4] J. C. Jung, C. Lutz, H. Pulcini, F. Wolter, Separating data examples by description logic
concepts with restricted signatures, in: Proc of KR, 2021.
[5] J. C. Jung, C. Lutz, H. Pulcini, F. Wolter, Logical separability of incomplete data under
ontologies, in: Proc. of KR, 2020.
[6] I. Seylan, E. Franconi, J. de Bruijn, Effective Query Rewriting with Ontologies over DBoxes,
in: Proc. of IJCAI, 2009, pp. 923โ925.
[7] E. Franconi, V. Kerhet, N. Ngo, Exact Query Reformulation over Databases with First-order
and Description Logics Ontologies, J. Artif. Intell. Res. 48 (2013) 885โ922.
[8] E. Franconi, V. Kerhet, Effective Query Answering with Ontologies and DBoxes, in:
Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader
on the Occasion of His 60th Birthday, 2019, pp. 301โ328.
[9] C. Lutz, I. Seylan, F. Wolter, The data complexity of ontology-mediated queries with closed
predicates, Logical Methods in Computer Science 15 (2019).
[10] D. Toman, G. E. Weddell, FO Rewritability for OMQ using Beth Definability and Interpola-
tion, in: Proc. of DL, 2021.
[11] D. Geleta, T. R. Payne, V. A. M. Tamma, An Investigation of Definability in Ontology
Alignment, in: Proc. of EKAW, 2016, pp. 255โ271.
[12] B. Konev, C. Lutz, D. K. Ponomaryov, F. Wolter, Decomposing description logic ontologies,
in: Proc. of KR, 2010.
[13] J. C. Jung, F. Wolter, Living without Beth and Craig: Definitions and interpolants in the
guarded and two-variable fragments, in: Proc. of LICS, 2021.
[14] M. Fortin, B. Konev, F. Wolter, Interpolants and explicit definitions in extensions of the
description logic EL, in: Proc. of KR, 2022.
[15] A. Artale, J. C. Jung, A. Mazzullo, A. Ozaki, F. Wolter, Living without Beth and Craig: Ex-
plicit definitions and interpolants in description logics with nominals and role hierarchies,
in: Proc. of AAAI, 2021.
[16] B. ten Cate, Lyndon Interpolation for Modal Logic via Type Elimination Sequences, Tech-
nical Report, ILLC, Amsterdam, 2022.
[17] M. Benedikt, B. ten Cate, M. Vanden Boom, Effective interpolation and preservation in
guarded logics, ACM Trans. Comput. Log. 17 (2016) 8:1โ8:46.
[18] J. C. Jung, A. Mazzullo, F. Wolter, More on interpolants and explicit definitions for descrip-
tion logics with nominals and/or role inclusions, 2022. Available at https://www.csc.liv.ac.
uk/~frank/publ/dl22interpolation.pdf.
[19] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
University Press, 2017.
[20] C. Lutz, R. Piro, F. Wolter, Description logic TBoxes: Model-theoretic characterizations
and rewritability, in: Proc. of IJCAI, 2011.
[21] V. Goranko, M. Otto, Model theory of modal logic, in: Handbook of Modal Logic, Elsevier,
2007, pp. 249โ329.
[22] C. Chang, H. J. Keisler, Model Theory, Elsevier, 1998.
[23] W. Rautenberg, Modal tableau calculi and interpolation, J. Philos. Log. 12 (1983) 403โ423.