Soundness Preserving Approximation for TBox Reasoning in R Ren Yuan, Jeff Z. Pan and Yuting Zhao Dept. of Computing Science, University of Aberdeen King’s College, Aberdeen AB24 3FX, UK Abstract. TBox reasoning in description logics is hard. For example, rea- soning in SROIQ (i.e. OWL2-DL) is N2ET-complete; even with R, a fragment of SROIQ supporting ALC GCIs and role chains, the complex- ity of reasoning is 2ET-hard. Although various optimisation tech- niques have been applied, existing tableau-based DL reasoners are still inefficient in dealing with arbitrary GCIs especially when complex role chains present. In this paper, we present a soundness preserving approxi- mation for TBox reasoning in R. The main idea is to convert R ontologies to EL+ with an additional complement table maintaining the complemen- tary relations between named concepts. Since existing benchmarks do not focus on complex GCIs and RIs, we propose a new set of testing ontologies for TBox reasoning in R and our preliminary evaluation shows that a naive implementation of our complement-integrated TBox reasoning algorithm outperforms existing reasoners on most of these ontologies. 1 Introduction The family of the description logics (DL) provides a wide range of formalisms with a trade-off between expressiveness and computational difficulty. TBox reasoning in description logics is hard; e.g., DL SROIQ [6], the adjacent logic of OWL2-DL is N2ET-complete [12]; even with R (following the notation of RIQ in [7]), a fragment of SROIQ supporting ALC GCIs and role chains, the complexity of reasoning is 2ET-hard [12]. This makes up a major obstacle of applying these expressive languages in large scale systems. There are mainly two approaches to providing efficient reasoning services. The first approach investigates sophisticated optimisation techniques for tab- leaux algorithms [5, 8, 9, 11, 22]. Their achievements have been applied in prac- tical DL reasoners such as FaCT++ [21], Pellet [18], Racer [3] and HermiT [17]. One of the major difficulties for tableau algorithms is the high degree of non- determinism introduced by GCIs. Some techniques, such as absorption [11, 22] can reduce GCIs into non-GCIs; however, they are only applicable on some kinds of GCIs. The second approach is based on transformations. Approximations can be seen as some useful transformations. Selman and Kautz [16] propose the idea of finding the least upper bound and most lower bound for the entire knowl- edge base or a concept. In practise, such bounds are usually computed in ei- ther syntactic or semantic way. Syntactic Approximation [2, 4, 15, 19, 23] weaken the ontology into a less expressive DL, while Semantic Approximation [14] ap- ply the idea of Knowledge Compilation [16] to precompute the entailed axioms. However, naive syntactic approximations can not guarantee the quality, i.e., soundness or completeness of reasoning. Semantic approximation requires the reasoning in the source language, which might require significant preprocess- ing time. KAON2 [13] reasoner rewrites SHIQ(D) ontologies into disjunctive datalog programs [10]. It is more dedicated to reasoning with large ABox and the reduction is exponential. We notice that less expressive DLs, such as EL+ can deal with large amount of GCIs of restricted patterns very efficiently and its inference patterns can be partially generalised to more expressive DLs by syntactic manipulation of TBox. In this paper, we present a soundness preserving syntactic approximation for TBox reasoning services of the DL R. More precisely, we syntactically approxi- mate an R TBox to EL+ [1] TBox. Compared with existing works, we propose a new approximation method together with new reasoning algorithms having the following features: 1. It’s a syntax-based approximation, which can be conducted very efficiently. 2. It preserves the complementary relations among concept names with an additional complement table. 3. Soundness-guaranteed TBox reasoning of resulting ontologies can be done in polynomial time. We implemented a prototype of our approach called REL and evaluate its performance on real world benchmarking ontology and a set of automated generated R TBox. Preliminary evaluations show that (1) REL outperforms tableaux based reasoners such as Pellet and FaCT++, and (2) its soundness preserving approximation service provides rather complete results, i.e. with high recall. The rest of the paper is organised as follows: in Section 2 we present our approximation approach with examples; in Section 3 we present a soundness- guaranteed TBox reasoning algorithm for the approximation ontologies; in Sec- tion 4 an evaluation of our prototypical implementation is conducted to com- pare with existing DL reasoners; in Section 5 we summarise our findings and highlight the potential of this study. 2 Approximation Approach In this section, we present our approximation approach by first showing ap- proximation principles with an example, and then formalising these principles into algorithms. 2.1 Principles R supports two types of TBox axioms: general concept inclusion (GCIs) and complex role inclusion (RIs). Because RIs are the same in R and EL+, and they are independent from GCIs, we preserve all the RIs in the approximation. The approximation of the GCIs is mainly about the approximation of concept expressions. In R, a concept is inductively defined by constructs as follows: C := >|⊥|A|¬C|C u D|C t D|∃r.C|∀r.C while in EL+ , a concept is inductively defined by constructs as: C := >|A|C u D|∃r.C where A is an atomic concept, r is a role name. Intuitively, an R construct belongs to one of the following sets: {>, ⊥}, {A, ¬C}, {C u D, C t D}, {∃r.C}, {∀r.C}. It’s easy to observe that the former construct in each set is EL+ -compatible, and the latter is equivalent to some negation of the former, which means for an arbitrary R concept expression, either itself or its complement can be composed by legal EL+ constructs. So we can represent non-EL+ part by replacing its appearance with a concept name and preserve its semantics by adding axioms defining its complement. From these observations we generalise our principles of approximation as follows: 1. Representing non-EL+ parts with new concept names. And, particularly, using a symbol y to represent the unique approximation of ⊥. 2. Maintaining the semantics of non-EL+ concepts by definitions of their com- plements. 3. Using an additional complement table CT to maintain the complementary relations between concept names. 4. Preserving all the RIs. 5. Asserting additional subsumptions in reasoning to recover the semantics of approximated concept expressions. An example is as follows: Example 1. T = {Koala v ∀eat.EucalyptLeave, EucalyptLeave v VegetarianFood, ∀eat.VegetarianFood v Herbivore} Following principle 1, we represent non-EL+ concepts ∀eat.EucalyptLeave and ∀eat.VegetarianFood by new names eatEucalyptLeave and eatVegetarianFood, respectively. Following principle 2, we define neatEucalyptLeave ≡ ∃eat.nEucalyptLeave and neatVegetarianFood ≡ ∃eat.nVegetarianFood to represent the complements of eatEucalyptLeave and eatVegetarianFood respectively. Then recursively, we in- troduce nEucalyptLeave and nVegetarianFood to represent non-EL+ concepts ¬EucalyptLeave and ¬VegetarianFood respectively. Thus the TBox becomes: T 0 = {eatVegetarianFood v Herbivore, Koala v eatEucalyptLeave, EucalyptLeave v VegetarianFood, neatEucalyptLeave ≡ ∃eat.nEucalyptLeave, neatVegetarianFood ≡ ∃eat.nVegetarianFood} Following principle 3, we build CT = {(eatEucalyptLeave, neatEucalyptLeave), (EucalyptLeave, nEucalyptLeave), (eatVegetarianFood, neatVegetarianFood), (VegetarianFood, nVegetarianFood)} Following principle 5, in such a knowledge base, reasoning can infer Koala v Herbivore as follows: EucalyptLeave v VegetarianFood → nVegetarianFood v nEucalyptLeave → neatVegetarianFood v neatEucalyptLeave → eatEucalyptLeave v eatVegetarianFood → Koala v Herbivore. 2.2 Algorithms Given an R TBox T , we first generate a set S(T ) of concept expressions appearing in T as follows: 1. Initialise S(T ) by an {>}. 2. If C is refereed in T, then add C into S(T ). 3. For each C ∈ S(T ), add ¬C into S(T ). 4. For each C ∈ S(T ), if C is a conjunction (disjunction), add all its conjuncts (disjuncts) into S(T ); if C is a existential (universal) restriction, add its filler into S(T ). 5. Go back to 3 and repeat until no more changes can be made. We then assign names to these concepts by a function n which assigns each atomic concept in S(T ) (including >) to itself, and each complex concept expression a unique name that does not appear in S(T ). We  d which assigns each conjunction  further define these names by a function C ≡ Ci ∈ S(T ) in S(T ) an axiom n(C) ≡ n(Ci ), each existential restriction C ≡ ∃r.D in S(T ) an axiom n(C) ≡ ∃r.n(D). With these names and definitions, we approximate T by Algorithm A-1. Its input is an R TBox T . Its output is (AS, CT) with AS an EL+ TBox and CT a set of paired concept names. Algorithm A-1: OntoApprox(T ) 1: AS := ∅ 2: CT := ∅ 3: for each GCI C v D ∈ T do 4: AS := AS ∪ {n(C) v n(D)} 5: end for 6: for each concept C ∈ S(T ) do 7: CT := CT{(n(C), n(¬C)), (n(¬C), n(C))} 8: if C is a conjunction or existential restriction then 9: AS := AS ∪ {d(C)} 10: end if 11: end for 12: for each RI β ∈ T do 13: AS := AS ∪ {β} 14: end for 15: normalise AS This algorithm needs some explanation: – By step-1 and step-2, AS and CT are initialised by empty sets. – Step-4 rewrite the GCI with the named concepts. – Step-7 updates CT. – Step-8 and 9 maintain the definition of some concepts. – Step-13 preserve all the RIs. – Step-15 normalise AS as a classical EL+ ontology [1]. It’s important to point out here that such a normalisation will not introduce any new concept name, because in step-4, all the GCIs have already been approximated into form A v B or A ≡ C, where A, B are concept names and C is either A1 u . . . u An or ∃r.A. After the execution of A-1, AS is a normalised EL+ ontology. For every concept name A ∈ CNAS , there exists B such that (A, B) ∈ CT or (B, A) ∈ CT. The complexity of A-1 is described by the following theorem: Theorem 1. Given an R TBox, T and Nα,T the number of axioms in T , Algorithm A-1 will terminate in O(Nα,T ) time in worst case. Proof. Algorithm A-1 is linearly w.r.t. Nα,T + |S(T )|, where |S(T )| is also linear w.r.t. Nα,T . We call the pair of (AS, CT) an EL+C ontology to indicate that it is an EL+ on- tology plus a complement table. As Algorithm A-1 shows, CT actually contains pairs of complementary named concepts. In the following, for each A appear in (AS, CT), we use CT(A) to represent the complement of A, i.e. (A, CT(A)) ∈ CT. Following Theorem 1 and the algorithms, we immediately know that |AS| = O(Nα,T ) and |CT| = O(Nα,T ). Also, the approximation is additive, which means OntoApprox(T1 ∪ T2 ) = OntoApprox(T1 ) ∪ OntoApprox(T2 ) when any concept expression C has the same n(C) in these three approximations. 3 Soundness-preserving EL+C TBox Reasoning We define entailment in an EL+C ontology O = (AS, CT) as: O |= α iff AS ∪ {A ≡ ¬B|(A, B) ∈ CT} |= α. Given CNAS the set of concept names, RNAS the set of role names, TBox reasoning in O yields, for each C ∈ CNAS , a subsumer set S(C) = {X|O |= C v X}, for each r ∈ RNAS , a relation set R(r) = {(X, Y)|O |= X v ∃r.Y}. 3.1 Completion rules TBox reasoning in AS alone can be done by EL+ classification [1]. However, due to the absence of knowledge maintained by CT, performing EL+ reasoning in AS without considering CT will lose much information. We therefore propose several additional completion rules to capture the semantics of CT and the y as shown in Table 1. R6 realises axiom A u ¬A v ⊥. R7 asserts the reverse subsumption between concepts to supplement the absence of negation. R8 builds up the relations between conjuncts of a conjunction, e.g. A u B v ⊥ implies A v ¬B. R9 deals with ⊥ in existential restrictions, e.g. A v ∃r.⊥ implies A v ⊥. We show the application of some rules with the following example: Table 1. Additional completion rules R6 If A, B ∈ S(X), A = CT(B) and y< S(X) then S(X) := S(X) ∪ {y} R7 If A ∈ S(B) and CT(B) < S(CT(A)) then S(CT(A)) := S(CT(A)) ∪ {CT(B)} R8 If A1 u . . . u Ai u . . . u An vy, A1 , . . . , Ai−1 , Ai+1 , . . . , An ∈ S(X) and CT(Ai ) < S(X) then S(X) := S(X) ∪ {CT(Ai )} R9 If (A, y) ∈ R(r) and y< S(A) then S(A) := S(A) ∪ {y} Example 2. O = {A v ∀r.∃s.B, B v ⊥, ¬C v ∃r.>} Obviously, we can infer A v C from the above TBox. OntoApprox((O)) will yield the following results: AS = {X2 ≡ ∃s.B, X5 ≡ ∃r.X3 , A v X4 , B vy, X8 ≡ ∃r.>, X7 v X8 } and CT = {(B, X1 ), (X1 , B), (X2 , X3 ), (X3 , X2 ), (X4 , X5 ), (X5 , X4 ), (A, X6 ), (X6 , A), (y, >), (>, y), (C, X7 ), (X7 , C), (X8 , X9 ), (X9 , X8 )} Intuitively, A v C can be inferred by reasoning in following steps: 1. X2 ≡ ∃s.B, B vy→ X2 ≡ ∃s. y→R9 X2 vy→R7 > v X3 ; 2. > v X3 , X8 ≡ ∃r.> → X8 v ∃r.X3 ; 3. X8 v ∃r.X3 , X5 ≡ ∃r.X3 → X8 v X5 ; 4. X8 v X5 , X7 v X8 → X7 v X5 →R7 X4 v C; 5. X4 v XC , A v X4 → A v C 3.2 Abstract algorithm The extra completion rules can be considered as introductions of new nor- malised EL+ axioms in addition to AS. For example, R7 introduces a new axiom CT(A) v CT(B) given known subsumption B v A. In the following we propose an abstract algorithm which performs EL+C TBox reasoning by realising the completion rules with incremental reasoning of EL+ [20]. The algorithm computes these sets by processing corresponding axioms. For each name concept or existential restriction appearing on LHS of some axiom, the algorithm maintains a Ô set while for each name concept A, the algorithm maintains a FIFO queue(A). Given a EL+C ontology O = (AS, CT), the algorithm is initialised as follows: 1. ∀C ∈ CNAS , S(C) = {C} ∪ {>}, S(y) = CNAS ; 2. ∀r ∈ RNAS , R(r) = ∅; 3. if A1 u . . . u An v B ∈ AS, then add A1 , . . . , Ai−1 u Ai+1 , . . . , An → B into Ô(Ai ); 4. if A u ∃r.B ∈ AS, then add ∃r.B ∈ into Ô(A); 5. if ∃r.A u B ∈ AS, then add B ∈ into Ô(∃r.A); 6. ∀A ∈ CNAS , queue(A)=Ô(A)∪Ô(>); Then, for all A ∈ CNAS such that y< S(A), Algorithm A-2 is applied to all the entries X ∈queue(A) until no more changes can be made. Algorithm A-2: Process(A, X) 1: if X = B1 , . . . , Bn → B and B < S(A) then 2: if B1 , . . . , Bn ∈ S(A) then 3: AddSubsumer(A,B) 4: end if 5: if y∈ S(B) then 6: for CT(Bi ) < S(A) and B1 , . . . , Bi−1 , Bi+1 . . . , Bn ∈ S(A) do 7: AddSubsumer(A,CT(Bi )) 8: end for 9: end if 10: end if 11: if X = ∃r.B then 12: if y∈ S(B) then 13: AddSubsumer(A, y) 14: else 15: if (A, B) < R(r) then 16: Process-new-edge(A, r, B) 17: end if 18: end if 19: end if The algorithm needs some explanations: – In step-3, Algorithm A-3 is called to add B as a subsumer of A. – Step-5 to Step-9 realise R8. – Step-12 to Step-13 realise R9. – In step-16, Algorithm Process-new-edge in [1] is called. During the execution of Algorithm A-2, Algorithm A-3 is called whenever a new subsumer is found. Its input are the subsumee and subsumer, respectively. Algorithm A-3: AddSubsumer(A,B) 1: S(A) = S(A) ∪ {B} 2: queue(CT(B)) =queue(CT(B)) ∪ {→ CT(A)} 3: Ô(CT(B)) =Ô(CT(B)) ∪ {→ CT(A)} 4: if y< S(B) and CT(B) < S(A) and CT(A) < S(B) then 5: queue(A)=queue(A)∪Ô(B) 6: for all concept names A0 and role name r with (A0 , A) ∈ R(r) do 7: queue(A0 )=queue(A0 )∪Ô(∃r.B) 8: end for 9: else 10: AddSubsumer(A,y) 11: for all concept names A0 and role name r with (A0 , A) ∈ R(r) do 12: AddSubsumer(A0 ,y) 13: end for 14: end if Some explanations of the above algorithm: – Step-2 and step-3 realise R7 with incremental reasoning. The application of R7 will always introduce a new axioms CT(B) v CT(A). Therefore we gen- erate a new entry → CT(A) for Ô(CT(B)) and initialise it into queue(CT(B)) accordingly. – Step-4 checks the condition of R6. Such a condition is important because once we realise that a concept is subsumed by y, we immediately know that it’s subsumed by any concept. – Step-10 to Step-13 realise R6 and R9 Post-processing should be done so that ∀A ∈ CNAS and y∈ S(A), S(A) := CNAS and R(r) := R(r) ∪ {(A, B)} for all r ∈ RNAS and B ∈ CNAS . Also, A ∈ S(>) should be subsumer of all the concept. The complexity of the reasoning is described by the following theorem: Theorem 2. Given an EL+C ontology O = (AS, CT) the computation of the S sets an R sets for all its named concepts and named roles will terminate in polynomial time w.r.t. |CNAS ∪ RNAS |. Proof. The complexity of A-3 immediately follow the polynomial complexity of EL+ classification [1] and incremental reasoning [20]. 3.3 Reasoning Service Given the original ontology O1 and its approximation O2 = OntoApprox(O1 ), we can provide various reasoning services: – The entailment checking of an arbitrary GCI is realised as: O1 |= C v D if O2 |= CApprox(C) v CApprox(D). – The unsatisfiability of an concept expression C can be realised by the en- tailment checking of O1 |=? C v ⊥, which will be reduced to entailment checking O2 |=? CApprox(C) vy. – The inconsistency checking of O1 can be realised by entailment checking O1 |=? > v ⊥. Therefore, the problem of ontology consistency in O1 can also be reduced to entailment checking O2 |=? > vy in O2 . – Incremental reasoning with a temporal ontology Otemp : O1 ∪ Otemp can be approximated into OntoApprox(O1 ∪ Otemp ), which is equivalent to O2 ∪ OntoApprox(Otemp ), whose taxonomy can be computed incrementally by adopting the incremental reasoning algorithm in [20]. The quality of the approximation and the reasoning is guaranteed by the following theorem: Theorem 3. Given an R ontology O1 , approximate it into O2 with Algorithm A-1. For any A, B ∈ CNO1 , O1 |= A v B if B ∈ S(A) can be inferred from O2 by Algorithm A-2. Proof (sketch): It is easy to see the approximation by Algorithm A-1 is an equivalent syntactic transformation, because it is reversible. The completion rules implemented by Algorithm A-2 are obviously soundness-guaranteed. Incompleteness Our extra completion rules process each axiom in AS individ- ually. In Algorithm A-2 we also process each queue entry individually. This helps keeping the reasoning tractable but some information that can only be derived from interaction of multiple entries will be lost: Example 3. T = {A u ¬B v C, A u B v C, D v ∃r.¬C, ∃r.B v E, ∃r.¬A v E} Obviously, we have T |= A v C and thus D v E. However, if we approximate it into ({X1 ≡ A u nB, X2 ≡ A u B, X3 ≡ ∃r.nC, X4 ≡ ∃r.nA, . . .}, {(B, nB), . . .}) and initialise Algorithm A-1, we will have queue(A) = {nB → X1 , B → X2 }. Obviously, B and nB are not subsumers of A thus we can’t further infer C ∈ S(A). This can be solved by resolution: nB → X1 ∈ queue(A) implies A v f c(nB)tX1 thus A v B t C. similarly we have A v nB t C. Together we can infer A v C. In order to further infer D v F. A new axiom ∃r.(B t ¬A) ≡ ∃r.B t ∃r.¬A has to be added into T and approximated for incremental reasoning. Although we can’t guarantee completeness, we will see in next section that the recall is high, at least for our benchmark ontologies. 4 Evaluation We implement our approximation and reasoning algorithm as a functionality of our REL reasoner for EL+ , which is a component of our TrOWL Tractable Reasoning infrastructure of OWL1 . To evaluate its performance, We compare REL with FaCT++ v1.2.3 and Pellet 2.0.0 rc5. The experiments are conducted in an environment of Microsoft Windows XP SP3 with 2.66 GHz CPU and 1G memory allocated to JVM 1.6.0.07. In order to test its effects on difficult TBox with complex GCIs, we create our own set of 16 R ontologies 2 . In these ontologies, the size of any conjunction or disjunction is at most 5, the depth of a concept expression on the lhs or rhs of a GCI is at most 4. The domain and range of any role is a disjunction of depth at most 3. These ontologies are split into two sets, i.e. S1 and S2. In S1, ontologies have increasing number of concept names and GCIs. |RN| is fixed to 10, number of simple RIs and complex RIs are about 10. In S2, ontologies have increasing |RN|. |CN| is fixed to 20, number of GCIs is fixed to 30, number of RIs is increasing with the |RN| . The performance metrics for REL include approximation time, 1 http://trowl.eu/ 2 http://www.abdn.ac.uk/˜csc303/benchmark/RBenchmarkTest.zip reasoning time and completeness. All the time are measured in seconds. To evaluate the completeness, we check the subsumption between each pair of named concepts and count the number of discovered subsumptions. Pellet timed-out or clashed in all the 16 ontologies. Results of REL and FaCT++ are illustrated in Table 2, in which recall is calculated as the ratio of Table 2. Evaluation Results Against FaCT++ S1 |CN| GCIs Tapproximation Treasoning Recall TFaCT++ R1 10 40 0.016 0.047 68.9% 0.797 R2 10 40 0.016 0.031 100% 0.015 R3 10 40 0.031 0.094 N/A - R4 20 40 0.015 0.032 100% 0.578 R5 20 40 0.016 0.047 N/A - R6 20 40 0.016 0.031 100% 3.25 R7 20 40 0.031 0.031 100% 0.437 R8 20 50 0.032 0.078 N/A - R9 20 50 0.031 0.109 N/A - R10 20 50 0.031 0.032 100% 0.61 S2 |RN| Tapproximation Treasoning Recall TFaCT++ R11 100 0.094 1.047 86.7% 1.109 R12 100 0.094 0.875 98.1% 2.907 R13 100 0.078 0.938 87.3% 4.3 R14 300 0.234 7.281 N/A - R15 300 0.319 10.563 100% 2.125 R16 300 0.234 5.969 N/A - subsumptions discovered by REL against those discovered by FaCT++. − means FaCT++ timed-out or run out of memory. As we can see, some ontologies are extremely difficult in contrast to their small size. By looking in depth into the ontologies, we see the differences as: – R2 is quite easy for both REL and FaCT++ because it contains many explicit equivalence between concept names. – R3 has relatively complex domain and range with disjunctions, which are difficult to optimise for tableau algorithms. – R4 and R7 are relatively easy because they are actually shallow ontologies with only a few implicit subsumptions. – R1, R5, R6, R8 and R9 are difficult for FaCT++ because they all have many explicit or implicit A v ∃r.> axioms, which will lead to large expansions for tableau algorithm. – R11, R12 and R13 are actually shallow with a few implicit subsumptions, although the number of roles is not small. In order to evaluate the usability of our approximative reasoning approach on real world ontologies, we test REL on the wine and cyc ontology. More precisely, we first remove all the ABox axioms from these ontologies, and then use Pellet, FaCT++ and REL to classify them. The results are given in Tab.3. In order to justify the complement-integrated reasoning algorithm, we also use a EL+ reasoner to classify the approximated EL+ TBox solely without taking complement table into account. Table 3. Evaluation on Real World Ontology Ontology DL FaCT++ Pellet REL Recall EL+ Recall OWL Guide Wine SHOIN 0.344 1.234* 0.094 96.8% 95.8% Cyc ALCHF 0.422 98.765 4.109 100% 1.2% Comparison shows that, REL can perform efficiently on real world ontolo- gies as well and the recall is rather high (more than 90%). Also the complement- integrated reasoning algorithm can significantly improve the recall on particular ontologies. 5 Conclusion & Future Work In this paper we presented our approach to approximating description logic R into EL+ with an additional complement table. The approximation method we proposed is a syntax-based transformation which is very efficient and preserv- ing the complementary relations. With additional completion rules and abstract algorithms that we proposed, the reasoning of resulted ontology is sound and tractable. Preliminary evaluation results showed that our approach can outper- form existing DL reasoners on some difficult R ontologies. The follow-up of the current work will be the investigation of the com- pleteness and the optimisation of the implementation. Potential extension of this method aims at including more expressiveness for both source and target languages: a more comprehensive approximation from OWL2-DL to OWL2-EL is under investigation. We expect our work to push one step forward to deal- ing with complex GCIs and RIs in very expressive DLs, and to build a bridge between the ALC and EL families of DLs. Acknowledgements This work has been partially supported by the European Project Marrying On- tologies and Software Technologies (MOST ICT 2008-216691). References 1. Franz Baader, Carsten Lutz, and Boontawee Suntisrivaraporn. Is tractable reasoning in extensions of the description logic el useful in practice? In Proceedings of the 2005 International Workshop on Methods for Modalities (M4M-05), 2005. 2. Perry Groot, Heiner Stuckenschmidt, and Holger Wache. Approximating descrip- tion logic classification for semantic web reasoning. In Asunción Gómez-Pérez and Jérôme Euzenat, editors, ESWC, volume 3532 of Lecture Notes in Computer Science, pages 318–332. Springer, 2005. 3. Volker Haarslev and Ralf Möller. RACER system description. In IJCAR ’01: Proceed- ings of the First International Joint Conference on Automated Reasoning, pages 701–706, London, UK, 2001. Springer-Verlag. 4. Pascal Hitzler and Denny Vrandecic. Resolution-based approximate reasoning for owl dl. In Y. Gil et al., editor, Proceedings of the 4th International Semantic Web Conference, Galway, Ireland, November 2005, volume 3729 of Lecture Notes in Computer Science, pages 383–397. Springer, Berlin, NOV 2005. 5. Ian Horrocks. Reasoning with expressive description logics: Theory and practice. In In: Andrei Voronkov, (ed) Proc. 18th Int. Conf. on Automated Deduction (CADE-18), pages 1–15. Springer, 2002. 6. Ian Horrocks, Oliver Kutz, and Ulrike Sattler. The even more irresistible sroiq. In Patrick Doherty, John Mylopoulos, and Christopher A. Welty, editors, KR 2006, pages 57–67. AAAI Press, 2006. 7. Ian Horrocks and Ulrike Sattler. Decidability of shiq with complex role inclusion axioms. Artif. Intell., 160(1):79–104, 2004. 8. Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Practical reasoning for expressive description logics. In LPAR ’99: Proceedings of the 6th International Conference on Logic Programming and Automated Reasoning, pages 161–180, London, UK, 1999. Springer- Verlag. 9. Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Practical reasoning for very ex- pressive description logics. Logic Journal of the IGPL, 8:2000, 2000. 10. Ullrich Hustadt, Boris Motik, and Ulrike Sattler. Reducing shiq-description logic to disjunctive datalog programs. In KR 2004, pages 152–162, 2004. 11. Horrocks I. and Tobies S. Optimisation of terminological reasoning. Technical report, 2000. 12. Yevgeny Kazakov. SRIQ and SROIQ are harder than SHOIQ. In DL 2008, 2008. to appear. 13. B. Motik. Practical dl reasoning over large aboxes with kaon2. 14. Jeff Z. Pan and Edward Thomas. Approximating OWL-DL Ontologies. In the Proc. of the 22nd National Conference on Artificial Intelligence (AAAI-07), pages 1434–1439, 2007. 15. Marco Schaerf and Marco Cadoli. Tractable reasoning via approximation. Artificial Intelligence, 74:249–310, 1995. 16. Bart Selman and Henry Kautz. Knowledge compilation and theory approximation. J. ACM, 43(2):193–224, 1996. 17. Rob Shearer, Boris Motik, and Ian Horrocks. Hermit: A highly-efficient owl reasoner. In Catherine Dolbear, Alan Ruttenberg, and Ulrike Sattler, editors, OWLED 2008, volume 432 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. 18. E Sirin, B Parsia, BC Grau, A Kalyanpur, and Y Katz. Pellet: A practical OWL-DL reasoner. Journal of Web Semantics, 5(2):51–53, June 2007. 19. Heiner Stuckenschmidt and Frank van Harmelen. Approximating terminological queries. In FQAS ’02: Proceedings of the 5th International Conference on Flexible Query Answering Systems, pages 329–343, London, UK, 2002. Springer-Verlag. 20. Boontawee Suntisrivaraporn. Module extraction and incremental classification: A pragmatic approach for EL+ ontologies. In Sean Bechhofer, Manfred Hauswirth, Joerg Hoffmann, and Manolis Koubarakis, editors, Proceedings of the 5th European Semantic Web Conference (ESWC’08), volume 5021 of Lecture Notes in Computer Science, pages 230–244. Springer-Verlag, 2008. 21. D. Tsarkov and I. Horrocks. Fact++ description logic reasoner: System description. In Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006), volume 4130 of Lecture Notes in Artificial Intelligence, pages 292–297. Springer, 2006. 22. Dmitry Tsarkov, Ian Horrocks, and Peter F. Patel-Schneider. Optimizing termino- logical reasoning for expressive description logics. J. Autom. Reason., 39(3):277–316, 2007. 23. Holger Wache, Perry Groot, and Heiner Stuckenschmidt. Scalable instance retrieval for the semantic web by approximation. In Mike Dean, Yuanbo Guo, Woochun Jun, Roland Kaschek, Shonali Krishnaswamy, Zhengxiang Pan, and Quan Z. Sheng, editors, WISE Workshops, volume 3807 of Lecture Notes in Computer Science, pages 245–254. Springer, 2005.