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.