While the computation of Craig interpolants for description logics (DLs) with the Craig Interpolation Property (CIP) is well understood, very little is known about the computation and size of interpolants for DLs without CIP or if one aims at interpolating concepts in a weaker DL than the DL of the input ontology and concepts. In this paper, we provide the first elementary algorithms computing (i) ℒ interpolants between ℒ-concepts under ℒℋ-ontologies and (ii) ℒ interpolants between ℒ-concepts under ℒ-ontologies. The algorithms are based on recent decision procedures for interpolant existence. We also observe that, in contrast, uniform depth restricted interpolants might be of non-elementary size.
Interpolants between description logic (DL) concepts have found many applications. For instance, they
can be used as explicit concept definitions or referring expressions, as explanations for concept inclusions,
as rewritings of queries, and as separating concepts in the context of concept learning [
The situation is very diferent for DLs that do not enjoy the CIP or if one is interested in interpolating
concepts in a weaker DL than the concepts used in the inclusion. In this case, the existence of an
interpolating concept does not follow from the validity of the inclusion and extracting interpolating
concepts from proofs becomes much harder. In fact, very little is known about how this could be done
and research has so far focused on deciding the existence of interpolants rather than constructing
them [
It is well known that Craig interpolants of ℒ concept inclusions under ℒℋ ontologies do not
necessarily exist [
Mosaic elimination procedures decide the existence of interpolants, but they do not construct any interpolants. The aim of this paper is to give the first elementary algorithms constructing ℒ interpolants whenever they exist under ontologies in ℒℋ and under ontologies and concept inclusions in ℒ. Our algorithms are not restricted to computing Craig interpolants, but work for arbitrary signatures. The idea of the algorithms is to run the mosaic elimination procedures discussed above and construct, in addition and inductively, for each eliminated mosaic entailed ℒ(Σ) concepts that witness non Σ -bisimilar satisfiability of its types. The witness concepts we propose are not aggregated at each step, but are polyadic in the sense that we define, for any set of concepts (types in the case of mosaics) which are not satisfiable in Σ -bisimilar nodes, for each ∈ an ℒ(Σ) concept Sep() such that the following holds: • |= ⊑ Sep() for all ∈ ; • |= ⊓∈ Sep() ⊑ ⊥.
The concept Sep() constructed for = {, ¬} is then the desired interpolant. We note that an
earlier attempt to construct interpolants while running a mosaic elimination procedure without using
polyadic separators does not work as stated [
We first introduce the syntax and semantics of the basic description logics ℒ, ℒℋ, and ℒ and introduce some model theory. We refer the reader to [19] for a comprehensive introduction to description logics. Let NC, and NR be mutually disjoint and countably infinite sets of concept, and role names. An ℒ concept is defined according to the syntax rule
, ::= ⊤ | | ¬ | ⊓ | (≥ .) where ranges over concept names, over role names, and ≥ 0. We use the standard abbreviations ∃. for (≥ 1 .), ∀. for ¬∃.¬, ⊔ for ¬(¬ ⊓ ¬), and → for ¬ ⊔ . An ℒ concept is an ℒ concept in which for every subformula (≥ 1 .), is actually 1. An ℒ concept inclusion (ℒ CI) takes the form ⊑ for ℒ concepts and . ℒ concept inclusions are defined accordingly. An ℒ ontology is a finite set of ℒ CIs. An ℒℋ ontology is a finite set of ℒ concept inclusions and role inclusions (RIs) ⊑ where , are role names from NR. The size of a (finite) syntactic object , denoted ‖‖, is the number of symbols needed to represent it as a word, and the role depth of a concept is the maximal nesting depth of concept constructors (≥ .).
As usual, the semantics is defined in terms of interpretations ℐ = (∆ ℐ , · ℐ ), where ∆ ℐ is a non-empty set, called domain of ℐ, and · ℐ is a function mapping every ∈ NC to a subset of ℐ ⊆ ∆ ℐ and every ∈ NR to a subset of ℐ ⊆ ∆ ℐ × ∆ ℐ . The extension ℐ of a concept in ℐ is defined as usual. An interpretation ℐ satisfies a CI ⊑ if ℐ ⊆ ℐ and an RI ⊑ if ℐ ⊆ ℐ . We say that ℐ is a model of an ontology if it satisfies all inclusions in it. A concept is satisfiable under ontology if there is a model ℐ of with ℐ ̸= ∅. Moreover, is subsumed by another concept under if ℐ ⊆ ℐ in every model ℐ of . We write |= ⊑ in this case.
We next introduce the studied notions and associated problems. A signature is a set Σ of concept
and role names. An ℒ(Σ) concept is an ℒ concept that uses only concept and role names from Σ .
Let ℒ, ℒ′ be DLs, and let us fix an ℒ ontology , ℒ concepts , , and a signature Σ . Then, an ℒ′(Σ)
interpolant for |= ⊑ is an ℒ′(Σ) concept with |= ⊑ and |= ⊑ . The associated
decision problem of ℒ′(Σ) interpolant existence over ℒ ontologies and concepts has been recently
studied and shown decidable [
The proof of Lemma 1 is based on the fact that Σ -bisimulations capture the expressive power of ℒ(Σ) concepts, and crucially relies on the use of compactness. In particular, it is not constructive in the sense that in the proof of implication 2 ⇒ 1, no interpolant is constructed. We study here the associated computation problems, that is, compute the interpolants if they exist. A notion dual to the notion of an interpolant is that of a separator. Given concepts , , we call a separator for , if ⊑ and ⊑ ¬. Clearly, is a separator for , if it is an interpolant for , ¬. Thus, the problems of finding interpolants and separators for a given pair of concepts are algorithmically equivalent. We will switch between these two perspectives depending on which one is more convenient in a given context.
In this section, we are concerned with computing ℒ interpolants of concept inclusions under ℒℋ
ontologies. We start with an example that illustrates the failure of the computation algorithm given
in [
Example 2. Fix ≥ 1, = { ⊑ , ⊑ ′ | ≤ }, Σ = {′, | ≤ }, and = ∃. ⊓ ∀.( → ⊔≤ ) and = ⊓≤ ∀.¬.
We show that , are not jointly ∼ ℒ,Σ-consistent under . Indeed, if , are jointly ∼
ℒ,Σconsistent, then all concepts in = { ⊓ ( → ⊔≤ )} ∪ {¬ | ≤ } are satisfied in mutually
Σ -bisimilar nodes, which is clearly not the case. By Lemma 1, there is an ℒ(Σ) interpolant for
|= ⊑ ¬. For instance, = ⊔≤ ∃′. is an ℒ(Σ) interpolant. The algorithm from [
We first show how a natural idea for computing interpolants, which works in several other settings, fails to compute elementary sized interpolants in the presence of role inclusions. Next we provide an algorithm which does compute elementary interpolants.
A natural idea to compute interpolants could be to show first that, if there is an ℒ(Σ) interpolant for |= 0 ⊑ 0, then there is one of small role depth , and then use the strongest ℒ consequence of 0 of this role depth . Let ≥ 0. A (Σ , )-uniform interpolant of 0 under is an ℒ(Σ) concept such that |= 0 ⊑ and |= ⊑ for every ℒ(Σ) concept of role depth at most with |= 0 ⊑ . A (Σ , )-uniform interpolant for 0 under always exists, and can be used as an interpolant for |= 0 ⊑ whenever an ℒ(Σ) interpolant for |= 0 ⊑ of role depth exists. This idea has been used to compute elementary sized modal logic interpolants of -calculus formulae [20] and it follows from its proof that it applies to computing interpolants under ℒ ontologies. We actually conjecture that it works for the majority of DLs enjoying the CIP, but we leave an elaboration for future work. Unfortunately, contrary to these settings, in our case (Σ , )-uniform interpolants need not be elementary in , and consequently do not lead to elementary sized interpolants. In what follows we denote by Tower the iterated exponential function, that is, Tower(0) = 1 and Tower( + 1) = 2Tower().
Theorem 3. There is an ℒℋ ontology , an ℒ concept 0, and signature Σ such that there is no (Σ , )-uniform interpolant of 0 under smaller than Tower( − 2).
Proof. Consider the ℒℋ ontology = { ⊑ , ⊑ ′}, the concept 0 = ∃.⊤ and Σ = {, ′}. We claim that no concept of size smaller than Tower( − 2) is a (Σ , )-uniform interpolant for 0 under . Assume towards contradiction that there is such an . Observe that for every ∈ ℒ(Σ) of depth − 1, ∀. → ∃′. is an ℒ(Σ) concept of depth and |= 0 ⊑ (∀. → ∃′.). Hence |= ⊑ (∀. → ∃′.). Consider all trees of depth − 1, choose one for every equivalence class of Σ -bisimulation and denote the set of all these chosen trees by . We have Tower( − 1) ≤ | | and ‖ ‖ < Tower( − 2). Thus, by the pigeonhole principle there are two diferent ℐ1, ℐ2 ∈ whose respective roots 1, 2 satisfy exactly the same sub-concepts of . Every two trees in are distinguished by some ∈ ℒ(Σ) of depth − 1, so let us pick such that 1 ∈ ℐ1 but 2 ∈/ ℐ2 . We claim that ̸|= ⊑ ∀. → ∃′., which contradicts that is an (Σ , )-uniform interpolant. This is witnessed by an interpretation constructed as follows. First take the disjoint union of ℐ1, ℐ2. Then take two fresh points 1, 2, and add edges 1 → 1, 1 → 1, 1 →′ 1 and 2 → 1, 2 →′ 2. Since |= 0 ⊑ and 0 is true at 1 we have 1 ∈ . This implies 2 ∈ because and ′ satisfy the same subconcepts of . But ∀. → ∃′. is false at 2, a contradiction.
On the positive side, we show the following second main result.
Theorem 4. Let be an ℒℋ ontology, 0, 0 ℒ concepts, and Σ be a signature. Then, if there is an ℒ(Σ) interpolant for |= 0 ⊑ 0, we can construct the DAG representation of such an interpolant in time double exponential in ‖‖ + ‖0‖ + ‖0‖.
The proof is by extending a known mosaic elimination procedure for deciding joint ∼
ℒ,Σconsistency for input ontology and concepts formulated in ℒℋ [
Let us fix an ℒℋ ontology , ℒ concepts 0, 0, and a signature Σ . We denote with sub(, 0, 0) the set of subconcepts that occur in , 0, 0, closed under single negation. A type for is any subset of sub(, 0, 0) realizable in a model of , that is, any set ⊆ sub(, 0, 0) such that there is a model ℐ of and element ∈ ∆ ℐ with = tpℐ () where:
tpℐ () = { ∈ sub(, 0, 0) | ∈ ℐ }.
We often treat a type as the conjunction of all concepts it contains, which allows us to write, for instance, |= ⊑ . A mosaic for is a set of types for . We say that a type is a completion of a concept ∈ sub(, 0, 0) if ∈ , and a mosaic is a completion of a set ⊆ sub(, 0, 0) of concepts if contains a completion of every ∈ .
Intuitively, a mosaic describes a collection of elements in an interpretation ℐ which realize precisely the types in and are mutually Σ -bisimilar. Naturally, not every set of types can be realized in this way, and we use a mosaic elimination procedure to determine which can. We write ⇝ ′ if an element of type ′ is a viable -successor of an element of type , that is, { | ∀. ∈ } ⊆ ′. We will denote { | ∀. ∈ } = / . We write ⇝ ′ if for every ∈ , there is ′ ∈ ′ with ⇝ ′. Let ℳ be a set of mosaics. A mosaic ∈ ℳ is bad if it violates one of the following conditions: (Atomic Consistency) for every , ′ ∈ and ∈ Σ , ∈ if ∈ ′; (Existential Saturation) for every ∈ and ∃. ∈ , there is ′ ∈ ℳ such that (a) ∈ ′ for some ′ ∈ ′ with ⇝ ′ and (b) if |= ⊑ for some ∈ Σ , then ⇝ ′.
Along the lines of the proof of Lemma 6.5 in [
Lemma 5. 0 and 0 are jointly ∼ ℒ,Σ-consistent under if there is a set ℳ* of mosaics that does not contain a bad mosaic and such that there is ∈ ℳ* and 1, 2 ∈ with 0 ∈ 1 and 0 ∈ 2.
It is a consequence of Lemma 5 that joint ∼ ℒ,Σ-consistency under ℒℋ ontologies can be decided in double exponential time. Indeed, an ℳ* as in Lemma 5 can be found (if it exists) by exhaustively eliminating bad mosaics from the set of all mosaics. Since the set of all mosaics is of double exponential size, and each round of the elimination procedure can be performed in time polynomial in the size of the current set of mosaics, the upper bound follows. By the link to interpolant existence provided in Lemma 1, also ℒ(Σ) interpolant existence is decidable in double exponential time.
Our aim is to extend the described mosaic elimination procedure by computing, for each type in an eliminated mosaic, its “contribution” to the elimination. To formalize this we introduce a polyadic notion of a separator reflecting the fact that a mosaic may contain more than two types. Assume a set of concepts. An ℒ(Σ) separator for is a function Sep from to ℒ(Σ) -concepts such that: • |= ⊑ Sep() for every ∈ ; • |= ⊓∈ Sep() ⊑ ⊥.
We call ℒ(Σ) -separable if there is an ℒ(Σ) separator for . We will use the following lemma which connects separation of concepts with separation of their completions.
Lemma 6. Assume a set ⊆ sub(, 0, 0) of concepts. The following are equivalent:
Proof. The implication (1) =⇒ (2) is straightforward because a separator for is a separator for every completion of .
For the other implication (2) =⇒ (1) assume that for every completion of we have a separator. Let cp() denote the set of all functions from to types which map every ∈ to one of its completions. The image [] of every such function ∈ cp() is a completion of , and thus, by assumption, is separated by some Sep .
We define a separator Sep for by setting, for every ∈ :
Sep() = com⊔pletion ∈cp()
⊓ of ()=
Sep () (* )
To prove |= ⊑ Sep() assume ℐ |= and ∈ ℐ . Let be the type tpℐ () of . Clearly, is a completion of . By assumption, for every ∈ cp() and ∈ we have |= () ⊑ Sep (). satisfies: Hence, for every ∈ cp() such that () = we get |= ⊑ Sep (). It follows that ∈ (Sep())ℐ .
It remains to show that |= ∈
⊓ Sep() ⊑ ⊥. Assume towards contradiction an interpretation ℐ |= with ∈ (⊓∈ Sep())ℐ . By definition of Sep, for every there is a completion such that ⊓ ∈cp() ()=
Sep ().
Consider a function ∈ cp() defined as () = for every . It follows that satisfies Sep () for every . This contradicts the assumption that {Sep () | ∈ } is a separator for the image of and as such is inconsistent.
We inductively define separators for each eliminated mosaic. Recall that there are two ways a mosaic can be eliminated: the base case when violates atomic consistency, and the inductive case when violates existential saturation. We look at these cases in turn.
Inductive Base. If violates atomic consistency then there is a concept name ∈ Σ and types , ′ ∈ with ∈ and ¬ ∈ ′. Let Sep() be if ∈ and ¬ otherwise. It follows that |= ⊑ Sep() for all , and ⊓ Sep() ⊑ ⊥.
∈
Inductive Step. Denote the current set of mosaics by ℳ and assume a mosaic ∈ ℳ is eliminated because it violates existential saturation. This means that there are ∈ and ∃. ∈ such that whenever ′ ∈ ℳ satisfies (i) ⇝ ′ for all |= ⊑ , and (ii) contains some ′ ∈ ′ with ⇝ ′ and ∈ ′ then ′ ∈/ ℳ. Consider the set:
= {′/ | ′ ∈ , ∈ Σ , and |= ⊑ } ∪ {{} ∪ / }.
It follows that every completion ′ of was already eliminated from ℳ: left and right part of the union correspond to parts (i) and (ii) of the violated condition. Lemma 6 provides us with a separator Sep for . We use Sep to get a separator Sep for as follows. We put:
⊓ |=⊑,
∈Σ Sep(′) = ∀.Sep(′/ ) and
Sep() = ¬ ⊓′̸= Sep(′) = ⊔ ⊔ ′̸= |=⊑, ∈Σ ∃.¬Sep(′/ ). for every ′ ̸= .
We claim that Sep separates . For every ′ ̸= we have |= ′ ⊑ Sep(′). This follows because for every |= ⊑ with ∈ Σ we have |= ′ ⊑ ∀.′/ and |= ′/ ⊑ Sep(′/ ). To show |= ⊑ Sep() assume an interpretation ℐ |= with ∈ ℐ . The point has an -child satisfying {} ∪ / and hence also Sep({} ∪ / ). By definition of a separator, the image Sep[] of Sep is inconsistent. Thus, the fact that satisfies Sep({} ∪ / ) implies that some concept ∈ Sep[] other than Sep({} ∪ / ) must be false at . We therefore have ∈ (¬Sep(′/ ))ℐ for some |= ⊑ with ∈ Σ and some ′. Since for every ∈ Σ with |= ⊑ we have ∈ (/ )ℐ and thus ∈ (Sep(/ ))ℐ , it follows that ′ ̸= . This proves that ∈ (Sep())ℐ . Note that Sep[ ] is inconsistent by definition: the concept Sep() is just a negated conjunction ⊓ Sep(′) of the rest. This ′̸= completes the proof that Sep separates .
This finishes the construction of separators for every eliminated mosaic. To construct the actual interpolant, note that Lemmas 1 and 5 imply that, if there is an ℒ(Σ) interpolant for |= 0 ⊑ 0, then all completions of {0, ¬0} have been eliminated. Lemma 6 provides us with an ℒ(Σ) separator Sep for {0, ¬0} and it is easy to see that Sep(0) is the sought ℒ(Σ) interpolant.
It remains to analyze the DAG size of the constructed separators, which we do by counting the number of sub-formulae used in the constructed separators. On a high-level, we construct one formula for every type in every eliminated mosaic. This formula is of negligible size 1 in the inductive base, so let us analyze the inductive step. This step relies on Lemma 6, and one can see that the construction in Equation (* ) uses double exponentially many sub-formulae. It remains to note that the Lemma is invoked only double exponentially often and that the construction of the separator formulae for the just eliminated concept introduces only double exponentially many sub-formulae. This completes the proof of Theorem 4.
We finish the section with some remarks regarding the size of the constructed interpolants. First, we strongly conjecture that there are examples in which the interpolant is forced to have double exponential role depth, so the upper size bound in Theorem 4 is optimal. Second, it is known that the size of DAG representation of interpolants in standard DLs enjoying the CIP is at most exponential [6, Theorem 3.26] and thus there is an exponential gap.
We are concerned with computing ℒ interpolants of concept inclusions in ℒ under ℒ ontologies. We use the same notation for ℒ as in the previous section for ℒℋ, defined in the obvious way. Our first result is that (Σ , )-uniform ℒ interpolants can be of non-elementary size. Theorem 7. There is an ℒ concept 0 and signature Σ such that there is no (Σ , )-uniform ℒ interpolant of 0 smaller than Tower( − 2).
Proof. Take the concept 0 = (≤ 1 .⊤), signature Σ = {, , ′}, and let > 0. Using ℒ(Σ) concepts ∃. → ∀. one can show the lower bound in the same way as in the proof of Theorem 3.
The main result of this section is as follows.
Theorem 8. Let be an ℒ ontology, 0, 0 ℒ concepts, and Σ be a signature. If there is an ℒ(Σ) interpolant for |= 0 ⊑ 0, then there is one of 3-exponential size which can be constructed in 4-exponential time in ‖‖ + ‖0‖ + ‖0‖.
Fix an ℒ ontology , ℒ concepts 0, 0, and a signature Σ . Our algorithm for computing interpolants again relies on a mosaic elimination procedure that determines the mosaics for which there is a model ℐ of which realizes the types in in mutually Σ -bisimilar nodes. To formalize the elimination condition, we need some new notation. Let ∙ ∈ N be maximal such that (≥ ∙ .) occurs in sub(, 0, 0) for some , . Let ∙ = {0, . . . , ∙ } ∪ {∞}, and define < and + on ∙ as usual by setting, for instance, ∙ < ∞ and + ∞ = ∞. For a role name and type , a witnessing function , assigns to every type ′ a ,(′) ∈ ∙ such that for each (≥ .) ∈ sub(, 0, 0), (≥ .) ∈ if ∑︀∈′ ,(′) ≥ . If is realizable, then there exists a witnessing function , for each role name : take a model ℐ of realizing in a node and define ,(′) = {︃ ∞ if = |{′ ∈ ∆ ℐ | (, ′) ∈ ℐ , ′ = tpℐ (′)}| ≤ ∙ otherwise. (1) Let be a mosaic, a role name, and (,)∈ be witnessing functions. To satisfy the types in a mosaic in mutually Σ -bisimilar nodes one must be able to partition, for ∈ Σ , their -successors into mosaics so that the back- and-forth conditions of Σ -bisimulations hold. Our formalization of this idea follows [18], but we modify the notation for our purposes. Say that a set of mosaics is a mosaic partition for (,)∈ if one can assign to each , ′ with ∈ and ,(′) > 0 a non-empty set (, ′) ⊆ (intuitively, the mosaics in containing ′ as an -successor of ) with ′ ∈ ′ for all ′ ∈ (, ′) in such a way that • for every ′ ∈ and ∈ , there exists a ′ ∈ ′ with ′ ∈ (, ′); • for all types , ′, |(, ′)| ≤ ,(′).
Let ℳ be a set of mosaics. A mosaic ∈ ℳ is bad if it violates one of the following conditions: (Existential Saturation) for every role name ∈ Σ there are witnessing functions (,)∈ and a mosaic partition ⊆ ℳ for (,)∈ .
The following result is shown in [18] (using slightly diferent wording): Lemma 9. (i) If the condition (Existential Saturation) is satisfied for some ∈ ℳ, then this is witnessed by a mosaic partition ⊆ ℳ with || ≤ ∙ × 22|sub(,0,0)|.
(ii) 0, 0 are jointly ∼ ℒ,Σ-consistent under if there is a set ℳ* of mosaics that does not contain a bad mosaic and such that there is ∈ ℳ* and 1, 2 ∈ with 0 ∈ 1 and 0 ∈ 2.
It is a consequence of Lemma 9 that joint ∼ ℒ,Σ-consistency under ℒ ontologies can be decided in double exponential time. Indeed, an ℳ* as in Lemma 9 can be found (if it exists) by exhaustively eliminating bad mosaics from the set of all mosaics. Since the set of all mosaics is of double exponential size, and each round of the elimination procedure can be performed in double exponential time, the upper bound follows. By the link to interpolant existence provided in Lemma 1, also ℒ(Σ) interpolant existence is decidable in double exponential time.
We next exploit the elimination procedure to construct interpolants. Similar to the previous Section 3 we compute an ℒ(Σ) separator for every eliminated mosaic. It will be convenient to actually compute something slightly stronger. Let ℳ be a set of mosaics. A function Sep that maps every in some ∈ ℳ to an ℒ(Σ) concept Sep() is called general ℒ(Σ) separator for ℳ if for every ∈ ℳ the restriction of Sep to is an ℒ(Σ) separator for .
We compute, by induction, a general ℒ(Σ) separator for the set of eliminated mosaics.
Inductive Base. Assume has been eliminated because atomic consistency is violated. Then there exists ∈ Σ such that the function Sep defined by setting Sep () = if ∈ and Sep () = ¬ otherwise, is an ℒ(Σ) separator for . Let ℰ0 be the set of all mosaics that violate atomic consistency and let Sep be defined as above for ∈ ℰ0. Then we obtain a general separator Sep0 for ℰ0 by setting Sep0() = Sep (), for all ∈ ∈ ℰ0.
⊓∈ℰ0
Inductive Step. Assume ℰ is the set of eliminated mosaics and Sep is a general separator for ℰ. Let ℳ be the set of mosaics that have not yet been eliminated. Setting Sep() = ⊤ for types that do not occur in any mosaic in ℰ, we may assume that Sep is defined for all types. Let be the mosaic eliminated in the next step. Then existential saturation is violated in ℳ. Note that this implies that one can pick a role name ∈ Σ such that for every witnessing functions ,, ∈ , and mosaic partition for (,)∈ there is an eliminated mosaic ′ ∈ ∩ ℰ. We fix such an .
Let be the set of all types. Denote by + the set of all conjunctions = ⊓ with ∈ ∈ {Sep(), ¬Sep()}. For any nonempty subset ℬ ⊆ + we set as usual ∇(ℬ) = ( ⊓ ∃.) ⊓ ∀.( ⊔ ).
∈ℬ ∈ℬ ∈ ∖ {0}.
Let () be the disjunction of all ∇(ℬ) such that ⊓ ∇(ℬ) is satisfiable under . Observe that |= ⊑ (). Take any 0 ∈ and set Sep(0) = ¬ () and Sep() = () for all ⊓ ∈ ∖{0} Proof. It sufices to show that |= 0 ⊑ Sep(0), the remaining conditions are trivial. Assume this is not the case. Then we have a model ℐ0 of and some 0 ∈ ∆ ℐ0 such that 0 ∈ (0 ⊓ (∈ ⊓∖{0} ())ℐ0 . Pick the (unique) ℬ ⊆ + such that 0 ∈ ∇(ℬ)ℐ0 . Then ∇(ℬ) is a disjunct of each () with ∈ . Take interpretations ℐ and with ∈ ( ⊓ ∇(ℬ))ℐ for ∈ ∖ {0}. We may assume that all ℐ, ∈ , coincide (otherwise take their disjoint union) and denote it by ℐ. Next define, for ∈ , ,(′) as in (1). Then (,)∈ is a family of witnessing functions. Let for each ∈ ℬ:
= {tpℐ () | there is ∈ with (, ) ∈ ℐ and ∈ ℐ } By the definition of ℬ, ̸= ∅ for every ∈ ℬ. Observe that none of the mosaics is in ℰ because otherwise |= ∈⊓ Sep() ⊑ ⊥ which is not the case since Sep() is a conjunct of for all ∈ .
We show that { | ∈ ℬ} form a mosaic partition for (,)∈ , and so derive a contradiction. To this end define (, ′) ⊆ { | ∈ ℬ} as
{ | there is ∈ ℐ with (, ) ∈ ℐ and tpℐ () = ′} To see that (, ′) is as required, first observe that ′ ∈ for any ∈ (, ′). Next assume that a with ∈ ℬ and ∈ are given. From ∈ ( ⊓ ∇(ℬ))ℐ we obtain a with (, ) ∈ ℐ and ∈ ℐ . Let ′ = tpℐ (). Then ∈ (, ′). The condition |(, ′)| ≤ .(′) follows directly from the definitions.
Using Lemma 10 we obtain a general ℒ(Σ) separator Sep+1 for ℰ ∪ { } by setting Sep+1() = Sep() ⊓ Sep() for all ∈ and Sep+1() = Sep() for all remaining types.
This finishes the construction of separators for every eliminated mosaic. One can now construct the actual interpolants in exactly the same way as in the previous section for ℒℋ via Lemma 6. To compute the size of the interpolants, observe that in the construction above ‖Sep+1()‖ ≤ ‖ Sep()‖× 22() 2 with a polynomial function and = ‖‖ + ‖0‖ + ‖0‖. As Sep stabilizes after at most double exponentially many elimination steps, ‖Sep‖ is bound by a 3-exponential function in ‖‖ + ‖0‖ + ‖0‖. This bound remains 3-exponential under DAG representation. The construction of Sep() involves satisfiability checks for concepts of 3-exponential size, so overall the interpolant can be constructed in 4-exponential time.
We have presented first non-trivial algorithms for computing ℒ interpolants under ℒℋ and ℒ ontologies, relying on the new notion of polyadic separators tailored to store witnesses for the fact that a mosaic (or set of types) cannot be realized in mutually bisimilar models. Theorems 4 and 8 demonstrate the inherent dificulty of the problem and explain why previously known techniques do not easily apply in the cases of ℒℋ and ℒ. It is worth to note that Theorem 4 can be easily modified to obtain non-elementary lower bounds for the size of uniform interpolants at the concept level in the presence of ℒℋ ontologies. These lower bounds, in turn, translate to non-elementary lower bounds for the size of uniform interpolants at the ontology level in ℒℋ. This implies that the resolution based calculus for computing uniform interpolants of ℒℋ ontologies from [21] cannot run in elementary time, answering a question posed by the authors.
In the future, we would like to extend our algorithms to other standard DL constructors. While we
believe that this will be rather easy for some constructors, like inverse roles or the universal role, we
expect it to be much more involved in other cases such as nominals. In fact, already unifying the two
presented algorithms into one for computing ℒ interpolants under ℒℋ ontologies appears to
be challenging. It would be also interesting to analyze our procedures in the ontology-free cases (or with
an ontology containing only role inclusions), for which we expect smaller interpolants. From a practical
perspective, it would be interesting to extend implemented tableaux algorithms to be able to compute
interpolants. Beyond description logics, it would be very interesting to compute interpolants in the
guarded and/or the two-variable fragments of first-order logic [
The authors have not employed any Generative AI tools. modal logic, in: Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023, 2023, pp. 417–428.
URL: https://doi.org/10.24963/kr.2023/41. doi:10.24963/KR.2023/41. [17] B. Konev, C. Lutz, D. Walther, F. Wolter, Formal properties of modularisation, in: H. Stuckenschmidt, C. Parent, S. Spaccapietra (Eds.), Modular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization, volume 5445 of Lecture Notes in Computer Science, Springer, 2009, pp. 25–66. URL: https://doi.org/10.1007/978-3-642-01907-4_3. doi:10.1007/978-3-642-01907-4\ _3. [18] L. Kuijer, T. Tan, F. Wolter, M. Zakharyaschev, Separation and definability in fragments of two-variable first-order logic with counting, 2025. URL: https://arxiv.org/abs/2504.20491. arXiv:2504.20491. [19] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
University Press, 2017. [20] J. C. Jung, J. Kolodziejski, Modal separation of fixpoint formulae, in: O. Beyersdorf, M. Pilipczuk, E. Pimentel, K. T. Nguyen (Eds.), 42nd International Symposium on Theoretical Aspects of Computer Science, STACS 2025, March 4-7, 2025, Jena, Germany, volume 327 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, pp. 55:1–55:20. doi:10.4230/LIPICS.STACS.2025.55. [21] P. Koopmann, R. Schmidt, Count and forget: Uniform interpolation of shq-ontologies, in: International Joint Conference on Automated Reasoning, 2014. URL: https://api.semanticscholar. org/CorpusID:38753229. Lemma 11. 0 and 0 are jointly ∼ ℒ,Σ-consistent under if there is a set ℳ* of mosaics that does not contain a bad mosaic and such that there is ∈ ℳ* and 1, 2 ∈ with 0 ∈ 1 and 0 ∈ 2. Proof (Sketch). For implication “⇒”, suppose that 0, 0 are jointly ∼ ℒ,Σ-consistent under , that is, there are models ℐ1, ℐ2 of and elements 1 ∈ 0ℐ1 and 2 ∈ 0ℐ2 such that ℐ1, 1 ∼ ℒ,Σ ℐ2, 2. Since ℒℋ is preserved under taking disjoint unions, we can assume without loss of generality that ℐ1 = ℐ2 = ℐ. We read of a set ℳ* of mosaics by taking
ℳ* = { {tpℐ () | ℐ, ∼ ℒ,Σ ℐ, } | ∈ ∆ ℐ }.
It is routine to verify that ℳ* satisfies the conditions formulated in Lemma 5.
For implication “⇐”, let ℳ* be a set of mosaics that does not contain a bad mosaic and such that there is * ∈ ℳ* and 1, 2 ∈ * with ∈ 1 and ∈ 2. We construct an interpretation ℐ as follows: ∆ ℐ = {(, ) | ∈ ℳ* and ∈ } ℐ = {(, ) ∈ ∆ ℐ | ∈ } ℐ = {((, ), (′, ′)) ∈ ∆ ℐ × ∆ ℐ | ⇝ ′ and for all ∈ Σ : (( |= ⊑ ) ⇒ ⇝ ′)} One can verify by structural induction that ∈ (, ) if (, ) ∈ ℐ , for all ∈ sub(, 0, 0) and (, ) ∈ ∆ ℐ . Consequently, (1, * ) ∈ 0ℐ and (2, * ) ∈ 0ℐ . Moreover, following relation : = {(, ), (′, ) | ∈ ℳ* } is a Σ -bisimulation. Since ((1, * ), (2, * )) ∈ , we conclude that 0, 0 are jointly ∼ ℒ,Σconsistent under .