Completion-based algorithms can be employed for computing 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 subjective probabilities. In this paper we extend the completion-based lcscomputation algorithm to nominals, yielding a procedure for the DL Prob-ELOc01.
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 [
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 [
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 [
?? 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 variant 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-E L [
Obese v P≥0.9∃hasCondition.HighPressure.
A completion algorithm for classifying TBoxes in the sublanguage Prob-E Lc01 of
Prob-E L was described in [
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
maximal nesting of quantifiers of the resulting concept descriptions. These
approximations, called role-depth bounded lcs (k-lcs), can be computed for EL with role
inclusions by using completion sets produced by the completion-based
classification algorithm [
In this paper, we give a classification algorithm for the classic DL ELO
introduced in [
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-E LOc01 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
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, 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 [
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
completionbased classification algorithms for the corresponding DL. For ELO, a
consequencebased classification algorithm is given by Kazakov et al. in [
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 [
Definition 2 ( R). Let T be an ELO-TBox in normal form, G ∈ NC a concept name, and D ∈ BCT . G RD 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 existential restrictions leading to D that starts either with G or with a nominal. This implies that, for G RD, 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 SG(A) and SG(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 SG(A)
for A ∈ BCT therefore stores all basic concepts that subsume A under the
assumption that G is not empty. Similarly SG(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 SG(A) = {A, >} and SG(A, r) = ∅. The completion sets are
then extended by applying the completion rules adapted from [
It can be shown that the algorithm terminates in polynomial time, and is
sound and complete for classifying the TBox T [
Proposition 1 ([
then SG(A) := SG(A) ∪ {B} OR3 If A1 ∈ SG(A), A1 v ∃r.B ∈ T and B 6∈ SG(A, r),
then SG(A, r) := SG(A, r) ∪ {B} OR4 If B ∈ SG(A, r), B1 ∈ SG(B), ∃r.B1 v C ∈ T and C 6∈ SG(A),
then SG(A) := SG(A) ∪ {C}
OR5 If {a} ∈ SG(A1) ∩ SG(A2), G RA2, and A2 ∈/ SG(A1),
then SG(A1) := SG(A1) ∪ {A2}
C vT D iff D ∈ SG(C), and
C vT ∃r.D iff there exists E ∈ BCT such that E ∈ SG(C, r) and D ∈ SG(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.
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 [
An algorithm that computes the role-depth bounded ELO-lcs using completion 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 SA(A) and SB(B). For every role name r, the algorithm then recursively computes the (k−1)-lcs of the concepts A0 and B0 in the subsumer sets SA(A, r) and SB(B, r), i.e. for which A vT ∃r.A0 and B vT ∃r.B0. 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 [
Notice, that for every pair (A0, B0) of r-successors of A and B it holds that A RA0 and B RB0. 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.B0 to be not empty, either. Thus, it suffices to consider the completion sets SA(. . .)
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 RX, B
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 := SA(X) ∩ SB(Y ) ∩ BCT 2: if k = 0 then 3: return l P RY ; k ∈ IN; 4: else 5: return l P u
P ∈CN
l P ∈CN and SB(. . .), without the need to additionally compute SA0 (. . .) and SB0 (. . .), or the completion sets SE (. . .) 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-E LOc01 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 situations where a degree of uncertainty is unavoidable. This is often the case in the medical and biological domains, where knowledge is obtained through clinical 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-E L was introduced by [
P.q C and ∃P.q r.C,
where r ∈ NR, . ∈ {>, <, ≥, ≤, =}, and q ∈ [
The semantics of this logic generalizes the semantics of classical ELO by
considering a set of possible worlds, corresponding to a formalization of subjective
(or Type 2) probabilities [
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: pdI (A) := μ({w ∈ W | d ∈ AIw }), pdI,e(r) := μ({w ∈ W | (d, e) ∈ rIw }).
The functions Iw and pdI are extended to general concepts through the following mutual recursion.
>Iw = ΔI ,
(∃r.C)Iw = {d ∈ ΔI | ∃e ∈ CIw .(d, e) ∈ rIw }, (C u D)Iw = CIw ∩ DIw ,
(P.q C)Iw = {d ∈ ΔI | pdI (C) . q }, ({o})Iw = {oIw },
(∃P.q r.C)Iw = {d ∈ ΔI | ∃e ∈ CIw .pdI,e(r) . q }, pdI (C) = μ({w ∈ W | d ∈ CIw }).
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 CIw ⊆ 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
reasoning, and deciding subsumption becomes intractable. In fact, as shown in [
The basic idea of the completion algorithm for Prob-E LOc01 is the same as in the crisp case: to construct a canonical model of the given TBox. In order to introduce it, we need to extend the notion of basic concepts to the new constructors
BCT = (Sig(T ) ∩ (NC ∪ NI )) ∪ {>} ∪ {P>0A, P=1A | A ∈ Sig(T ) ∩ NC }. Since probabilistic interpretations contain a set of worlds, the completion algorithm has to work on sets of completion sets: one for each world and, since Prob-E LOc01 also contains nominals, for each basic concept. Let P0T denote the set of all probabilistic concepts of the form P>0A appearing in T . The completion algorithm uses a set of worlds V := {0, 1, ε} ∪ P0T ; this way, for each GCI B v P>0A ∈ T the world v = P>0A serves as witness for this subsumptoironS.∗GT(hXe,rre,fovr)e,wthheerePrXob-isE LaOcc0o1ncceopmtpnleatmioen, s>et,s oarreannoowmoinfathl,evfo∈rmVS,∗GG(Xis,va) concept name or >, ∗ ∈ {0, ε} and r is a role name. The completion sets contain basic concepts from BCT . The normal form for Prob-E LOc01-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-E LOc01-concepts extends the one for ELO in distinguishing between concept names X and probabilistic concepts P>0X. For example, non-emptiness of G does not imply non-emptiness of P>0X, even if G RX, e.g. in worlds with probability 0. Similarly, non-emptiness of G does not imply non-emptiness of X for G RP>0X. Therefore we introduce two kinds of reachability relation, G 0 RX for G RX and G ε RX for G RP>0X: Definition 3 (Reachability of Prob-E LOc01-concept descriptions). Let T be a Prob-E LOc01-TBox in normal form, G ∈ NC ∪ {>}, and D ∈ NC ∪ NI . G 0 RD 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.
G ε RD iff G 0 RX, P>0Y ∈ 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.
When it is clear from the context which relation 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} ∈ SG(X, v), then {a} must be in ∗ SG(X, w) for all w ∈ V .
∗
The completions sets SG(X, v) and SG(X, r, v) are initialized as follows: ∗ ∗ 0 R or ε R we are using, we – 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 C0 ∈ S∗G(X, v) and C0 v D ∈ T , then S∗G(X, v) := S∗G(X, v) ∪ {D}
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>0A in the subsumer set of B, then rule PR6 will push A into the subsumer set of B for the world v = P>0A, i.e., the world v is a witness of the subsumption. Similarly, whenever P=1A is in the subsumer set of B for some world v, then rule PR7 and PR10 will push P=1A 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 [
Tex = {A v P=1B,
B v C, P=1C v D} Clearly, we have A vTex D, however, without rule PR7, the completion algorithm is stuck with P=1B ∈ S0(A, 0) and will never derive B ∈ S0(A, 1), C ∈ S0(A, 1), P=1C ∈ S0(A, 0) and finally D ∈ S0(A, 0). A detailed proof is given in the appendix (see Lemmas 1 and 2). Also note that the completion algorithm for Prob-E LOc01 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-ELOc01-lcs The approach for computing the role-depth bounded Prob-E LOc01-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 probabilistic 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 concepts only once, since whenever X ∈ S0G(A, v) with v 6= 0, then by completion rule PR9 we have also P>0X ∈ S0G(A, 0) and similarly, whenever X ∈ S0G(A, 1) then we also have P=1X ∈ S0G(A, 0) by completion rule PR10. The algorithm to compute the role-depth bounded lcs in Prob-E LOc01 is described in Figure 4. Theorem 2. Let T be a Prob-E LOc01-TBox, C and D be Prob-E LOc01-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-E LOc01lcs 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
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-E LOc01, we have introduced a completion algorithm that generalizes the previously known algorithm for Prob-E Lc01, with correct rules for handling nominals, 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 concepts in DLs with nominals—both for the crisp case in ELO and the probabilistic case in Prob-E LOc01. 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+
Input: C, D: Prob-ELOc01-concept descriptions; T : Prob-ELOc01-TBox; k ∈ IN Output: k-lcs(C, D): role-depth bounded Prob-ELOc01-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 RX, B RY ;
S: set of saturated completion sets; k: natural number Output: k-lcs(A, B): role-depth bounded Prob-ELOc01-lcs of X, Y w.r.t. T and k 1: CN := dE∈S0A(X,0)∩S0B(Y,0)∩BCT E 2: if k = 0 then 3: return CN 4: else 5: return CN u
(E,F )∈PRA(X,r)×PRB(Y,r) where PRG(X, r) = Sv∈V \{0} S0G(X, r, v)
Fig. 4. Computation algorithm for role-depth bounded Prob-ELOc01-lcs.
[
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 subjective 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 innocuous axioms may interact to produce unexpected (and possibly unwanted) consequences. A further study of this problem will be a matter of future work.
l and A.-Y. Turhan, editors, Proceedings of the First International Workshop on Uncertainty in Description Logics (UniDL’10), 2010. 16. R. Pen˜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 ELTBoxes. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI’13), Beijing, China, 2013. AAAI Press. To appear.
Correctness of the Classification Algorithm for Prob-ELOc01
Theorem 1. The completion algorithm for Prob-ELOc01 is sound and complete.
We prove each of the claims in the following. Please note that the
consequencedriven algorithms for ELO from [
Lemma 1. The completion algorithm is sound, i.e.
C ∈ S∗G(X, v) implies G : P∗X vT PvC
C ∈ S∗G(X, r, v) implies G : P∗X vT Pv∃r.C
(1)
(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-ELOc01, which are not in the original completion
algorithm in [
∗ PR5 If {a} ∈ S∗G1 (X, ∗1) ∩ S∗G2 (D, ∗2), then by induction hypothesis we have GG ∗:2P∗1 X vT {a} and G : P∗2 D vT {a}. Additionally, by definition of R,
RD 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). PR7 If P=1A ∈ S∗G(X, 0), then by induction hypothesis G : P∗X vT P=1A.
Thus the implication A ∈ S∗G(X, 1) ⇒ G : P∗X vT P=1A is obviously correct, and we can add A to SG(x, 1).
∗ PR11 If {a} ∈ S∗G(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 (P∗X)I,w ⊆ {a}I,w = {aI} = {a}I,v0 for all v0 ∈ W . Hence it holds that G : P∗X vT Pv0 {a}. This means, that the addition of {a} to S∗G(X, v0) 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 } ∪ {(A, v) ∈ Sig(T ) ∩ NC × V | G γ(v)
R A, {a} 6∈ SγG(v)(A, γ(v))}
W := V μ(0) := 0 μ(w) :=
1 |W \ {0}| aIG = [a] for all w ∈ W \ {0} 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γG(v)(B, πv(w))} rIG,w = {([a], [b]) ∈ ΔIG ×ΔIG | ∃A : A ∈ S0G({a}, r, w) ∧ {b} ∈ SγG(w)(A, γ(w))} ∪ {([a], (A, w)) ∈ ΔIG ×ΔIG | A ∈ S0G({a}, r, w)} ∪ {((B, v), [b]) ∈ ΔIG ×ΔIG | ∃A : A ∈ SγG(v)(B, r, πv(w))
∧ {b} ∈ SγG(w)(A, γ(w))} ∪ {((B, v), (A, w)) ∈ ΔIG ×ΔIG | A ∈ SγG(v)(B, r, πv(w))} Before proving that IG is indeed a model of T , we generalize the definition of AIG,w to probabilistic concepts:
X ∈ SγG(v)(B, πv(w)) iff (B, v) ∈ XIG,w
X ∈ S0G({a}, 0) iff [a] ∈ XIG,w for X ∈ BCT , (B, v) ∈ ΔIG for X ∈ BCT , [a] ∈ ΔIG (3) (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. – If X = P>0A. For the “⇒” direction, let P>0A ∈ SγG(v)(B, πv(w)). By rule PR6, we have A ∈ SγG(v)(B, P>0A) and by definition of IG (B, v) ∈ AIG,u with πv(u) = P>0A. By definition of πv and IG this means μ(u) > 0 and thus (B, v) ∈ (P>0A)IG,w. For the “⇐” direction, let (B, v) ∈ (P>0A)IG,w, i.e. there is u ∈ W \ {0} with (B, v) ∈ AIG,u. The definition of IG yields A ∈ SγG(v)(B, πv(u)) with πv(u) 6= 0 by definition of πv. Then by rule PR9 P>0A ∈ SγG(v)(B, πv(w)). – If X = P=1A. For the “⇒” direction, let P=1A ∈ SγG(v)(B, πv(w)). By rules PR7 and PR10 we have P=1A ∈ SγG(v)(B, u) for all u ∈ W and by rule PR8 A ∈ SγG(v)(B, u) for all u ∈ W \ {0}. Since πv is a bijection on W with πv(0) = 0, this also means A ∈ SγG(v)(B, πv(u0)) for all u0 ∈ W \ {0} and w0 ∈ W , especially P=1A ∈ SγG(v)(B, πv(w)). hence by definition of IG, (B, v) ∈ AIG,u0 for all u0 ∈ W \ {0}. Finally, the definition of μ then yields (B, v) ∈ (P=1A)IG,w.
For the “⇐” direction, let (B, v) ∈ (P=1A)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 yields A ∈ SγG(v)(B, πv(u0) = 1) and by rule PR10 P=1A ∈ SγG(v)(B, w0) for all 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) ∈ CIG,w, then (3) yields C ∈ SγG(v)(B, πv(w)) and by rule PR1 also D ∈ SγG(v)(B, πv(w)). (3) then yields (B, v) ∈ DIG,w. Let [a] ∈ CIG,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γG(v)(B, πv(w)), and by rule PR2 D ∈ SγG(v)(B, πv(w)). (3) then yields (B, v) ∈ DIG,w. 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) ∈ CIG,w, then (3) yields C ∈ SγG(v)(B, πv(w)) and by rule PR3 A ∈ SγG(v)(B, r, πv(w)). Then, there are two cases: If (A, w) ∈ ΔIG , i.e. there is no nominal {b} ∈ SγG(w)(A, γ(w)), then the definition of rIG,w yields ((B, v), (A, w)) ∈ rIG,w. By the initialization of the completion sets we also have A ∈ SγG(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γG(w)(A, γ(w)) and the definition of rIG,w yields ((B, v), [b]) ∈ rIG,w. On the other hand, rule PR11 with {b} ∈ SγG(w)(A, γ(w)) yields also {b}γ(∈w)SγG(w)(A, 0) and then rule PR5 with {b} ∈ S0G({b}, 0) ∩ SγG(w)(A, 0) and G R A shows that Pγ(w)A ∈ S0G({b}, 0) and thus A ∈ S0G({b}, w), i.e. [b] ∈ AIG,w.
Similarly, let [a] ∈ CIG,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 A ∈ SγG(w)(C, πw(w)) and C ∈ SγG(v)(B, r, πv(w)). Since πw(w) = γ(w), and γ(πv(w)) = γ(w) for all v ∈ V , by rule PR4 we get D ∈ SγG(v)(B, πv(w)) and thus by (3) (B, v) ∈ DIG,w.
If α = [b] ∈ ΔIG , the definitions of AIG,w and rIG,w yield A ∈ S0G({b}, w) and there exists C such that C ∈ SγG(v)(B, r, πv(w)) and {b} ∈ SγG(w)(C, γ(w)). Because of {b} ∈ SγG(w)(C, γ(w)), we have SγG(w)(C, γ(w)) ⊇ S0G({b}, w) (which can be shown by induction on the number of rule applications to the latter), and hence also A ∈ SγG(w)(C, γ(w)). Since C ∈ SγG(v)(B, r, πv(w)), πw(w) = γ(w), and γ(πv(w)) = γ(w) for all v ∈ V hold, rule PR4 finally yields D ∈ SγG(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∈ BIG,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 α ∈ BIG,0. Since IG is a model of T , this shows that G 6vT ∃r.B.
A.2
Lemma 3. Let T be a Prob-ELOc01-TBox, T 0 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 RX, B RY , 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∈S0A(X,0)∩S0B(Y,0)∩BCT
E 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 concept 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 completion 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-E LOc01-TBox, T 0 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 RX, B RY , k be a natural number and L = k-lcs-r(X, Y, S, k, A, B). Then for each Prob-E LOc01concept F with Sig(F) ⊆ Sig(T ) and rd(F ) ≤ k, X vT 0 F and Y vT 0 F imply L vT 0 F .
Proof. By induction on the role-depth rd(F ). Let rd(F ) = 0, i.e. F = d E contains 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 algorithm yields that E ∈ S0X (X, 0) and since A RX also E ∈ S0A(X, 0). Similarly, we have E ∈ S0B(Y, 0) for all conjuncts E of F and thus
L =
l E∈S0A(X,0)∩S0B(Y,0)∩BCT
E vT 0 F.
If rd(F ) > 0, F may contain two kinds of conjuncts: basic concepts and (possibly 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 that there exists an E ∈ S0A(X, r, 0) such that F 0 v∈TS0 0AF( E,,c0o)m(pi.lee.teEnevssT y0iFeld0)s, and an E0 ∈ S0B(Y, r, 0) such that F 0 ∈ S0B(E0, 0) (i.e. E0 vT 0 F 0). By induction hypothesis, it follows that k-lcs-r(E, E0, S, k−1, A, B) vT 0 F 0, thus L vT 0 ∃r.k-lcs-r(E, E0, 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-ELOc01-TBox, C and D be Prob-ELOc01-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.