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.
Craig interpolants and explicit definitions have many potential applications in ontology
engineering and ontology-based information systems. Examples include the extraction of equivalent
acyclic TBoxes from ontologies [
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 [
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 [
For a discusson of further related work on interpolation, Beth definability, interpolant
existence, and explicit definition existence we refer the reader to [
We first introduce standard DL definitions and notation [
The semantics is given in terms of interpretations ℐ = (Δℐ , · ℐ ), defined as usual [
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 ∈ ℐ if ∈ , 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 [
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 [
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) [
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 if 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 [
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 afect the complexity of explicit definition existence.
We obtain the following complexity result as a consequence of Theorems 1-2 and Lemmas 3-4.
ontology-free interpolant existence (with RIs) and ontology-free explicit definition existence (with RIs) are both 2ExpTime-complete.
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.
Σ ⊆ 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 [
sig(, 1, 2). Then the following conditions are equivalent:
ℐ1
1 ∼ ℒ,Σ ∼ ℒ,Σ ¬2
The existence of explicit definitions can be characterized as follows.
signature. Then the following conditions are equivalent:
ℐ1 1 , 1, 2
1 ⊓ ∃.⊤ ∼ ℒℋ,Σ ∼ ℒℋ,Σ ∼ ℒℋ,Σ 1 2 2 2 ′ 2 ⊓ ¬∃.⊤ ℐ2 ℐ2
We formulate our main complexity result about the problem of deciding the existence of interpolants and explicit definitions.
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 NExpTimehardness 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()).
• 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}, relations ,, ⊆ () × (′) 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.
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 , (, ) ∈ if ∈ . • 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
(0, ) (2, )
(1, )
2 (2, ) (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.
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.
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 [
Let 1, 2 be Ξ-types. We call 1, 2 -equivalent if for every ∃. ∈ Ξ, we have ∃. ∈ 1 if ∃. ∈ 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 ⇝ , ′ if ′ ⇝ − , . 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′) if (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: ∈ if ∈ ′, 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 of 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 if a mosaic ( , ∅) survives elimination. In what follows, let Real denote the set of all sets of types which are jointly realizable modulo ℒ(Σ)-bisimulations.
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 1,2 = ∃.(
1′∈⊔Real, 1⇝ 1′,⇝ ,′,∈′∈1′ 22′∈⇝Rea2l′, l 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.
Real × Real such that 1 ∈ 1 and ¬2 ∈ 2 for some types 1 ∈ 1 and 2 ∈ 2. Then, l =
1∈⊔Real: 2∈Real: there is 1 ∈ 1 with 1 ∈ 1 there is 2 ∈ 2 with ¬2 ∈ 2 1,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 [
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]. 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.