Most Specific Generalizations w.r.t. General EL-TBoxes

1 Introduction

Description Logics (DL) allow to model application domains in a structured and well-understood way. Due to their formal semantics, DLs can offer powerful reasoning services.

In recent years the lightweight DL EL became popular as an ontology language for large-scale ontologies. EL provides the logical underpinning of the OWL 2 EL profile of the W3C web ontology language [W3C OWL Working Group, 2009], which is used in important life science ontologies, as for instance, SNOMED CT [Spackman, 2000] and the thesaurus of the US national cancer institute (NCI) [Sioutos et al., 2007], which contain ten thousands of concepts. The reason for the success of EL is that it offers limited, but sufficient expressive power, while reasoning can still be done in polynomial time [Baader et al., 2005].

In DLs basic categories from an application domain can be captured by concepts and binary relations by roles. Implications between concepts can be specified in the so-called TBox. A general TBox allows complex concepts on both sides of implications. Facts from the application domain can be captured by individuals and their relations in the ABox.

∗Partially supported by the German Research Foundation (DFG) in the Collaborative Research Center 912 "Highly Adaptive EnergyEfficient Computing".

Classical inferences for DLs are subsumption, which computes the sub- and super-concept relationships of named concepts and instance checking, which determines for a given individual whether it belongs to a given concept. Reasoning support for the design and maintenance of large ontologies can be provided by the bottom-up approach, which allows to derive a new concept from a set of example individuals, see [Baader et al., 1999]. For this kind of task the generalization inferences least common subsumer (lcs) and most specific concept (msc) are investigated for lightweight DLs like EL. The lcs of a collection of concepts is a complex concept that captures all commonalities of these concepts. The msc generalizes an individual into a complex concept, that is the most specific one (w.r.t. subsumption) of which the individual is an instance of.

Unfortunately, neither the lcs nor the msc need to exist, if computed w.r.t. general EL-TBoxes [Baader, 2003] or cyclic ABoxes written in EL [K¨usters and Molitor, 2002]. Let's consider the TBox statements:

Penicillin ⊑ Antibiotic ⊓ ∃kills.S-aureus, Carbapenem ⊑ Antibiotic ⊓ ∃kills.E-coli, S-aureus ⊑ Bacterium ⊓ ∃resistantMutant.Penicillin, E-coli ⊑ Bacterium ⊓ ∃resistantMutant.Carbapenem

We want to compute the lcs of Penicillin and Carbapenem. Now, both concepts are defined by the type of bacterium they kill. These, in turn, are defined by the substance a mutant of theirs is resistant to. This leads to a cyclic definition and thus the common subsumer cannot be captured by a finite ELconcept, since this would need to express the cycle. If computed w.r.t. a TBox that extends the above one by the axioms:

Antibiotic ⊑ ∃kills.Bacterium,

Bacterium ⊑ ∃resistantMutant.Antibiotic,

then the lcs of Penicillin and Carbapenem is just Antibiotic. We can observe that the existence of the lcs does not merely depend on whether the TBox is cyclic. In fact, for cyclic ELTBoxes exact conditions for the existence of the lcs have been devised [Baader, 2004]. However, for the case of general ELTBoxes such conditions are unknown.

There are several approaches to compute generalizations even in this setting. In [Lutz et al., 2010] an extension of EL with greatest fixpoints was introduced, where the generalization concepts always exist. Computation algorithms for approximative solutions for the lcs were devised in [Baader et al., 2007; Pe˜naloza and Turhan, 2011b] and for the msc in [K¨usters and Molitor, 2002]. The last two methods simply compute the generalization concept up to a given k, a bound on the maximal nestings of quantifiers. If the lcs or msc exists and a large enough k was given, then these methods yield the exact solutions. However, to obtain the least common subsumer and the most specific concept by these methods in practice, a decision procedure for the existence of the lcs or msc, resp., and a method for computing a sufficient k are still needed. This paper provides these methods for the lcs and the msc.

In this paper we first introduce basic notions for the DL EL and its canonical models, which serve as a basis for the characterization of the lcs introduced in the subsequent section. There we show that the characterization can be used to verify whether a given generalization is the most specific one and that the size of the lcs, if it exists, is polynomially bounded in the size of the input, which yields a decision procedure for the existence problem. In Section 4 we show the corresponding results for the msc. We end with some conclusions.

2 Preliminaries

2.1 The Description Logic EL

Let NC,NR and NI be disjoint sets of concept, role and individual names. Let A ∈ NC and r ∈ NR. EL-concepts are built according to the syntax rule

An interpretation I = (∆I , ·I ) consists of a non-empty domain ∆I and a function ·I that assigns subsets of ∆I to concept names, binary relations on ∆I to role names and elements of ∆I to individual names. The function is extended to complex concepts in the usual way. For a detailed description of the semantic of DLs see [Baader et al., 2003].

Let C, D denote EL-concepts. A general concept inclusion (GCI) is an expression of the form C ⊑ D. A (general) TBox T is a finite set of GCIs. A GCI C ⊑ D is satisfied in an interpretation I if C I ⊆ DI . An interpretation I is a model of a TBox T if it satisfies all GCIs in T .

Let a, b ∈ NI, r ∈ NR and C a concept, then C(a) is a concept assertion and r(a, b) a role assertion. An interpretation I satisfies an assertion C(a) if aI ∈ C I and r(a, b) if (aI , bI ) ∈ rI holds. An ABox A is a finite set of assertions. An interpretation I is a model of an ABox A if it satisfies all assertions in A. A knowledge base (KB) K consists of a TBox and an ABox (K = (T ,A)). An interpretation is a model of K = (T ,A) if it is a model of T and A. 1

Important reasoning tasks considered for DLs are subsumption and instance checking. A concept C is subsumed by a concept D w.r.t. a TBox T (denoted C ⊑T D) if C I ⊆ DI holds in all models I of T . A concept C is equivalent to a concept D w.r.t. a TBox T (denoted C ≡T D) if C ⊑T D and D ⊑T C hold. A reasoning service dealing with a KB is instance checking. An individual a is instance of the concept C w.r.t. K (denoted K |= C(a)) if aI ∈ C I holds in all models I of K. These two reasoning problems can be decided for EL in polynomial time [Baader et al., 2005].

1 Since we only use the DL EL, we write 'concept' instead of 'EL-concept' and assume all TBoxes, ABoxes and KBs to be written in EL in the following.

Based on subsumption and instance checking our two inferences of interest least common subsumer (lcs) and most specific concept (msc) are defined.

Definition 1. Let C,D be concepts and T a TBox. The concept E is the lcs of C, D w.r.t. T (lcsT (C,D)) if the properties

are satisfied. If a concept E satisfies Property 1 it is a common subsumer of C and D w.r.t. T .

The lcs is unique up to equivalence, while common subsumers are not unique, thus we write G ∈ csT (C, D).

The role depth rd(C) of a concept C denotes the maximal nesting depth of ∃ in C. If, in Definition 1 the concepts E and F have a role-depth up to k, then E is the role-depth bounded lcs (k-lcsT (C, D)) of C and D w.r.t. T .

NI,A is the set of individual names used in an ABox A.

Definition 2. Let a ∈ NI,A and K = (T ,A) a KB. A concept C is the most specific concept of a w.r.t. K (mscK(a)) if it satisfies:

If in the last definition the concepts C and D have a roledepth limited to k, then C is the role depth bounded msc of a w.r.t. K (k-mscK(a)). The msc and the k-msc are unique up to equivalence in EL.

2.2 Canonical Models and Simulation Relations

The correctness proof of the computation algorithms for the lcs and msc depends on the characterization of subsumption and instance checking, respectively. In case of an empty TBox, homomorphisms between syntax trees of concepts [Baader et al., 1999] were used. A characterization w.r.t. general TBoxes using canonical models and simulations was given in [Lutz and Wolter, 2010], which we want to use in the following.

Let X be a concept, TBox, ABox or KB, then NC,X (NR,X) denotes the set of concept names (role names) occurring in X and sub(X) denotes the subconcepts in X.

Definition 3. Let C be a concept and T a TBox.

The canonical model IC,T of C and T is defined as follows:

The notion of a canonical model can be extended to a KB.

Definition 4. Let K = (T , A) be a KB. The canonical model IK w.r.t. K is defined as follows:

To identify some properties of canonical models we use simulation relations between interpretations.

Definition 5. Let I1, I2 be interpretations. S ⊆ ∆I1 ×∆I2 is a simulation between I1 and I2 if the following conditions are satisfied for all A ∈ NC and for all r ∈ NR:

The tuple (I, d) denotes an interpretation I with d ∈ ∆I . If there exists a simulation S ⊆ ∆I ×∆J with (d, e) ∈ S, we write (I, d) ≲ (J , e) and say (J , e) simulates (I, d). We write (I, d) ≃ (J , e) if (I, d) ≲ (J , e) and (J , e) ≲ (I, d) holds. We summarize some important properties of canonical models.

Lemma 6. [Lutz and Wolter, 2010] Let C be a concept and T a TBox.

1. IC,T is a model of T .
2. For all models I of T and all d ∈ ∆I holds: d ∈ C I iff (IC,T , dC) ≲ (I, d).

This Lemma gives us a characterization of subsumption. A similar Lemma was shown for the instance relationship.

Lemma 7. [Lutz and Wolter, 2010] Let K be a KB. IK satisfies: 1. IK is a model of K. 2. K |= C(a) iff da ∈ C IK .

Next, we recall some known operations on interpretations. Taking an element d of the domain of an interpretation as the root, the interpretation can be unraveled into a possibly infinite tree. The nodes of the tree are words that correspond to paths starting in d. We have that π = dr1d1r2d2r3... is a path in an interpretation I, if the domain elements di and di+1 are connected via rI i+1 for all i.

Definition 8. Let I be an interpretation with d ∈ ∆I . The tree unraveling Id of I in d is defined as follows:

The length of an element σ ∈ ∆Id , denoted by |σ|, is the number of role names occurring in σ. If σ is of the form dr1d1r2...rmdm, then dm is the tail of σ denoted by tail(σ) = dm. The interpretation I ℓd denotes the finite subtree of the tree unraveling Id up to depth ℓ. Such a tree can be translated into an ℓ-characteristic concept of an interpretation (I, d).

Definition 9. Let (I, d) be an interpretation. The ℓcharacteristic concept Xℓ (I, d) is defined as follows:

3 Existence of Least Common Subsumers

In this section we develop a decision procedure for the problem whether for two given concepts and a given TBox the least common subsumer of these two concepts exists w.r.t. the given TBox. If not stated otherwise, the two input concepts are denoted by C and D and the TBox by T .

Similar to the approach used in [Baader, 2004] we proceed by the following steps:

1. Devise a method to identify lcs-candidates for the lcs. The set of lcs-candidates is a possibly infinite set of common subsumers of C and D w.r.t. T , such that if the lcs exists then one of these lcs-candidates actually is the lcs.
2. Characterize the existence of the lcs. Find a condition such that the problem whether a given common subsumer of C and D w.r.t. T is least (w.r.t. ⊑T ), can be decided by testing this condition.
3. Establish an upper bound on the role-depth of the lcs. We give a bound ℓ such that if the lcs exists, then it has a roledepth less or equal ℓ. By such an upper bound one needs to check only for finitely many of the lcs-candidates if they are least (w.r.t. ⊑T ).

The next subsection addresses the first two problems, afterwards we show that such a desired upper bound exists.

3.1 Characterizing the Existence of the lcs

The characterization presented here is based on the product of canonical models. This product construction is adopted from [Baader, 2003; Lutz et al., 2010] where it was used to compute the lcs in EL with gfp-semantics and in the DL ELν , respectively.

To obtain the k-lcsT (C,D) we build the product of the canonical models (IC,T , dC) and (ID,T , dD) and then take the k-characteristic concept of this product model.

Lemma 10. Let k ∈ N.

This and all the proofs omitted in this paper due to space constraints can be found in [Zarrieß and Turhan, 2013].

In the following we take Xk (IC,T × ID,T , (dC, dD)) as a representation of the k-lcsT (C,D). It is implied by Lemma 10 that the set of k-characteristic concepts of the product model (IC,T × ID,T , (dC, dD)) for all k is the set of lcscandidates for the lcsT (C, D), which can be stated as follows.

Corollary 11. The lcsT (C,D) exists iff there exists a k ∈ N such that for all ℓ ∈ N: k-lcsT (C,D) ⊑T ℓ-lcsT (C,D).

Obviously, this doesn't yield a decision procedure for the problemwhether the k-lcsT (C,D) is the lcs, since subsumption cannot be checked for infinitely many ℓ in finite time.

Next, we address step 2 and show a condition on the common subsumers that decides whether a common subsumer is least or not. The main idea is that the product model captures all commonalities of the input concepts by means of canonical models. Thus we compare the canonical models of the common subsumers and the product model using simulationequivalence ≃.

Proof sketch. For any F ∈ csT (C,D) it holds by Lemma 6, Claim 3 that (IF,T , dF ) is simulated by (IC,T , dC) and (ID,T , dD) and therefore also by (IC,T × ID,T , (dC, dD)).

Assume (IE,T , dE) is simulation-equivalent to the product model. We need to show that E ≡T lcsT (C,D). By transitivity of ≲ it is implied that (IF,T , dF ) ≲ (IE,T , dE) and E ⊑T F by Lemma 6. Therefore E ≡T lcsT (C,D).

For the other direction assume E ≡T lcsT (C,D). It has to be shown that (IE,T , dE) simulates the product model. Let J(dC,dD) be the tree unraveling of the product model. Since E is more specific than the k-characteristic concepts of the product model for all k (by Corollary 11), (IE,T , dE) simulates the subtree J k (dC,dD) of J(dC,dD) limited to elements up to depth k, for all k. For each k we consider the maximal simulation from J k (dC,dD) to (IE,T , dE). Note that ((dC, dD), dE) is contained in any of these simulations. Let σ be an element of ∆J(dC,dD) at an arbitrary depth ℓ. We show how to determine the elements of ∆IE,T , that simulate this fixed element σ. Let Sn(σ) be the maximal set of elements from ∆IE,T that simulate σ in each of the trees J n (dC,dD) with n ≥ ℓ. We can observe that the infinite sequence (Sℓ+i(σ))i=0,1,2,... is decreasing (w.r.t. ⊇). Therefore at a certain depth we reach a fixpoint set. This fixpoint set exists for any σ. It can be shown that the union of all these fixpoint sets yields a simulation from the product model to (IE,T , dE).

By the use of this Lemma it can be verified whether a given common subsumer is the least one or not, which we illustrate by an example.

Example 13. Consider again the TBox from the introduction (now displayed with abbreviated concept names)

and the following extended TBox

In Figure 1 we can see that

but it is not the lcs, because its canonical model cannot simulate the product model (IP,T1 × IC,T1 , (dP, dC)). The concept A, however, is the lcs of P and C w.r.t. T2. We have (IP,T2 × IC,T2 , (dP, dC)) ≲ (IA,T2 , dA) since any element from ∆IP,T2 ×IC,T2 in AIP,T2 ×IC,T2 or BIP,T2 ×IC,T2 is simulated by A or B, respectively.

The characterization of the existence of the lcs given in Corollary 11 can be reformulated using Lemma 12.

Corollary 14. The lcsT (C,D) exists iff there exists a k such that the canonical model of Xk (IC,T ×ID,T , (dC, dD)) w.r.t. T simulates (IC,T ×ID,T , (dC, dD)).

This corollary still doesn't yield a decision procedure for the existence problem, since the depth k is still unrestricted. Such a restriction will be developed in the next section.

3.2 A Polynomial Upper Bound on the Role-depth of the lcs

In this section we show that, if the lcs exists, its role-depth is bounded by the size of the product model. First, consider again the TBox T2 from Example 13, where A ⊑T2 ∃kills.(B ⊓ ∃resistantMutant.A) holds, which results in a loop in the product model through the elements A, A and B, B. Furthermore, the cycles in the product model involving the roles kills and resistantMutant are captured by the canonical model IA,T2 . Therefore A ≡T2 lcsT2 (P, C). On this observation we build our general method.

We call elements (dF , dF ′) ∈ ∆IC,T ×ID,T synchronous if F = F ′ and asynchronous otherwise. The structure of (IC,T × ID,T , (dC, dD)) can now be simplified by considering only synchronous successors of synchronous elements.

In order to find a number k, such that the product model is simulated by the canonical model of K =Xk (IC,T ×ID,T , (dC, dD)), we first represent the model (IK,T , dK) as a subtree of the tree unraveling of the product model J(dC,dD) with root (dC, dD). We construct this representation by extending the subtree J k (dC,dD) by new tree models at depth k. We need to ensure that the resulting interpretation, denoted by ̂ J k (dC,dD) , is a model of T , that is simulation-equivalent to (IK,T , dK). The elements σ ∈ ∆J k (dC,dD) with |σ| = k that we extend and the corresponding trees we append to them are selected as follows: Let M be a conjunction of concept names and ∃r.F ∈ sub(T ). If σ ∈ M J k (dC,dD) and M ⊑T ∃r.F, then we append the tree unraveling of the canonical model I∃r.F,T . Furthermore, we consider elements that have a tail that is a synchronous element. If tail(σ) = (dF , dF ), then F is called tail concept of σ. To select the elements with a synchronous tail, that we extend by the canonical model of their tail concept, we use embeddings of J k (dC,dD) into (IK,T , dK). Let H = {Z1, ...,Zn} be the set of all functional simulations Zi from J k (dC,dD) to (IK,T , dK) with Zi((dC, dD)) = dK. We say that σ with tail concept F is matched by Zi if Zi(σ) ∈ F IK,T . The set of elements σ ∈ ∆J k (dC,dD) with |σ| = k, that are matched by a functional simulation Zi is called matching set, denoted by M(Zi). Now consider the setM(H) := {M(Z1), ...,M(Zn)}. If σ is contained in all maximal matching sets fromM(H), then we extend σ by the tree unraveling of the canonical model of its tail concept w.r.t. T .

We can show that the resulting interpretation ̂ J k (dC,dD) has the desired properties.

Having this representation of the canonical model of the k-lcsT (C,D) we first show a sufficient condition for the existence of the lcs.

Corollary 16. If all cycles in (IC,T ×ID,T , (dC, dD)), that are reachable from (dC, dD) consist of synchronous elements, then the lcsT (C,D) exists.

Proof sketch. There exists an ℓ ∈ N such that all paths in the tree unraveling J(dC,dD) of (IC,T ×ID,T , (dC, dD)) starting in (dC, dD) have a maximal asynchronous prefix up to length ℓ, i.e., if there exists an element at depth ≥ ℓ + 1, then it is a synchronous element. Consider the number

We unravel (IC,T × ID,T , (dC, dD)) up to depth ℓ +m+ 1 such that we get J ℓ+m+1 (dC,dD) . Now it is ensured that the corresponding model ̂ J ℓ+m+1 (dC,dD) contains all paths with a maximal asynchronous prefix up to length ℓ. It is implied that ̂ J ℓ+m+1 (dC,dD) = J(dC,dD). From Lemma 15 and Corollary 14 it follows that Xℓ+m+1 (IC,T ×ID,T , (dC, dD)) is the lcs.

As seen in Example 13 for T2, this is not a necessary condition for the existence of the lcs.

Another consequence of Lemma 15 is, that if the product model (IC,T × ID,T , (dC, dD)) has only asynchronous cycles reachable from (dC, dD), then the lcsT (C,D) does not exist. Since in this case J(dC,dD) is infinite but ̂ J k (dC,dD) is finite for all k ∈ N, a simulation from (IC,T ×ID,T , (dC, dD)) to ̂ J k (dC,dD) never exists for all k. For instance, this case applies to Example 13 w.r.t. to T1.

The interesting case is where we have both asynchronous and synchronous cycles reachable from (dC, dD) in the product model. In this case we choose a k that is large enough and then check whether the canonical model of Xk (IC,T ×ID,T , (dC, dD)) w.r.t. T simulates the product model.

We show in the next Lemma that the role-depth of the lcsT (C,D), if it exists, can be bounded by a polynomial, that is quadratic in the size of the product model.

Proof sketch. Assume lcsT (C,D) exists. From Corollary 14 and Lemma 15 it follows that there exists a number ℓ such that

Every path in ̂ J ℓ (dC,dD) has a maximal asynchronous prefix of length ≤ ℓ. From depth ℓ + 1 on there are only synchronous elements in the tree ̂ J ℓ (dC,dD) . From (1) it follows that every path p in (IC,T × ID,T , (dC, dD)) starting in (dC, dD), is simulated by a corresponding path pℓ in ̂ J ℓ (dC,dD) also starting in (dC, dD). The simulation chain of p and pℓ is depicted in Figure 2. The idea is to use the simulating path pℓ to construct a simulating path in ̂ J ℓ (dC,dD) (also starting in (dC, dD)) with a maximal asynchronous prefix of length ≤ n2 , where n2 is the number of pairs of elements from ∆IC,T ×ID,T . Intuitively, if pℓ has a maximal asynchronous prefix that is longer than n2 , then there are pairs in the simulation chain that occur more than once. This is used to construct a simulating path with a shorter maximal asynchronous prefix step-wise. After a finite number of steps the result is a simulating path, such that all pairs consisting of asynchronous elements in the corresponding simulation chain are pairwise distinct. Therefore we need only asynchronous elements from ̂ J ℓ (dC,dD) up to depth n2 to simulate the product model. Then we add m+1 to n2 to ensure that ̂ J n2+m+1 (dC,dD) contains all paths fromJ(dC,dD) starting in (dC, dD), that have a maximal asynchronous prefix of length ≤ n2 . As argued above ̂ J n2+m+1 (dC,dD) simulates (IC,T × ID,T , (dC, dD)).

Using Lemma 12 and Lemma 17 we can now show the main result of this paper.

Theorem 18. Let C,D be concepts and T a general TBox. It is decidable in polynomial time whether the lcsT (C, D) exists. If the lcsT (C, D) exists it can be computed in polynomial time.

Proof. First we compute the bound k as given in Lemma 17 and then the k-characteristic concept K of (IC,T × ID,T , (dC, dD)). The canonical model of K can be build according to Definition 3 in polynomial time [Baader et al., 2005]. Next we check whether (IC,T × ID,T , (dC, dD)) ≲ (IK,T , dK) holds, which can be done in polynomial time. If yes, K is the lcs by Lemma 12 and if no, the lcs doesn't exist by Lemma 17.

The results from this section can be easily generalized to the lcs of an arbitrary set of concepts M = {C1, ...,Cm} w.r.t. a TBox T . But in this case the size of the lcs is already exponential w.r.t. an empty TBox [Baader et al., 1999]. In this general case we have to take the product model

whose size is exponential in the size of M and T , as input for the methods introduced in this section. Then the same steps as for the binary version can be applied.

4 Existence of Most Specific Concepts

We show now that the results obtained for the lcs, can be easily applied to the existence problem of the msc.

Example 19 (From [K¨usters and Molitor, 2002]). The msc of the individual a w.r.t. the following KB

doesn't exist, whereas w.r.t. the modified KB

C is the msc of a.

To decide existence of the msc of an individual a w.r.t. a KB K = (T , A), we again start with defining the set of msccandidates for the msc by taking the k-characteristic concept of the canonical model (IK, da) of K.

Lemma 20. Let k ∈ N. It holds that K |= Xk (IK, da)(a) and for a concept E with rd(E) ≤ k, K |= E(a) implies Xk (IK, da) ⊑T E.

Therefore Xk (IK, da) ≡T k-mscK(a). Now we use the canonical model of Xk (IK, da) w.r.t. the TBox component T of K and the model (IK, da) to check whether Xk (IK, da) is the most specific concept.

Lemma 21. For a concept C it holds that C ≡T mscK(a) iff (IK, da) ≃ (IC,T , dC).

By this Lemma the existence of the msc can be characterized as follows.

Corollary 22. The mscK(a) exists iff there exists a k such that the canonical model of Xk (IK, da) w.r.t. T simulates (IK, da).

To decide whether an appropriate k exists such that Xk (IK, da) simulates (IK, da), we further examine the structure of (IK, da). In Example 19 da has a self-loop in the model (IK1 , da), but the canonical models of Xk (IK1 , da) are finite for all k ∈ N, because the TBox is empty. Therefore a simulation never exists. In comparison, the model (IK2 , da) has additionally a self-loop at dC and the canonical models of Xk (IK2 , da) w.r.t. T2 also contain this loop.

Intuitively, in the general case, the elements in ∆IK , that are elements in bIK (for b ∈ NI,A), correspond to the asynchronous elements of the product of canonical models and the elements dC ∈ ∆IK for some concept C, correspond to the synchronous elements. The model (IK, da) also has an analogous structure compared to the product model (IC,T × ID,T , (dC, dD)) in the sense that elements in ∆IK , that belong to concepts only have successor elements that belong to concepts. Therefore similar arguments as presented in Section 3.2 can be used to show, that a representation of the canonical model of Xk (IK, da) as a subtree of the tree unraveling of (IK, da) can be obtained. This representation is denoted by ̂ J k da . This model is used to show an upper bound on the role-depth k of the msc.

Lemma 23. Let m := max({rd(F) | F ∈ sub(K)}) and n := |NI,A|. If the mscK(a) exists, then (IK, da) ≲ ̂ J n2+m+1 da .

The results of this section can be summarized in the following theorem.

Theorem 24. Let K = (T ,A) be a KB and a ∈ NI,A. It is decidable in polynomial time whether the mscK(a) exists. If the mscK(a) exists, it can be computed in polynomial time.

Proof sketch. First we compute the bound k as given in Lemma 23 and then the k-characteristic concept Xk (IK, da). The canonical model of K can be build according to Definition 4 in polynomial time [Baader et al., 2005]. Then we check whether (IK, da) ≲ (IC,T , dC) holds, which can be done in polynomial time. If yes, C is the msc and if no, the msc doesn't exist by Corollary 22.

All the proofs omitted here due to space constraints are given in [Zarrieß and Turhan, 2013].

5 Conclusions

In this paper we have studied the conditions for the existence of the lcs and of the msc, if computed w.r.t. general TBoxes or cyclic ABoxes, respectively, written in the DL EL. In this setting neither the lcs nor the msc need to exist. It was an open problem to give necessary and sufficient conditions for their existence. We showed that the existence problem of the msc and the lcs of two concepts is decidable in polynomial time. Furthermore, we showed that the role-depth of these most specific generalizations can be bounded by a polynomial. This upper bound k can be used to compute the msc or lcs, if it exists. Otherwise the computed concept can still serve as an approximation [Pe˜naloza and Turhan, 2011b].