Role-depth bounded Least Common Subsumer in Prob-EL with Nominals Andreas Ecke1? , Rafael Peñaloza1,2?? , and Anni-Yasmin Turhan1? ? ? 1 Institute for Theoretical Computer Science, Technische Universität Dresden 2 Center for Advancing Electronics Dresden {ecke,penaloza,turhan}@tcs.inf.tu-dresden.de Abstract. Completion-based algorithms can be employed for comput- ing the least common subsumer of two concepts up to a given role-depth, in extensions of the lightweight DL EL. This approach has been applied also to the probabilistic DL Prob-EL, which is variant of EL with sub- jective probabilities. In this paper we extend the completion-based lcs- computation algorithm to nominals, yielding a procedure for the DL Prob-ELO01 c . 1 Introduction The least common subsumer (lcs) is a reasoning service that generalizes a set of input concept descriptions into a single concept description that subsumes all the input concepts and is the least one w.r.t. subsumption. This inference has turned out to be quite useful for a number of applications, like the definition of similarity measures for concept descriptions [5, 7], the bottom-up construction of knowledge bases [4], information retrieval, and more (see [6, 16]). In particular, for large biomedical ontologies the lcs can be used effectively to aid construction and maintenance. Many of these biomedical ontologies, notably SNOMED CT [12]and the Gene Ontology [1], are written in the EL-family of lightweight description logics. An interesting extension of EL that still admits tractable reasoning is the use of nominals. Nominals basically allow to characterize a concept in terms of specific individuals. Nominals are also admitted in the OWL 2 EL profile of OWL [14] and thus are interesting to practical applications. For the EL-family of DLs there exist completion-based classification algorithms [3] that compute all the subsumption relations between all named concepts and nominals in an ontology in polynomial time. Kazakov et al. showed in [11] that the original completion algorithm is indeed incomplete for ELO and introduced a complete ? Supported by DFG Graduiertenkolleg 1763 (QuantLA). ?? Partially supported by DFG within the Cluster of Excellence ‘cfAED’ ??? Partially supported by the German Research Foundation (DFG) in the Collaborative Research Center 912 “Highly Adaptive Energy-Efficient Computing”. consequence-based classification algorithm for this DL. This algorithm is a vari- ant of the completion-based algorithm, with the additional benefit of exhibiting a pay-as-you-go behavior, and thus allows for efficient implementation. Another extension of EL is Prob-EL [13], which allows the modeling of un- certain knowledge by introducing probabilistic constructors. Prob-EL uses sub- jective (or Type-2 [10]) probabilities, which correspond to degrees of belief and are interpreted using a multiple-world semantics. For example, in Prob-EL one can express that obese people are likely to have high pressure, without requiring every obese person to be hypertense, using the GCI Obese v P≥0.9 ∃hasCondition.HighPressure. A completion algorithm for classifying TBoxes in the sublanguage Prob-EL01 c of Prob-EL was described in [13]. For general EL-TBoxes with cyclic concept definitions, the lcs may not exist, as it may require an infinite nesting of existential restrictions to be expressed. Therefore, an approximation has been introduced in [16], that limits the maxi- mal nesting of quantifiers of the resulting concept descriptions. These approxi- mations, called role-depth bounded lcs (k-lcs), can be computed for EL with role inclusions by using completion sets produced by the completion-based classifi- cation algorithm [8]. In this paper, we give a classification algorithm for the classic DL ELO intro- duced in [11] in terms of the completion algorithm in order to extend the k-lcs to this DL. Furthermore, we extend the completion algorithm for (a moderate form of) subjective probabilities to nominals, which results in a classification algorithm for the DL Prob-ELO01 c . In this direction, we correct a small error from the algorithm in [13] that caused it to be incomplete. From this algorithm, we develop an algorithm that computes the k-lcs for Prob-ELO01 c . We show that for both lcs approximations, the resulting concept description subsumes all input concepts, and is the least one w.r.t. subsumption. Thus, if the exact lcs exists for some role-depth bound n, then the k-lcs is exact for k ≥ n. Recently, necessary and sufficient conditions for the existence of the lcs w.r.t. general EL- TBoxes have been devised [17]. By the use of these conditions the k for which the role-depth bound lcs and the lcs coincide can be determined, if the lcs exists. The paper is organized as follows. First, we introduce some basic notions. In Section 3 we give a completion algorithm for EL with nominals and extend the k-lcs algorithm to this DL. The completion-based classification algorithm for Prob-ELO01 c is devised in Section 4, along with the algorithm for the k-lcs for this probabilistic DL. We end with conclusions and remarks on future work. The main proofs of Section 4 have been deferred to the appendix. 2 Preliminaries ELO-concept descriptions are built from mutually disjoint sets NC of concept names, NR of role names and NI of individual names using the syntax rule: C, D ::= > | A | {a} | C u D | ∃r.C, Table 1. Concept constructors and TBox axioms for ELO. Syntax Semantics named concept A (A ∈ NC ) AI ⊆ ∆I top concept > ∆I nominal {a} (a ∈ NI ) {a}I = {aI } conjunction C uD (C u D)I = C I ∩ DI existential restriction ∃r.C (r ∈ NR ) (∃r.C)I = {d ∈ ∆I | ∃e.(d, e) ∈ rI ∧ e ∈ C I } GCI CvD C I ⊆ DI where A ∈ NC , r ∈ NR and a ∈ NI . As usual the semantics of ELO-concepts are defined by means of interpretations. The semantics of named concepts and roles are extended to concept descriptions as shown in the upper part of Table 1. An ELO-TBox consists of a finite set of general concept inclusion axioms (GCIs) of the form C v D. We use C ≡ D as an abbreviation for C v D and D v C. With Sig(T ) we denote the signature of a TBox T , i.e., the set of all concept, role, and individual names that occur in T . An interpretation is a model for a TBox if it satisfies all its GCIs, as shown in the lower part of Table 1. The central inference discussed in this paper is the least common subsumer (lcs) of two concept descriptions, i.e., to compute a concept that subsumes both and is the least one w.r.t. subsumption. Since the lcs does not need to exist for general EL-TBoxes [2], we follow the idea from [16] and compute an approxima- tion of the lcs that limits the role depth (rd(C)), i.e., the maximal nesting of quantifiers of the resulting concept C: Definition 1 (Role-depth bounded lcs). Let L be a DL, T be an L-TBox and k ∈ IN. The role-depth bounded least common subsumer of two L-concept descriptions C1 , C2 w.r.t. T (written: k-lcsT (C1 , C2 )) is the L-concept descrip- tion D s.t.: 1. rd(D) ≤ k, 2. C1 vT D and C2 vT D, and 3. for each L-concept description E holds: C1 vT E and C2 vT E and rd(E) ≤ k, implies D vT E. For the DLs considered in this paper, the k-lcs is unique up to equivalence for a given k; thus we speak of the k-lcs. 3 The k-lcs in ELO The algorithms to compute the role-depth bounded lcs are based on completion- based classification algorithms for the corresponding DL. For ELO, a consequence- based classification algorithm is given by Kazakov et al. in [11], building upon the incomplete completion algorithm developed in [3]. The completion algorithm presented next adapts the ideas of the complete algorithm. 3.1 Completion Algorithm for Classification of ELO-TBoxes The completion algorithms works on normalized TBoxes. We define for ELO the set of basic concepts for a TBox T as BCT = (Sig(T ) ∩ (NC ∪ NI )) ∪ {>}. An ELO-TBox T is in normal form if every GCI contained in T is of one of the forms: A v B, A1 u A2 v B, A v ∃r.B, or ∃r.A v B, with A, A1 , A2 , B ∈ BCT . All ELO-TBoxes can be transformed into normal form in linear time by applying a set of normalization rules similar to those given in [3].Before describing the completion algorithm in detail, we introduce the reachability relation R , which plays a fundamental role in the correct treatment of nominals [3, 11]. Definition 2 ( R ). Let T be an ELO-TBox in normal form, G ∈ NC a concept name, and D ∈ BCT . G R D iff there exist roles r1 , . . . , rn and basic concepts A0 , . . . , An , B0 , . . . , Bn ∈ BCT , n ≥ 0 such that Ai vT Bi for all 0 ≤ i ≤ n, Bi−1 v ∃ri .Ai ∈ T for all 1 ≤ i ≤ n, A0 is either G or a nominal, and Bn = D. Informally, the concept name D is reachable from G if there is a chain of ex- istential restrictions leading to D that starts either with G or with a nominal. This implies that, for G R D, if the interpretation of G is not empty, then the interpretation of D cannot be empty either. This, in turn can cause equivalence of concepts, e.g. |AI | > 0 and A v {b} implies A ≡ {b}. The basic idea of the completion algorithm for EL (without nominals) is to store all basic concepts that subsume a concept A ∈ (Sig(T ) ∩ NC ) ∪ {>} in its subsumer set S(A) and and all basic concepts B for which ∃r.B subsumes A in the subsumer set S(A, r). These completion sets are then extended using a set of completion rules. However, with nominals the algorithm needs to keep track of completion sets of the form S G (A) and S G (A, r) for every G ∈ (Sig(T ) ∩ NC ) ∪ {>}, since the non-emptiness of an interpretation of a concept G may imply additional subsumption relationships for A. The completion set S G (A) for A ∈ BCT therefore stores all basic concepts that subsume A under the assumption that G is not empty. Similarly S G (A, r) stores all concepts B for which ∃r.B subsumes A under the same assumption. For every G ∈ (Sig(T ) ∩ NC ) ∪ {>}, every basic concept A and every role name r, the completion sets are initialized as S G (A) = {A, >} and S G (A, r) = ∅. The completion sets are then extended by applying the completion rules adapted from [11] and shown in Figure 1 exhaustively. It can be shown that the algorithm terminates in polynomial time, and is sound and complete for classifying the TBox T [11]. In particular, if no rules are applicable the completion sets have the following properties. Proposition 1 ([11]). Let T be an ELO-TBox in normal form to which the completion rules have been applied exhaustively, C, D ∈ BCT , r ∈ Sig(T ) ∩ NR , and G = C if C ∈ NC and G = > otherwise. Then, the following properties hold: OR1 If A1 ∈ S G (A), A1 v B ∈ T and B 6∈ S G (A), then S G (A) := S G (A) ∪ {B} OR2 If A1 , A2 ∈ S G (A), A1 u A2 v B ∈ T and B 6∈ S G (A), then S G (A) := S G (A) ∪ {B} OR3 If A1 ∈ S G (A), A1 v ∃r.B ∈ T and B 6∈ S G (A, r), then S G (A, r) := S G (A, r) ∪ {B} OR4 If B ∈ S G (A, r), B1 ∈ S G (B), ∃r.B1 v C ∈ T and C 6∈ S G (A), then S G (A) := S G (A) ∪ {C} OR5 If {a} ∈ S G (A1 ) ∩ S G (A2 ), G R A2 , and A2 ∈ / S G (A1 ), G G then S (A1 ) := S (A1 ) ∪ {A2 } Fig. 1. Completion rules for ELO C vT D iff D ∈ S G (C), and C vT ∃r.D iff there exists E ∈ BCT such that E ∈ S G (C, r) and D ∈ S G (E). We now show how to use these completion sets for computing the role-depth bounded lcs for ELO-concept description w.r.t. a general ELO-TBox. 3.2 Computing the Role-depth Bounded ELO-lcs In order to compute the role-depth bounded lcs of two ELO-concepts C and D, we follow an idea very similar to the one presented for ELR-concepts in [8], where we compute the cross product of the tree unravelings of the completion graph for C and D up to the role-depth k. Clearly, in the presence of nominals, the right completion sets need to be chosen such that they preserve the non-emptiness of the interpretation of concepts derived by R . An algorithm that computes the role-depth bounded ELO-lcs using comple- tion sets is shown in Figure 2. In the first step, the algorithm introduces two new concept names A and B as abbreviations for the concepts C and D, and the augmented TBox is normalized. The completion sets are then initialized and the completion rules from Figure 1 are applied exhaustively, yielding the saturated completion sets. In the recursive procedure k-lcs-r for concepts A and B, we first obtain all the basic concepts that subsume both A and B from the sets S A (A) and S B (B). For every role name r, the algorithm then recursively computes the (k−1)-lcs of the concepts A0 and B 0 in the subsumer sets S A (A, r) and S B (B, r), i.e. for which A vT ∃r.A0 and B vT ∃r.B 0 . The resulting concepts are conjoined as existential restrictions to the resulting k-lcs. The algorithm only introduces concept and role names that occur in the original TBox T . Therefore those names introduced by the normalization are not used in the concept description for the k-lcs and an extra denormalization step as in [16, 8] is not necessary. Notice, that for every pair (A0 , B 0 ) of r-successors of A and B it holds that A R A0 and B R B 0 . Intuitively, we are assuming that the interpretation of both A and B is not empty. This in turn causes the interpretation of ∃r.A0 and ∃r.B 0 to be not empty, either. Thus, it suffices to consider the completion sets S A (. . .) Procedure k-lcs(C, D, T , k) Input: C, D: ELO-concept descriptions; T : ELO-TBox; k ∈ IN Output: role-depth bounded ELO-lcs of C, D w.r.t. T and k 1: T 0 := normalize(T ∪ {A ≡ C, B ≡ D}) 2: ST := apply-completion-rules(T 0 ) 3: return k-lcs-r(A, B, ST , k, A, B, Sig(T )) Procedure k-lcs-r(X, Y, ST , k, A, B, Sig(T )) Input: A, B: concept names, X, Y : basic concepts with A R X, B R Y ; k ∈ IN; ST : set of saturated completion sets; Sig(T ): signature of T Output: role-depth bounded ELO-lcs of X, Y w.r.t. T and k 1: CN := S A (X) ∩ S B (Y ) ∩ BCT 2: if k = 0 then l 3: return P P ∈CN 4: else 5: return l l  l  P u ∃r.k-lcs-r E, F, ST , k−1, A, B, Sig(T ) P ∈CN r∈Sig(T )∩NR E∈S A (X,r), F ∈S B (Y,r) Fig. 2. Computation algorithm for role-depth bounded ELO-lcs. 0 0 and S B (. . .), without the need to additionally compute S A (. . .) and S B (. . .), or the completion sets S E (. . .) for any other basic concept E encountered during the recursive computation of the k-lcs. This allows for a goal-oriented optimization in cases where there is no need to classify the full TBox. 4 The k-lcs in Prob-ELO 01 c So far, we have discussed only classic DLs that can be used to represent and reason with certain knowledge. However, it is not uncommon to encounter sit- uations where a degree of uncertainty is unavoidable. This is often the case in the medical and biological domains, where knowledge is obtained through clini- cal testing, and there might exist hidden, or not completely understood, factors affecting the outcome. For instance, we would like to be able to express that obese people are likely to have high pressure, without asserting that every obese person must have high pressure. The probabilistic logic Prob-EL was introduced by [13] as an extension of EL that allows to express uncertain knowledge through probabilistic concepts and roles. Here, we extend these ideas to cover also nominals. Formally, Prob-ELO concepts extend classical ELO concepts with the constructors P.q C and ∃P.q r.C, where r ∈ NR , . ∈ {>, <, ≥, ≤, =}, and q ∈ [0, 1]. Intuitively, a concept of the form P.q C denotes the class of all objects that belong to C with a probability .q. For the above example, we can use the concept P≥0.9 ∃hasCondition.HighPressure to represent the class of all individuals that are likely to have high pressure. The semantics of this logic generalizes the semantics of classical ELO by con- sidering a set of possible worlds, corresponding to a formalization of subjective (or Type 2) probabilities [10]. Formally, the semantics of Prob-ELO are based on probabilistic interpretations of the form I = (∆I , W, (Iw )w∈W , µ), where ∆I is a (non-empty) domain, W is a non-empty set of (possible) worlds, µ is a discrete probability distribution over W , and for every w ∈ W , Iw is a classical ELO interpretation with domain ∆I . Additionally, for every a ∈ NI and every two worlds w, w0 ∈ W , it holds that aIw = aIw0 . From a probabilistic interpretation, we can compute the probability that a given element of the domain d ∈ ∆I belongs to the interpretation of a named concept A, and respectively, the probability that a pair of individuals are related via a role r as follows: pId (A) := µ({w ∈ W | d ∈ AIw }), pId,e (r) := µ({w ∈ W | (d, e) ∈ rIw }). The functions Iw and pId are extended to general concepts through the following mutual recursion. >Iw = ∆I , (∃r.C)Iw = {d ∈ ∆I | ∃e ∈ C Iw .(d, e) ∈ rIw }, (C u D)Iw = C Iw ∩ DIw , (P.q C)Iw = {d ∈ ∆I | pId (C) . q}, ({o})Iw = {oIw }, (∃P.q r.C)Iw = {d ∈ ∆I | ∃e ∈ C Iw .pId,e (r) . q}, pId (C) = µ({w ∈ W | d ∈ C Iw }). We say that the probabilistic interpretation I = (∆I , W, (Iw )w∈W , µ) satisfies the GCI C v D if for every world w ∈ W it holds that C Iw ⊆ DIw . I is a model of the TBox T if I satisfies all GCIs in T . A concept C is subsumed by concept D w.r.t. the TBox T (C vT D), if every model I of T satisfies C v D. Unfortunately, the probabilistic constructors increase the complexity of rea- soning, and deciding subsumption becomes intractable. In fact, as shown in [9], the problem is ExpTime-complete, even if only one constructor of the form P.q with q ∈ (0, 1) is allowed. Moreover, the problem becomes PSpace-hard if prob- abilistic existential restrictions of the form ∃P>0 r or ∃P=1 r are used. To regain tractability Prob-EL was restricted in [13] to probabilistic concepts of the form P>0 C or P=1 C and no probabilistic existential restrictions or roles, yielding the DL Prob-EL01 01 c . The extension of this DL by nominals is Prob-ELO c , which is the DL we consider for the remainder of the paper. 4.1 Completion Algorithm for Prob-ELO 01 c The basic idea of the completion algorithm for Prob-ELO01c is the same as in the crisp case: to construct a canonical model of the given TBox. In order to intro- duce it, we need to extend the notion of basic concepts to the new constructors BCT = (Sig(T ) ∩ (NC ∪ NI )) ∪ {>} ∪ {P>0 A, P=1 A | A ∈ Sig(T ) ∩ NC }. Since probabilistic interpretations contain a set of worlds, the completion al- gorithm has to work on sets of completion sets: one for each world and, since Prob-ELO01 T c also contains nominals, for each basic concept. Let P0 denote the set of all probabilistic concepts of the form P>0 A appearing in T . The com- pletion algorithm uses a set of worlds V := {0, 1, ε} ∪ P0T ; this way, for each GCI B v P>0 A ∈ T the world v = P>0 A serves as witness for this subsump- tion. Therefore, the Prob-ELO01 G c completion sets are now of the form S∗ (X, v) G or S∗ (X, r, v) where X is a concept name, >, or a nominal, v ∈ V , G is a concept name or >, ∗ ∈ {0, ε} and r is a role name. The completion sets con- tain basic concepts from BCT . The normal form for Prob-ELO01 c -TBoxes is the same as the normal form as for ELO-TBoxes, i.e. each axiom is of the form C v D, C1 u C2 v D, C v ∃r.A, or ∃r.A v D, with C, C1 , C2 , D ∈ BCT and A ∈ (Sig(T ) ∩ NC ) ∪ {>}. The reachability relation for Prob-ELO01c -concepts extends the one for ELO in distinguishing between concept names X and probabilistic concepts P>0 X. For example, non-emptiness of G does not imply non-emptiness of P>0 X, even if G R X, e.g. in worlds with probability 0. Similarly, non-emptiness of G does not imply non-emptiness of X for G R P>0 X. Therefore we introduce two kinds 0 ε of reachability relation, G R X for G R X and G R X for G R P>0 X: Definition 3 (Reachability of Prob-ELO01 c -concept descriptions). Let T be a Prob-ELO01 c -TBox in normal form, G ∈ NC ∪ {>}, and D ∈ NC ∪ NI . 0 G R D iff there exist r1 , . . . , rn ∈ NR and basic concepts A0 , . . . , An where Ai ∈ S0G (Ai−1 , ri , 0) for all 1 ≤ i ≤ n, such that A0 is either G or a nominal and An = D. ε 0 G R D iff G R X, P>0 Y ∈ S0G (X, 0) and there are r1 , . . . , rn ∈ NR and A0 , . . . , An ∈ NC with Ai ∈ SεG (Ai−1 , ri , ε) for all 1 ≤ i ≤ n such that A0 = Y and An = D. 0 ε When it is clear from the context which relation R or R we are using, we will sometimes denote it simply as R . Additionally, nominals interact with the set of possible worlds in a different way than normal concepts. In particular, the concepts P>0 {a} and P=1 {a} are indeed equivalent to {a}, since {a} is interpreted as the singleton domain element aI in each world. This implies that also X v P>0 {a}, X v P=1 {a} and X v {a} are equivalent. In other words, whenever {a} ∈ S∗G (X, v), then {a} must be in S∗G (X, w) for all w ∈ V . The completions sets S∗G (X, v) and S∗G (X, r, v) are initialized as follows: – S0G (X, 0) = {>, X} and S0G (X, v) = {>} for all v ∈ V \ {0}, – SεG (X, ε) = {>, X} and SεG (X, v) = {>} for all v ∈ V \ {ε}, – S0G (X, r, v) = SεG (X, r, v) = ∅ for all v ∈ V . PR1 If C 0 ∈ S∗G (X, v) and C 0 v D ∈ T , then S∗G (X, v) := S∗G (X, v) ∪ {D} PR2 If C1 , C2 ∈ S∗G (X, v) and C1 u C2 v D ∈ T , then S∗G (X, v) := S∗G (X, v) ∪ {D} PR3 If C 0 ∈ S∗G (X, v) and C 0 v ∃r.D ∈ T , then S∗G (X, r, v) := S∗G (X, r, v) ∪ {D} PR4 If D ∈ S∗G (X, r, v), D0 ∈ Sγ(v) G (D, γ(v)) and ∃r.D0 v E ∈ T , G G then S∗ (X, v) := S∗ (X, v) ∪ {E} ∗2 PR5 If {a} ∈ S∗G1 (X, ∗1 ) ∩ S∗G2 (D, ∗2 ) and G R D, then S∗G1 (X, ∗1 ) := S∗G1 (X, ∗1 ) ∪ {P∗2 D} PR6 If P>0 A ∈ S∗G (X, v), then S∗G (X, P>0 A) := S∗G (X, P>0 A) ∪ {A} PR7 If P=1 A ∈ S∗G (X, 0), then S∗G (X, 1) := S∗G (X, 1) ∪ {A} PR8 If P=1 A ∈ S∗G (X, v), v 6= 0, then S∗G (X, v) := S∗G (X, v) ∪ {A} PR9 If A ∈ S∗G (X, v) and v 6= 0, P>0 A ∈ P0T , then S∗G (X, v 0 ) := S∗G (X, v 0 ) ∪ {P>0 A} G G G PR10 If A ∈ S∗ (X, 1) and P=1 A occurs in T , then S∗ (X, v) := S∗ (X, v) ∪ {P=1 A} G G 0 G 0 PR11 If {a} ∈ S∗ (X, v) then S∗ (X, v ) := S∗ (X, v ) ∪ {{a}} Fig. 3. Completion rules for Prob-ELO01 c These completion sets are then extended by applying the completion rules from Figure 3 exhaustively. The function γ : V → {0, ε} used in rule PR4 is defined by γ(0) = 0, and γ(v) = ε for all v ∈ V \ {0}. The completion rules can be divided into two groups. The rules PR1 to PR5 form the first group and are basically the same as the rules OR1 to OR5 for ELO—they are used to compute all subsumption relationships between concepts inside each world. The next five rules PR6 to PR11 handle probabilistic concepts and therefore propagate derived facts between the different worlds. For example, whenever we have P>0 A in the subsumer set of B, then rule PR6 will push A into the subsumer set of B for the world v = P>0 A, i.e., the world v is a witness of the subsumption. Similarly, whenever P=1 A is in the subsumer set of B for some world v, then rule PR7 and PR10 will push P=1 A into the subsumer sets of B for all other worlds w and rule PR8 will finally put A into the subsumer set of B for each world with non-zero probability (i.e. all worlds except world 0). Rule PR11 distributes nominals in subsumer sets between the worlds in V as explained earlier. This set of completion rules extends the rules given in [13] for Prob-EL01 c in two ways. First, by the rules for nominals (written as completion rules). Second, by rule PR7, which is actually necessary to achieve completeness of the completion algorithm for Prob-EL01 c (without nominals). To see this, consider the following TBox: Tex = {A v P=1 B, B v C, P=1 C v D} Clearly, we have A vTex D, however, without rule PR7, the completion algorithm is stuck with P=1 B ∈ S0 (A, 0) and will never derive B ∈ S0 (A, 1), C ∈ S0 (A, 1), P=1 C ∈ S0 (A, 0) and finally D ∈ S0 (A, 0). Theorem 1. The completion algorithm for Prob-ELO01 c is sound and complete. A detailed proof is given in the appendix (see Lemmas 1 and 2). Also note that the completion algorithm for Prob-ELO01 c still runs in polynomial time, since |BCT |, |Sig(T ) ∩ NC |, |Sig(T ) ∩ NI |, |V |, are all linear in the size of |T | = n. 4.2 Computing the Role-depth Bounded Prob-ELO 01 c -lcs The approach for computing the role-depth bounded Prob-ELO01 c -lcs is similar to the classical case, where we first introduce new concept names for the input concepts, normalize the TBox, apply the completion rules, then we intersect the direct subsumers stored in the completion sets and add the cross-product of the existential restrictions of both concepts. However, in the presence of prob- abilistic concepts, we need to compute also the probabilistic direct subsumers and probabilistic existential restrictions. Therefore, this algorithm computes the cross-product of the existential restrictions three times: for the unconditional concepts, for those concepts with probability 1, and for concepts with non-zero probability. In contrast, we need to compute the intersection of the basic con- cepts only once, since whenever X ∈ S0G (A, v) with v 6= 0, then by completion rule PR9 we have also P>0 X ∈ S0G (A, 0) and similarly, whenever X ∈ S0G (A, 1) then we also have P=1 X ∈ S0G (A, 0) by completion rule PR10. The algorithm to compute the role-depth bounded lcs in Prob-ELO01 c is described in Figure 4. Theorem 2. Let T be a Prob-ELO01 01 c -TBox, C and D be Prob-ELO c -concepts and k be a natural number. Then k-lcs(C, D, T , k) is the role-depth bounded least common subsumer of C and D w.r.t. T and the role-depth k. Correctness of this algorithm for computing the role-depth bounded Prob-ELO01 c - lcs follows from soundness and completeness of the completion rules which are used to generate the underlying completion sets. The full proof can be found in the appendix. As in the crisp case, the resulting k-lcs can have a size exponential in k if computed for n input concepts, but it is still polynomial in the size of the input TBox T . 5 Conclusions In this paper we have studied extensions of the light-weight description logic EL, that include nominals and are capable of handling uncertainty. For the DL Prob-ELO01 c , we have introduced a completion algorithm that generalizes the previously known algorithm for Prob-EL01 c , with correct rules for handling nom- inals, while still retaining the polynomial time complexity of classification. Second, we described how the completion sets saturated by the completion algorithm can be combined to compute (approximations of) the lcs of two con- cepts in DLs with nominals—both for the crisp case in ELO and the probabilistic case in Prob-ELO01 c . In cases where the exact lcs exists, the algorithms compute the exact lcs for a sufficiently large k. The extension of EL+ by nominals, covers (most of) the OWL 2 EL profile, thus combining the algorithms for computing the role-depth bounded lcs in EL+ Procedure k-lcs(C, D, T , k) Input: C, D: Prob-ELO01 01 c -concept descriptions; T : Prob-ELO c -TBox; k ∈ IN Output: k-lcs(C, D): role-depth bounded Prob-ELO01 c -lcs of C, D w.r.t. T and k 1: T 0 := normalize(T ∪ {A ≡ C, B ≡ D}) 2: ST := apply-completion-rules(T 0 ) 3: L := k-lcs-r(A, B, ST , k, A, B) 4: return L Procedure k-lcs-r(X, Y, S, k, A, B) Input: A, B: concept names, X, Y : basic concepts with A R X, B R Y ; S: set of saturated completion sets; k: natural number Output: k-lcs(A, B): role-depth bounded Prob-ELO01 c -lcs of X, Y w.r.t. T and k d 1: CN := E∈S A (X,0)∩S B (Y,0)∩BCT E 0 0 2: if k = 0 then 3: return CN 4: else  l 5: return CN u r∈Sig(T )∩NR l ∃r.k-lcs-r(E, F, S, k−1, A, B) u A (X,r,0)×S B (Y,r,0) (E,F )∈S0 0 l   P=1 ∃r.k-lcs-r(E, F, S, k−1, A, B) u A (X,r,1)×S B (Y,r,1) (E,F )∈S0 0 l   P>0 ∃r.k-lcs-r(E, F, S, k−1, A, B) , (E,F )∈PRA (X,r)×PRB (Y,r) where PRG (X, r) = S0G (X, r, v) S v∈V \{0} Fig. 4. Computation algorithm for role-depth bounded Prob-ELO01 c -lcs. [8] and in ELO presented here allows to compute generalizations in this profile. Similarly, as in case of the lcs, an approximation of the most specific concept (msc) can be computed based on a completion algorithm, see [15]. For DLs with nominals, the completion algorithm given in this paper can be directly used for this, since an ABox can always be absorbed into the TBox in a preprocessing step using these nominals. However, since the msc in the presence of nominals is trivial (msc(a) = a), another target DL should be considered in order to yield an informative version of the msc. Besides the msc, there exist several other non-standard inferences that have been studied for classical DLs and would be of interest in the context of subjec- tive probabilities. One of them is axiom pinpointing, i.e. the task of discovering the precise axioms from a knowledge base that are responsible for a consequence to follow. The use of probabilities introduces a new challenge as seemingly in- nocuous axioms may interact to produce unexpected (and possibly unwanted) consequences. A further study of this problem will be a matter of future work. References 1. M. Ashburner. Gene ontology: Tool for the unification of biology. Nature Genetics, 25:25–29, 2000. 2. F. Baader. Terminological cycles in a description logic with existential restrictions. In G. Gottlob and T. Walsh, editors, Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI-03), pages 319–324. Morgan Kaufmann, 2003. 3. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI-05), Edinburgh, UK, 2005. Morgan-Kaufmann Publishers. 4. F. Baader, R. Küsters, and R. Molitor. Computing least common subsumers in description logics with existential restrictions. In T. Dean, editor, Proc. of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI-99), pages 96–101, Stockholm, Sweden, 1999. Morgan Kaufmann, Los Altos. 5. A. Borgida, T. Walsh, and H. Hirsh. Towards measuring similarity in description logics. In Proc. of the 2005 Description Logic Workshop (DL 2005), volume 147 of CEUR Workshop Proceedings, 2005. 6. S. Brandt and A.-Y. Turhan. Using non-standard inferences in description logics — what does it buy me? In G. Görz, V. Haarslev, C. Lutz, and R. Möller, editors, Proc. of the 2001 Applications of Description Logic Workshop (ADL 2001), num- ber 44 in CEUR Workshop, Vienna, Austria, September 2001. RWTH Aachen. See http://CEUR-WS.org/Vol-44/. 7. C. d’Amato, N. Fanizzi, and F. Esposito. A semantic similarity measure for expres- sive description logics. In Proc. of Convegno Italiano di Logica Computazionale, CILC05, 2005. 8. A. Ecke and A.-Y. Turhan. Role-depth bounded least common subsumers for EL+ and ELI. In Y. Kazakov, D. Lembo, and F. Wolter, editors, Proc. of the 2012 De- scription Logic Workshop (DL 2012), volume 846 of CEUR Workshop Proceedings. CEUR-WS.org, 2012. 9. V. Gutiérrez-Basulto, J. C. Jung, C. Lutz, and L. Schröder. A closer look at the probabilistic description logic prob-EL. In Proceedings of Twenty-Fifth Conference on Artificial Intelligence (AAAI-11), 2011. 10. J. Y. Halpern. An analysis of first-order logics of probability. Artificial Intelligence, 46:311–350, 1990. 11. Y. Kazakov, M. Krötzsch, and F. Simančı́k. Practical reasoning with nominals in the EL family of description logics. In G. Brewka, T. Eiter, and S. A. McIlraith, editors, Proc. of the 12th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-12), pages 264–274. AAAI Press, 2012. 12. K. M. Kudla and M. C. Rallins. Snomed: A controlled vocabulary for computer- based patient records. Journal of the American Health Information Management Association, 69:40–44, 1998. 13. C. Lutz and L. Schröder. Probabilistic description logics for subjective uncertainty. In F. Lin, U. Sattler, and M. Truszczynski, editors, Proc. of the 12th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-10). AAAI Press, 2010. 14. B. Motik, B. Cuenca Grau, I. Horrocks, Z. Wu, A. Fokoue, and C. Lutz. OWL 2 web ontology language profiles. W3C Recommendation, 27 October 2009. http: //www.w3.org/TR/2009/REC-owl2-profiles-20091027/. 15. R. Peñaloza and A.-Y. Turhan. Towards approximative most specific concepts by completion for EL01 with subjective probabilities. In T. Lukasiewicz, R. Peñaloza, and A.-Y. Turhan, editors, Proceedings of the First International Workshop on Uncertainty in Description Logics (UniDL’10), 2010. 16. R. Peñaloza and A.-Y. Turhan. A practical approach for computing generalization inferences in EL. In M. Grobelnik and E. Simperl, editors, Proc. of the 8th European Semantic Web Conf. (ESWC’11), Lecture Notes in Computer Science. Springer, 2011. 17. B. Zarrieß and A.-Y. Turhan. Most specific generalizations w.r.t. general EL- TBoxes. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI’13), Beijing, China, 2013. AAAI Press. To appear. A Omitted Proofs A.1 Correctness of the Classification Algorithm for Prob-ELO 01 c Theorem 1. The completion algorithm for Prob-ELO01 c is sound and complete. We prove each of the claims in the following. Please note that the consequence- driven algorithms for ELO from [11] and also the completion algorithm presented in Section 3 compute subsumption relationships under the assumption that cer- tain concepts have a non-empty interpretation. To indicate the assumption that, say G is not empty, when considering the subsumption relationship between C and D, we write G : C vT D. Lemma 1. The completion algorithm is sound, i.e. C ∈ S∗G (X, v) implies G : P∗ X vT Pv C (1) C ∈ S∗G (X, r, v) implies G : P∗ X vT Pv ∃r.C (2) Proof. We show this by induction on the number of rule applications. It is easy to see that the initial subsumer sets satisfy (1) and (2). Also, after each rule application (1) and (2) will still be satisfied. We will only show (1) for the new completion rules for Prob-ELO01 c , which are not in the original completion algorithm in [13]. For property (2), note that none of these new rules changes the subsumer sets S∗G (X, r, v). PR5 If {a} ∈ S∗G1 (X, ∗1 ) ∩ S∗G2 (D, ∗2 ), then by induction hypothesis we have G : P∗1 X vT {a} and G : P∗2 D vT {a}. Additionally, by definition of R , ∗ G 2 R D implies that if G is not empty, then P∗2 D must be not empty as well. Thus we have G : P∗2 D ≡T {a} and therefore G : P∗1 X v P∗2 D. This means, that the addition of P∗2 D to S∗G1 (X, ∗1 ) still satisfies (1). G PR7 If P=1 A ∈ S∗ (X, 0), then by induction hypothesis G : P∗ X vT P=1 A. Thus the implication A ∈ S∗G (X, 1) ⇒ G : P∗ X vT P=1 A is obviously correct, and we can add A to S∗G (x, 1). G PR11 If {a} ∈ S∗ (X, v), then by induction hypothesis G : P∗ X vT Pv {a}, i.e. for all models I = (∆I , W, (Iw )w∈W , µ) of T and all worlds w ∈ W we have: if G is not empty, then (P∗ X)I,w ⊆ (Pv {a})I,w . Together with (P>0 {a})I,w = {d | ∃v ∈ W : µ(v) > 0 ∧ d ∈ {a}I,v } = {d | ∃v ∈ W : µ(v) > 0 ∧ d = aI } = {aI } = {a}I,w and similarly (P=1 {a})I,w = {a}I,w , this yields: if G is not empty, then 0 (P∗ X)I,w ⊆ {a}I,w = {aI } = {a}I,v for all v 0 ∈ W . Hence it holds that G : P∗ X vT Pv0 {a}. This means, that the addition of {a} to S∗G (X, v 0 ) still satisfies (1). Lemma 2. The completion algorithm is complete, i.e. for a normalized TBox T , G ∈ NC , B ∈ BCT , and r ∈ NR we have G vT B implies B ∈ S0G (G, 0) G vT ∃r.B implies ∃A with A ∈ S0G (G, r, 0) and B ∈ S0G (A, 0) Proof. We assume that B 6∈ S0G (G, 0) (resp. there is no A with A ∈ S0G (G, r, 0) and B ∈ S0G (A, 0)) and construct a model IG of T which shows that G 6vT B (resp. G 6vT ∃r.B). To construct this model, we need the classes of equivalent nominals: [a] = {b ∈ Sig(T ) ∩ NI | {a} ∈ S0G ({b}, 0)}. The domain of the interpretation will contain all nominals (modulo equivalence) and for each world w ∈ V all concepts that are not subsumed by a nominal and can be reached from G or a nominal using the relation R . Let IG = (∆IG , W, (IG,w )w∈W , µ) be the following interpretation: ∆IG := {[a] | a ∈ Sig(T ) ∩ NI } ∪ γ(v) G {(A, v) ∈ Sig(T ) ∩ NC × V | G R A, {a} 6∈ Sγ(v) (A, γ(v))} W := V µ(0) := 0 1 µ(w) := for all w ∈ W \ {0} |W \ {0}| aIG = [a] for all a ∈ Sig(T ) ∩ NI To interpret concept and role names, we also need a bijection πv (w) : W → W for each v ∈ W \ {0} with πv (v) = ε and πv (0) = 0. Moreover, π0 is the identity mapping on W . Then: AIG ,w = {[a] | A ∈ S0G ({a}, w)} ∪ {(B, v) ∈ ∆IG | A ∈ Sγ(v) G (B, πv (w))} rIG ,w = {([a], [b]) ∈ ∆IG ×∆IG | ∃A : A ∈ S0G ({a}, r, w) ∧ {b} ∈ Sγ(w) G (A, γ(w))} ∪ {([a], (A, w)) ∈ ∆IG ×∆IG | A ∈ S0G ({a}, r, w)} ∪ {((B, v), [b]) ∈ ∆IG ×∆IG | ∃A : A ∈ Sγ(v) G (B, r, πv (w)) G ∧ {b} ∈ Sγ(w) (A, γ(w))} ∪ {((B, v), (A, w)) ∈ ∆IG ×∆IG | A ∈ Sγ(v) G (B, r, πv (w))} Before proving that IG is indeed a model of T , we generalize the definition of AIG ,w to probabilistic concepts: G X ∈ Sγ(v) (B, πv (w)) iff (B, v) ∈ X IG ,w for X ∈ BCT , (B, v) ∈ ∆IG (3) X ∈ S0G ({a}, 0) iff [a] ∈ X IG ,w for X ∈ BCT , [a] ∈ ∆ IG (4) To show this, we make a case distinction according to the kind of concept X is. First notice that in (3) X cannot be a nominal, since otherwise B would be subsumed by one and hence not be in the domain ∆IG as we assumed. – If X = >, then (3) and (4) are true by definition of >IG ,w = ∆IG and the fact that > is in each subsumer set. – If X = A ∈ NC , then (3) and (4) are true by definition of AIG ,w . G – If X = P>0 A. For the “⇒” direction, let P>0 A ∈ Sγ(v) (B, πv (w)). By rule PR6, we have A ∈ Sγ(v) (B, P>0 A) and by definition of IG (B, v) ∈ AIG ,u G with πv (u) = P>0 A. By definition of πv and IG this means µ(u) > 0 and thus (B, v) ∈ (P>0 A)IG ,w . For the “⇐” direction, let (B, v) ∈ (P>0 A)IG ,w , i.e. there is u ∈ W \ {0} with (B, v) ∈ AIG ,u . The definition of IG yields G A ∈ Sγ(v) (B, πv (u)) with πv (u) 6= 0 by definition of πv . Then by rule PR9 G P>0 A ∈ Sγ(v) (B, πv (w)). G – If X = P=1 A. For the “⇒” direction, let P=1 A ∈ Sγ(v) (B, πv (w)). By rules G PR7 and PR10 we have P=1 A ∈ Sγ(v) (B, u) for all u ∈ W and by rule PR8 G A ∈ Sγ(v) (B, u) for all u ∈ W \ {0}. Since πv is a bijection on W with πv (0) = 0, this also means A ∈ Sγ(v)G (B, πv (u0 )) for all u0 ∈ W \ {0} and 0 hence by definition of IG , (B, v) ∈ AIG ,u for all u0 ∈ W \ {0}. Finally, the definition of µ then yields (B, v) ∈ (P=1 A)IG ,w . For the “⇐” direction, let (B, v) ∈ (P=1 A)IG ,w , i.e. for all u ∈ W \ {0} we have (B, v) ∈ AIG ,u , especially for u0 with πv (u0 ) = 1. The definition of IG G yields A ∈ Sγ(v) (B, πv (u0 ) = 1) and by rule PR10 P=1 A ∈ Sγ(v) G (B, w0 ) for all w0 ∈ W , especially P=1 A ∈ Sγ(v) G (B, πv (w)). This interpretation IG is indeed a model of T , which we will show using a case distinction on the types of GCIs in T . – C v D ∈ T . Let (B, v) ∈ C IG ,w , then (3) yields C ∈ Sγ(v) G (B, πv (w)) and G by rule PR1 also D ∈ Sγ(v) (B, πv (w)). (3) then yields (B, v) ∈ DIG ,w . Let [a] ∈ C IG ,w , then C ∈ S0G ({a}, 0) by (4) and by rule PR1 it also holds that D ∈ S0G ({a}, 0). (4) then yields [a] ∈ DIG ,w . – C1 u C2 v D ∈ T . Let (B, v) ∈ (C1 u C2 )IG ,w , i.e. by the semantics of u (B, v) ∈ C1IG ,w and (B, v) ∈ C2IG ,w . Then (3) yields C1 , C2 ∈ Sγ(v) G (B, πv (w)), G IG ,w and by rule PR2 D ∈ Sγ(v) (B, πv (w)). (3) then yields (B, v) ∈ D . Let [a] ∈ (C1 u C2 )IG ,w , i.e. [a] ∈ C1IG ,w and [a] ∈ C2IG ,w . We then have C1 , C2 ∈ S0G ({a}, 0) by (4) and by rule PR2 also D ∈ S0G ({a}, 0). (4) then yields [a] ∈ DIG ,w . – C v ∃r.A. Let (B, v) ∈ C IG ,w , then (3) yields C ∈ Sγ(v) G (B, πv (w)) and by rule PR3 A ∈ Sγ(v) (B, r, πv (w)). Then, there are two cases: If (A, w) ∈ ∆IG , G i.e. there is no nominal {b} ∈ Sγ(w) G (A, γ(w)), then the definition of rIG ,w IG ,w yields ((B, v), (A, w)) ∈ r . By the initialization of the completion sets G we also have A ∈ Sγ(w) (A, πw (w)) as γ(w) = πw (w) by definition, and thus (A, w) ∈ AIG ,w . Together with ((B, v), (A, w)) ∈ rIG ,w , this yields (B, v) ∈ (∃r.A)IG ,w . If (A, w) 6∈ ∆IG , then there is a nominal {b} ∈ Sγ(w) G (A, γ(w)) and the defi- IG ,w IG ,w nition of r yields ((B, v), [b]) ∈ r . On the other hand, rule PR11 with G G {b} ∈ Sγ(w) (A, γ(w)) yields also {b} ∈ Sγ(w) (A, 0) and then rule PR5 with γ(w) {b} ∈ S0 ({b}, 0) ∩ Sγ(w) (A, 0) and G R A shows that Pγ(w) A ∈ S0G ({b}, 0) G G and thus A ∈ S0G ({b}, w), i.e. [b] ∈ AIG ,w . Similarly, let [a] ∈ C IG ,w , then (4) yields C ∈ S0G ({a}, 0). By rule PR3 it holds that A ∈ S0G ({a}, r, 0). Again, we have the two cases as before, which can be shown analogously. – ∃r.A v D. Let (B, v) ∈ (∃r.A)IG ,w , i.e. there is an α ∈ ∆IG ,w such that ((B, v), α) ∈ rIG ,w and α ∈ AIG ,w . By definition of IG , there are two cases. If α = (C, w) ∈ ∆IG , then the definitions of AIG ,w and rIG ,w yield G G A ∈ Sγ(w) (C, πw (w)) and C ∈ Sγ(v) (B, r, πv (w)). Since πw (w) = γ(w), and G γ(πv (w)) = γ(w) for all v ∈ V , by rule PR4 we get D ∈ Sγ(v) (B, πv (w)) and IG ,w thus by (3) (B, v) ∈ D . If α = [b] ∈ ∆IG , the definitions of AIG ,w and rIG ,w yield A ∈ S0G ({b}, w) G G and there exists C such that C ∈ Sγ(v) (B, r, πv (w)) and {b} ∈ Sγ(w) (C, γ(w)). Because of {b} ∈ Sγ(w) (C, γ(w)), we have Sγ(w) (C, γ(w)) ⊇ S0G ({b}, w) G G (which can be shown by induction on the number of rule applications to G G the latter), and hence also A ∈ Sγ(w) (C, γ(w)). Since C ∈ Sγ(v) (B, r, πv (w)), πw (w) = γ(w), and γ(πv (w)) = γ(w) for all v ∈ V hold, rule PR4 finally G yields D ∈ Sγ(v) (B, πv (w)) and thus by (3) (B, v) ∈ DIG ,w . Similarly, let [a] ∈ (∃r.A)IG ,w , i.e. there is an α ∈ ∆IG ,w with ([a], α) ∈ rIG ,w and α ∈ AIG ,w . Again, we have the two cases as before, which can be shown analogously. Finally, by the assumption B 6∈ S0G (G, 0) and the definition of IG we have (G, 0) 6∈ B IG ,0 , whereas G ∈ S0G (G, 0) yields (G, 0) ∈ GIG ,0 . Since IG is a model of T , this proves G 6vT B. The second case is similar. If we assume that there exists no concept A with A ∈ S0G (G, r, 0) and B ∈ S0G (A, 0), then by definition of the interpretation IG , there is no element α ∈ ∆IG with ((G, 0), α) ∈ rIG ,0 and α ∈ B IG ,0 . Since IG is a model of T , this shows that G 6vT ∃r.B. A.2 Correctness of the k-lcs Algorithm for Prob-ELO 01 c Lemma 3. Let T be a Prob-ELO01 0 c -TBox, T be the TBox obtained from T by applying the normalization rules, S be the set of completion sets obtained from T 0 , A, B be concept names, X, Y be basic concepts with A R X, B R Y , k be a natural number and L = k-lcs-r(X, Y, S, k, A, B). Then X vT 0 L and Y vT 0 L. Proof. Similar to the crisp case, this lemma can be shown by induction on k for the recursive procedure k-lcs-r. For the case k = 0, the result l L= E E∈S0A (X,0)∩S0B (Y,0)∩BCT of k-lcs-r is a conjunction of (possibly probabilistic) concept names, but no existential restrictions. By soundness of the completion rules, we know that E ∈ S0A (X, 0) ∩ S0B (Y, 0) implies X vT 0 E and Y vT 0 E. Since L contains exactly those conjuncts, we also have X vT 0 L and Y vT 0 L. For the case k > 0, L is a conjunction of (possibly probabilistic) concept names and existential restrictions ∃r.E, P=1 ∃r.E, and P>0 ∃r.E. For the con- cept names, the same argument as for the case k = 0 applies. For existential restrictions of the form ∃r.k-lcs-r(E, F, S, k−1, A, B) with (E, F ) ∈ S0A (X, r, 0) × S0B (Y, r, 0), we know that E ∈ S0A (X, r, 0) implies X vT 0 ∃r.E by soundness of the com- pletion algorithm, and similarly Y vT 0 ∃r.F . Then the induction hypothesis yields E vT 0 L0 and F vT 0 L0 for L0 = k-lcs-r(E, F, S, k−1, A, B) and thus also X vT 0 ∃r.L0 and Y vT 0 ∃r.L0 . Similarly, by soundness we get that E ∈ S0A (X, r, 1) implies X vT 0 P=1 ∃r.E respectively E ∈ PRA (X, r) implies X vT 0 P>0 ∃r.E and by induction hypothesis E vT 0 k-lcs-r(E, F, S, k−1, A, B), thus X vT 0 P=1 ∃r.k-lcs-r(E, F, S, k−1, A, B), respectively X vT 0 P>0 ∃r.k-lcs-r(E, F, S, k−1, A, B). All together, this means X vT 0 L. The case for Y vT 0 L is analogous. Lemma 4. Let T be a Prob-ELO01 0 c -TBox, T be the TBox obtained from T by applying the normalization rules, S be the set of completion sets obtained from T 0 , A, B be concept names, X, Y be basic concepts with A R X, B R Y , k be a natural number and L = k-lcs-r(X, Y, S, k, A, B). Then for each Prob-ELO01 c - concept F with Sig(F) ⊆ Sig(T ) and rd(F ) ≤ k, X vT 0 F and Y vT 0 F imply L vT 0 F . d Proof. By induction on the role-depth rd(F ). Let rd(F ) = 0, i.e. F = E con- tains no existential restrictions. Since X vT 0 F and Y vT 0 F , we also have X vT 0 E and Y vT 0 E for all conjuncts E of F . Then, completeness of the algo- rithm yields that E ∈ S0X (X, 0) and since A R X also E ∈ S0A (X, 0). Similarly, we have E ∈ S0B (Y, 0) for all conjuncts E of F and thus l L= E vT 0 F. E∈S0A (X,0)∩S0B (Y,0)∩BCT If rd(F ) > 0, F may contain two kinds of conjuncts: basic concepts and (possi- bly probabilistic) existential restrictions. The basic concepts in F must appear in L as well by an argument analog to the case rd(F ) = 0. Let ∃r.F 0 be a top-level conjunct of F . Since X vT 0 F and Y vT 0 F , completeness yields that there exists an E ∈ S0A (X, r, 0) such that F 0 ∈ S0A (E, 0) (i.e. E vT 0 F 0 ), and an E 0 ∈ S0B (Y, r, 0) such that F 0 ∈ S0B (E 0 , 0) (i.e. E 0 vT 0 F 0 ). By induc- tion hypothesis, it follows that k-lcs-r(E, E 0 , S, k−1, A, B) vT 0 F 0 , thus L vT 0 ∃r.k-lcs-r(E, E 0 , S, k−1, A, B) vT 0 ∃r.F 0 . The other two cases of probabilistic existential conjuncts P=1 ∃r.F 0 and P>0 ∃r.F 0 of F are similar. Together, this implies L vT 0 F . Together, Lemmata 3 and 4 fulfill all requirements of the role-depth bounded least common subsumer. Thus, the following theorem is a direct consequence of both lemmas and the fact that the k-lcs procedure introduces new concept names A and B for the concepts C and D and then calls the procedure k-lcs-r for these new concept names A and B, using the completion sets of the extended and normalized TBox. Theorem 2. Let T be a Prob-ELO01 01 c -TBox, C and D be Prob-ELO c -concepts and k be a natural number. Then k-lcs(C, D, T , k) is the role-depth bounded least common subsumer of C and D w.r.t. T and the role-depth k.