In this paper we investigate the module-theoretic properties of ? and >-reachability modules in terms of inseparability relations for the DL SRIQ. We show that, although these modules are not depleting or self-contained, they share the robustness properties of syntactic locality modules and preserve all justi cations for an entailment.
Modularization plays an important part in the design and maintenance of large
scale ontologies. Modules are loosely de ned as subsets of ontologies that cover
some topic of interest, where the topic of interest is de ned by a set of symbols.
Extracting minimal modules is computationally expensive and even undecidable
for expressive DLs [
Suntisrivaraporn [
In this paper we investigate the module-theoretic properties of reachability modules for the DL SRIQ. We show that these modules are not self-contained or depleting but they are robust under vocabulary restrictions, vocabulary extensions, replacement and joins. By showing that reachability modules preserve all justi cations for entailments, we show that depleting modules are su cient for preserving all justi cations but not necessary.
In Section 2 we give a brief introduction to the DL SRIQ and modularization as de ned by inseparability relations. Section 3 introduces a normal form for SRIQ TBoxes as well as the rules necessary to transform any such TBox to normal form. In Section 4 we introduce both ?- and > reachability modules and investigate all their module theoretic properties in terms of inseperability relations. All proofs of the work presented appears in the accompanying appendix. Lastly in Section 5 we conclude this paper with a short summary of the results. 2
In this section we give a brief introduction to modularization and the DL SRIQ
[
Constructs atomic concept role inverse role universal role role composition top bottom negation conjunction disjunction exist restriction value restriction self restriction atmost restriction atleast restriction Axiom concept inclusion role inclusion re exivity irre exivity disjointness
Syntax Semantics
C CI 2 I ; C 2 NC R RI I I ; R 2 NR R R I = f(y; x) j (x; y) 2 RI g; R 2 NR
U U I = I I R1 : : : Rn f(x; z) j (x; y1) 2 R1I ^ (y1; y2) 2 R2I ^ : : :
^(yn; z) 2 RnI; n 2; Ri 2 NRg > >I = I ? ?I = ; :C (:C)I = I n CI C1 u C2 (C1 u C2)I = C1I \ C2I C1 t C2 (C1 t C2)I = C1I [ C2I 9R:C fx j (9y)[(x; y) 2 RI ^ y 2 CI ]g 8R:C fx j (8y)[(x; y) 2 RI ! y 2 CI ]g 9R:Self fx j (x; x) 2 RI g 6 nR:C fx j #fy j (x; y) 2 RI ^ y 2 CI g 6 ng > nR:C fx j #fy j (x; y) 2 RI ^ y 2 CI g > ng Syntax Semantics
C1 v C2 C1I C2I R1 : : : Rn v Rn+1 (R1 : : : Rn)I RI ; n 1
Ref (R) f(x; x) j x 2 I g RI
Irr(R) f(x; x) j x 2 I g \ RI = ;
Dis(R; S) SI \ RI = ;
Table 1. Syntax and semantics of SRIQ
Module extraction is the process of extracting subsets of axioms from TBoxes
that are self contained with respect to some criteria. These sets of axioms, called
modules, may be used for various purposes such as reuse, optimization and error
pinpointing amongst others [
De nition 1. (Module for the arbitrary DL L) Let L be an arbitrary description language, O an L ontology, and a statement formulated in L. Then, O0 O is a module for if O0 j= .
in O(a -module in O) whenever: O j= if and only
De nition 1 is su ciently general so that any subset of an ontology preserving a statement of interest is considered a module, the entire ontology is therefore a module in itself.
Di erent use cases usually result in di erent notions of what the de nition
and characteristics of a module should be. Modules are often de ned via the
notion of conservative extensions. Given some signature (a set of concept and
role names) and a set of axioms, a conservative extension of this set is simply
one that implies all the same consequences over the signature. More formally:
De nition 2. (Conservative extension [
have T j= i T1 j= . { T is a conservative extension of T1 if T is a for = Sig(T1). with Sig( )
, we -conservative extension of T1
Given that both sets of axioms imply the same consequences for a given signature we may then use the smaller set whenever we wish to reason over this signature. A closely related notion to conservative extensions is that of inseparability.
De nition 3. [
De nition 4. [
{ an S -module of T if M S T . { a self-contained S -module of T if M S { a depleting S -module of T if ; S
[Sig(M) T . [Sig(M) T n M.
Modules may therefore be characterized by some inseparability criteria. It
is of interest how modules de ned this way would behave under di erent use
case scenarios. For this purpose, several properties of inseparability relations [
More formally:
De nition 6. [
Sig(T2) , if T1 S T2 then Ti S T1 [ T2, for i = 1; 2. 3
In this section we introduce a normal form for SRIQ TBoxes. We utilize normalization in order to simplify the de nitions, to ease the understanding of the work that follows, as well as to simplify the presentation of proofs. De nition 7. Given Bi 2 (NC [ f>g), Ci 2 (NC [ f?g), D 2 f9R:B; nR:B; 9R:Self g, with R; S; Ri; Si role names from NR or their inverses and n > 1, a SRIQ TBox T is in normal form if every axiom 2 T is in one of the following forms: 1: B1 u : : : u Bn v C1 t : : : t Cm 3: B1 u : : : u Bn v D 5: R1 v R2 7: Dis(R1; R2) 2: D v C1 t : : : t Cm 4: R1 : : : Rn v Rn+1 6: D1 v D2
In order to normalize a SRIQ TBox T we repeatedly apply the normalization
rules from Table 2. Each application of a rule rewrites an axiom into its equivalent
normal form. It is easy to see that the application of every rule ensures that the
normalized TBox is a conservative extension of the original. We note that the
SRIQ axiom Ref (R) is represented by its equivalent > v 9R:Self and Irr(R)
by 9R:Self v ? [
Example 1. Let 1 = B v :C, and 2 = :A v B. Then, 1 may be normalized by application of rule NR2 to 1N = B u C v ? since :C = :C t ?. 2 may be normalized by application of rule NR1 to 2N = > v B [ A since :A = :A u >.
For the rest of this paper we assume that all TBoxes are in normal form.
Deciding conservative extensions has been shown to be computationally
expensive or even undecidable for relatively inexpressive DLs. Therefore, an
approximation of these modules, based on syntax, called syntactic locality modules [
9R>:Self In the grammar, we have that A?; A> 62 is an atomic concept, R? (resp. S?) is either an atomic role (resp. a simple atomic role) not in or the inverse of an atomic role (resp. of a simple atomic role) not in , C is any concept, R is any role, S is any simple role, and C? 2 Con?( ), C> 2 Con>( ). We also denote by w? a role chain w = R1 : : : Rn such that for some i with 1 i n, we have that Ri is (possibly inverse of ) an atomic role not in . A TBox T is ?-local (>-local) w.r.t. if is ?-local (>-local) w.r.t. for all 2 T .
Algorithm 1 may be used to extract both the minimal ? and >-locality based modules for a signature S.
A variant of ?-syntactic locality modules called ?-reachability based modules
[
T De nition 9. (?-Reachability) Let T be a SRIQ TBox in normal form and
Sig(T ) a signature. The set of ?-reachable names in T w.r.t. , denoted by ?, is de ned inductively as follows: { For every x 2 ( [ f>g) we have x 2 T ?. { For every inclusion axiom ( L v R) 2 T , if Sig( L) y 2 Sig( R) is also in T >.
T
? then every
Algorithm 1 (Module Extraction Algorithm for SRIQ [
It is self-evident from De nition 8 that an axiom is ?-reachable w.r.t exactly when it is not ?-local w.r.t. . Similarly we de ne an axiom to be >-reachable exactly when it is not >-local.
T De nition 10. (>-Reachability) Let T be a SRIQ TBox in normal form and
Sig(T ) a signature. The set of >-reachable names in T w.r.t. , denoted by >, is de ned inductively as follows: { For every x 2 ( [ ?) we have that x 2 T >. { For all inclusion axioms ( L v R) 2 T , if
R = ?, or R is of the form A1 t : : : t An and all Ai 2 T >, or
R has any other form and there exists some x 2 Sig( R) \ then every y 2 Sig( L) is also in T >.
T > Every axiom := L v R such that, R = ?, or R is of the form A1 t : : : t aaSArxineigo(aamnlwRsda)iysa\slldeATnTio>t>2e,-dwreebaTycch>aTal,lbole>rTaa>nnRd-drehfaiaRscsh;cSaaabnlgllyeed.oAtthhleleTra>>xfi-o.orremTmahscehaoanfsbdetithlitetohyfeformaerlmoledxuDislTeitss>f(o-sRrroe;maSTce)ho2axvbeTl2er .
It is easy to show that ?-reachability modules are equivalent to ?-locality modules. However, by the de nition of >-reachability we observe that these are not equivalent to >-locality modules. Example 2. Let T be a TBox such that T = f 1; 2; 3; 4g, with 1 := A v 9r:D1; 2 := B v nr:D2; 3 := 9r:> v C; 4 := D1 v D2 and let = fCg. Then T > = f 1; 2; 3g but the >-locality module for T w.r.t. is f 1; 2; 3; 4g.
The di erence stems from the fact that in 1 and 2 the >-reachability of r does not ensure the >-reachability of D1 and D2 respectively. This occurs because, given an axiom = L v R, >-locality ensure that if is >-local then so are all of the symbols in Sig( ), whereas >-reachability is de ned such that the >-reachability of only guarantees that all symbols of L and only some symbols of R will be >-reachable. Thus >-reachability based modules are at most the size of >-locality modules but in general could be substantially smaller. Similar to ?> -locality modules we note that reachability module extraction may also be alternated until a xpoint is reached. These modules are denoted by T ?> .
In order to investigate the module-theoretic properties of reachability
modules, we follow a similar approach to Sattler et al. [
T2 ?> ?> . > reachability inseparable, denoted by T1 > T2, if T1 ? reachability inseparable, denoted by T1 ? T2, if T1 reachability inseparable, denoted by T1 ?> > = T2 ? = T2 T2, if T1 >; ?; ?> =
Firstly we show that >-reachability modules are subsumption inseparable. Concept inseparability follows as a special case of subsumption inseparability. Lemma 1. Let T be a SRIQ TBox, and Sig(T ) a signature. Then T j= C v D if and only if T > j= C v D for arbitrary SRIQ concept descriptions C and D such that Sig(C) [ Sig(D) .
Corollary 1. Let T be a normalized SRIQ TBox, Sig(T ) a signature and S an inseparability relation from De nitions 3 and 4. Then T > S T . T > is therefore a S -module of T .
We show by way of counter example that T > is not a self-contained or depleting S module of T when T > 6= Sig(T >).
Example 3. Let T be a TBox such that T = f 1 = A v 9r:D1; 2 = B v nr:D2; 3 = 9r:> v C; 4 = D1 v D2g, and let = fCg. Then T > = f 1; 2; 3g, = [ Sig(T >) = fA; B; C; r; D1; D2g =6 T >. But T j= D1 v D2 and T > 6j= D1 v D2. Therefore T > is not a self-contained c -module of T . Similarly, T n T > j= 4 6= ; with = D1; D2 and D1; D2 2 . Therefore, T > is not a depleting c -module of T .
Before investigating the robustness properties of reachability modules we introduce some lemmas to aid us in the proofs that follow. x. In particular T x
. 0 then T x
T x = T1 x.
and xb2e fa>n;s?iggn.aTtuhreen, T(1T1a[ndT2T)2 bxe =SRT1IQx TBoxes with Sig(T1) \ Sig(T2) [ T2 x. Proposition 1. For x 2 f>; ?g, x-reachability is robust under replacement. Proposition 2. For x 2 f>; ?g, x-reachability is robust under vocabulary extensions.
Proposition 3. For x 2 f>; ?g, x-reachability is robust under vocabulary restrictions.
Proposition 4. For x 2 f>; ?g, x-reachability is robust under joins.
Reachability modules therefore share all the robustness properties listed.
However, we have seen that these modules are neither depleting nor self-contained
modules. Amongst other things, the depleting and self-contained nature of
modules are utilised in order to nd all MinAs (justi cations) for an entailment [
We show that although our modules do not share these properties they do contain all MinAs for a given signature.
Theorem 2. Let T be a normalized SRIQ TBox and a signature such that
Sig(T ). Then for arbitrary concept descriptions C; D, such that T j= C v D and Sig(C) [ Sig(D) T > we have that T > contains all MinAs for T j= C v D.
The proof to show that T ?> modules share all the robustness properties
of T > modules follows from the above lemmas and follows the proof for ?>
locality modules by Sattler, et al. [
We have investigated the module-theoretic properties of reachability modules for SRIQ TBoxes. Reachability modules di er from syntactic locality modules in that they are not self-contained or depleting. One application of the self-contained and depleting nature of locality modules is the nding of all justications for entailments. However, in terms of nding justi cations, by showing that reachability modules do preserve all justi cations for entailments, we have shown that these properties are su cient but that they are not necessary.
We did preliminary investigations into the size di erence between locality and reachability modules. We extracted a random sample of 1000 modules from each of the Pizza, Nci, Nap and Xylocopa v4 ontologies. Reachability modules were between 2.5% and 33% smaller than locality modules with an average of 22% reduction in size across all ontologies tested.
Our focus for future research is to do an in-depth empirical evaluation on di erences with respect to size and performance between extracting reachability modules for SRIQ and existing syntactic locality methods. We also plan to extend these results to SROIQ.
Acknowledgments We wish to thank the reviewers for their contributions and insightful comments. This work was partially funded by Project number 247601, Net2: Network for Enabling Networked Knowledge, from the FP7-PEOPLE2009-IRSES call. This work is based upon research supported in part by the National Research Foundation of South Africa (UID 85482, IFR2011032700018).
Theorem 1 Exhaustively applying the rules from Table 2 to any SRIQ TBox T results in a SRIQ TBox T 0 in normal form. The normalization process can be completed in linear time in the number of axioms.
Proof: We show that any SRIQ TBox can be converted to an equivalent normal form as follows: { Step 1 - -elimination: Rule NR11 may be applied at most once for each axiom in the TBox. No other rule introduces new axioms that contain equivalences. Therefore the elimination of all equivalences from the TBox will require linear time and add at most a linear number of axioms. { Step 2 - 8-elimination: Applying rule NR7 to every occurrence of a universal restriction in any axiom, irrespective of order, will result in the elimination of all universal restrictions within that axiom. Nested restrictions are handled recursively as they are removed and inserted into the added axioms as C^. There are a constant number of universal restrictions per axiom and therefore the application of rule NR7 will run in constant time, with each application adding a constant number of new axioms. Therefore eliminating all universal restrictions across all axioms will require linear time and add at most a linear number of new axioms. { Step 3 - 6-elimination: Applying rule NR10 to every occurrence of an atmost restriction in any axiom, irrespective of order, will result in the elimination of all atmost restrictions within that axiom. Nested restrictions are handled recursively as needed. There are a constant number of atmost restrictions per axiom and therefore the application of rule NR10 will run in constant time. Therefore eliminating all atmost restrictions across all axioms will require linear time. { Step 4 - Complex role- ller elimination: At the start of this step there are no universal or at most restrictions. We eliminate all complex role llers by applying rules NR8 and NR9 to all axioms. There are a constant number of complex role llers per axiom, therefore the application of these rules requires constant time per axiom and will add at most a constant number of axioms. Therefore, removing all complex role llers from an ontology by using rules NR8 and NR9 will require at most linear time and add a linear number of new axioms. { Step 5 - :-elimination and u, t-simpli cation: At this step there are no existential restriction or at-least restriction with complex role llers. Given any axiom = ( L v R), in a left to right fashion we apply the rules as follows: 1. Apply rules NR1, NR3, NR6 to L until L consists of an existential restriction, an at-least restriction or the conjunction of concept names. There are a constant number of complex concept description, negations, disjunctions and conjunctions in L, each of these rules either eliminates a negation, removes a complex concept description or eliminates a disjunction. There are a constant number of times each of these operations may be applied. Rules NR3 and NR6 each add a constant number of axioms. Therefore, L can be processed in constant time for each axiom. 2. Apply rules NR2, NR4, NR5 to R until R consists of an existential restriction, an at-least restriction or a disjunction of concept names. There are a constant number of times each of these operations may be applied. Rules NR4 and NR5 each add a constant number of axioms.
Therefore, L can be processed in constant time for each axiom. These rules are applied repeatedly until no further processing may be applied to either L and R. Since each step can be completed in constant time and add at most a constant number of new axioms, normalization can be completed in linear time in the number of axioms with at most a linear increase in the number of axioms. 2 Lemma 1 Let T be a SRIQ TBox, and Sig(T ) a signature. Then T j= C v D if and only if T > j= C v D for arbitrary SRIQ concept descriptions C and D such that Sig(C) [ Sig(D) .
Proof: We have to prove two parts. First: If T > j= C v D then T j= C v D. This follows directly from the fact that T > T and that SRIQ is monotonic.
Conversely, we show that, if T j= C v D then T > j= C v D. Assume the contrary, that is, assume T j= C v D but that T > 6j= C v D. Then there must exist an interpretation I and an individual w 2 I such that I is a model of T > and w 2 CI n DI . Modify I to I0 by setting xI0 := I for all concept names x 2 Sig(T ) n T >, and rI0 := I I for all roles names r 2 Sig(T )n > and leaving everything else unchanged. We show that I0 is a model of T >. For all := L v R, with 2 T >, we have that: { If R is such that Sig( R) T > we have that ( R)I = ( R)I0 since it does not change the interpretation of any symbols. { If R is an existential restriction of the form 9r:A with y 2 Sig( R) n T >, then (y)I0 = I or (y)I0 = I I depending on whether y is a role or concept name. In both cases we have that ( R)I ( R)I0 . { If R is an at-least restriction of the form nr:A with y 2 Sig( R) n T >, then (y)I0 = I or (y)I0 = I I depending on whether y is a role or concept name. In both cases we have that ( R)I ( R)I0 . { If R is of the form 9R:Self with R 2 T > we have that ( R)I = ( R)I0 since it does not change the interpretation of the symbol R. { If is of the form Dis(R; S) then by de nition it is always in T >, thus R; S 2 T >. Therefore, the interpretation of alpha does not change. > and Sig( L) 2 >. Now for every
> and thus
T = ( L v R) 2 T n T In all cases ( L)I = ( L)I0 since 2 T ( L)I0 ( R)I0 . Thus, I0 is a model for T
> we have: { {
R is a concept name and RI0 = R is a role name and RI0 = I
I , or
I , or { R is a disjunction of the form A1 t : : : t An with at least one Ai 62 T >, thus AiI0 = I and RI0 = A1I [ : : : [ I [ : : : [ AIn = I , or { R is an existential restriction 9r:A1, thus rI0 = I I and A1I0 = I so that (9r:A1)I0 = I , or { R is 9r:Self , thus rI0 = I I so that (9r:Self )I0 = I , or { R is an atleast restriction nr:A2, thus rI0 = I I , A2I0 = I and j I j n so that ( nr:A2)I0 = I . This follows from the fact that for any concept description nr:A, j I j j(r:A)I j n for it to be satis able. Since for all cases LI0 RI0 , we conclude that I0 is a model for T . But I and I0 correspond on all symbols y 2 (Sig(D) [ Sig(C)) T > and therefore DI0 = DI and CI0 = CI . Now since CI = CI0 and w 2 CI we have that w 2 CI0 n DI0 and hence T 6j= C v D, contradicting the assumption. 2 and 0 be signatures, x 2 f>; ?g and T a is naontd 0Tisxnroetacharbealec,htahbelne theisn notis nTotx re0arcehaacbhlaeb.le.
Lemma 2 Let be an axiom, SRIQ TBox. Then: 1. Assume that there is some axiom 2 T x such that 62 T 0 x. Therefore, twheishiasvae ctohnattradiicstinoont by0TLexmrmeaach2a.1blseinbcuet that it0. iTshuTs,xTreaxchabTle.0 xB. uAt similar argument is used to show that T x T1 x and T1 x T x. 2. For every T we have that 0 \ Sig( ) . Therefore, from Lemma 2.2 we have that whenever T is not reachable it is also not 0 reachable and we have that T 0 x contains at most all those axioms in T x. Thus, T 0 x T x. 3. L0etreac=habTle.x,Si n0c=e T 0T1xTa1nadnd S2i(gT(T\)T1)S.Aigs(sTu1m) ewe hisaverebaychthabelienbduutctnivoet de nition of x reachability that 0. But by Lemma 2.1 we have that whenever is not 0 reachable then it is also not reachable. Therefore, T x contains at most all those axioms in T1 x. Thus, T x T1 x.
and xbe2afn>s;i?gnga.tTuhree,nT(1Ta1n[dTT22) bxe =SRT1IQx TBoxes with Sig(T1) \ Sig(T2) [ T2 x. Proof: Let M = (T1 [ T2) x, M1 = T1 x, M2 = T2 x. Now T1 T1 [ T2 thus by Lemma 3.3 we have that M1 M. Similarly M2 M and thus M1 [M2 M [ M which gives us M1 [ M2 M. Let 0 = [ T1x [ T2x. To show that M M1 [ M2 we note that, when extracting these modules, the order in which axioms are extracted are irrelevant. We therefore assume that any algorithm rst extracts axioms in M1 [M2 then tests all other axioms for 0T1x[T2 -reachability. Consider any axiom 2 (T1 [ T2) n (M1 [ M2). If 2 T1 then 2 T1 n M1 and stTai2tsxenm\oetSnitgTt(o1x)d[erive,re(taackhe[anbtlehT.2axNt[owixsTpn1rxeo)cto\nSdT1iitxgio([n)Sirge(aTc2h[)a\blTeS1xiwg.e(TTm1h)aunsipbyulaLitmeemptlmhieiass 2.2 we have that is not [ T2 [ T1x reachable. The case where 2 T2 is treated analogously. 2 Proposition 1 For x 2 f>; ?g, x-reachability is robust under replacement. Proof: Let Sig(T ) \ (Sig(T1) [ Sig(T2)) Sig(Ti) , for i = 1; 2. Now we have: . This implies that Sig(T ) \ (T [ T1) x == TT2 xx[ T1 xx ((LPermecmonad4it)ion)
= (T2 [ T[ )T x (Lemma 4) 2 Proposition 2 For x 2 f>; ?g, x-reachability is robust under vocabulary extensions.
Proof: Let 0 \ (Sig(T1) [ Sig(T2)) 00 = \ 0 (which implies 00 and T1 and 00 x T2 i.e., T1 x = T2 x. Let 0). Then we have that: T1 0x = T1 0x0( ) = (T1 x) 0x0 (Lemma 3.1) = (T2 x) 0x0 (Precondition) = T2 0x0 (Lemma 3.1) = T2 0x( ) As for equality ( ), set inclusion is due to 0 \ Sig(T1) = 00 and the combination of Lemma 3.2 and Lemma 3.3, and the converse is due to 00 0 and Lemma 3.1. Equality ( ) is justi ed analogously. 2 Proposition 3 For x 2 f>; ?g, x-reachability is robust under vocabulary restrictions.
Proof: Follows from the fact that we have robustness under vocabulary extensions. 2 Proposition 4 For x 2 f>; ?g, x-reachability is robust under joins. Proof: For i = 1; 2, let Mi = Ti x with Sig(T1) \ Sig(T2) , and let M = (T1 [ T2) x. The precondition says that M1 = M2 . It is clear from Lemma 3.3 that M Mi. It su ces to show M M1. Take any axiom cas2e (T12[TT12)nnMM1,1.thItenremaisinnsotto shMowx1 rtehaacthablies nsiontce M[ 1 M=x1Tr1eaxch.aIbnlec.aIsne 2 T2 n M1, we also have that 2 T2 n M2 because M1 = M2. This means that is not [ Mx2 reachable therefore not [ Mx1 reachable. 2 Theorem 2 Let T be a normalized SRIQ TBox and a signature such that
Sig(T ). For arbitrary concept descriptions C; D such that T j= C v D and Sig(C) [ Sig(D) T > we have that T > contains all MinAs for T j= C v D. Proof: Assume that T j= C v D for some Sig(C) [ Sig(D) T >, but there is a MinA M for T j= C v D that is not contained in T >. If C v D is a tautology then M must be empty with M T >. Thus, we assume that C v D is not a tautology. Since M 6 T >, there must be an axiom 2 M n T >. De ne M1 := M \ T >. M1 is a strict subset of M since 62 M1. There are two cases, either M1 = ; or it contains at least one axiom.
In the case where M1 = ;, de ne T1 = T n T > with M T1. Now since M j= C v D we have by monotinocity that T1 j= C v D. Since T1 T we have by Lemma 3.3 that T1 > T > and thus that T1 > = ;. But by Lemma 1 we have that T1 > j= C v D if, and only if, T1 j= C v D. Since C v D is not a tautology we have that T1 > 6j= C v D and thus that M 6j= C v D.
In the case where M1 6= ; we claim that M1 j= C v D, which contradicts the fact that M is a MinA for T j= C v D.
We use proof by contraposition to show this. Assume that M1 6j= C v D, i.e., there is a model I1 of M1 such that CI1 6 DI1 . We modify I1 to I by setting yI := I1 for all concept names y 2 Sig(T ) n T >, and rI := I1 I1 for all rCoIles=nCamI1essinrc2eSSiigg((CT)) n TT >>.. IWt efohllaovwes DthIat=CDI I61 DsinIc.eItSriegm( Dai)ns to bTe>sh,oawnnd that I is indeed a model of M, and therefore satis es all axioms = ( L v R) i(n )MI=,in(cl)uId1i.nOg th.eIrfwise=tDheirse(Rarre; Rtw2)o tphoesnsibbyilidtieesn:ition Sig( ) T > so that { {
Therefore I is a model for M. But since CI 6 proving the contrapositive.
DI we have that M 6j= C v D
2