Classi cation is a fundamental reasoning task in ontology design, and there is currently a wide range of reasoners highly optimised for classi cation of SROIQ ontologies. Existing reasoners, however, do not exploit the fact that most of the axioms in many realisti+c+S. RInOtIhQis ontologies are expressed in some lightweight DL, such as EL paper, we propose a novel reasoning technique that allows us to completely classify a large subset of the signature of a SROIQ ontology by relying only on a reasoner for a given lightweight DL. We also show how this information can then be exploited by the fully- edged SROIQ reasoner HermiT to complete the classi cation of the ontology.
Classi cation |the problem of identifying the subsumption relationships between all pairs of atomic concepts occurring in the input ontology| is a fundamental reasoning task in ontology design. The decision problems associated to classi cation, however, have a very high worst-case complexity for expressive DLs; in particular, subsumption w.r.t. an ontology is 2Nexptime-complete for SROIQ [14] |the DL underlying the standard ontology language OWL 2 [5].
Despite these discouraging complexity results, considerable e ort has been devoted to making classi cation feasible in practice. As a result, many reasoning algorithms and optimisation techniques have been developed, and there is currently a wide range of highly-optimised reasoners, such as Pellet [19], FaCT++ [20], RacerPro [9] and HermiT [6], that support classi cation of ontologies written in expressive description logics.
Since individual subsumption tests performed during classi cation can be computationally very expensive, most DL reasoners implement variants of the well-known Enhanced Traversal Algorithm [2], which reduces the number of required subsumption tests. Sophisticated optimisation techniques are also implemented on top of these algorithms to further reduce the number of potentially expensive subsumption tests [10].
A widely implemented technique is the told subsumptions optimisation [10], which provides an inexpensive way of computing subsumption relationships that hold in the input ontology. In typical ontologies, however, most candidate subsumption relationships between atomic concepts will not hold; hence, e ciently identifying and exploiting such non-subsumption relationships becomes critical in practice, and several optimisation techniques have been developed with this goal in mind. In particular, the completely de ned concepts optimisation [21] identi es a fragment of the ontology for which told subsumption provides complete information; furthermore model-merging and other related techniques exploit the computations performed during individual concept satis ability tests to detect non-subsumptions [10, 8, 6]. However, although these techniques have proved e ective in practice, the classi cation of very large ontologies can still require a large number of expensive subsumption tests.
In recent years, there has been a growing interest in so-called lightweight
DLs. The description logic E L++ [
Unfortunately, many ontologies fall outside the E L++ fragment, and so cannot be classi ed using E L++ reasoners. In many cases, however, such ontologies contain only a relatively small number of non E L++ axioms. For example, out of the 219,224 axioms in the latest version of NCI, only 65 are non E L++. Being able to use an E L++ reasoner to e ciently compute most of the subsumptions and non-subsumptions required to classify these ontologies could lead to signi cant improvements in both performance and scalability.
In this paper, we propose a technique where a reasoner for some DL L is used as \black box" by a reasoner for a more expressive logic L0. We focus on the case where L0 is SROIQ, and we present a classi cation algorithm that, given a SROIQ ontology O, proceeds as follows: 1. It computes a signature L Sig(O) and a fragment ML O written in L such that the concepts in L can be completely classi ed using only the axioms in ML; more precisely, L and ML will be such that, for each atomic concept A 2 L and each B 2 Sig(O) [ f>; ?g, we have O j= A v B i ML j= A v B. 2. It classi es ML using an L-reasoner and feeds (in a compact way) the obtained (non-)subsumptions to a SROIQ-reasoner, such as HermiT, that can e ectively exploit this information [6].
Step 1 involves two important technical challenges. First, L should be as large as possible; in particular, for ontologies with only a few non-L axioms, it is reasonable to expect L to contain most of the ontology's signature. Second, ML must be complete for L. Although techniques such as the completely de ned concepts optimisation can be used to identify a complete fragment, these techniques are very restricted; thus, we exploit module extraction techniques [4, 7], which, in addition to giving completeness guarantees, are more generally applicable, more exible, and more robust.
We believe that our results are interesting from both a theoretical and a practical point of view. We show that given a SROIQ ontology O that is not captured by any known polynomial fragment of SROIQ, it is often possible to identify a large subset of Sig(O) such that all subsumers of concepts in w.r.t. O can be computed using a polynomial time classi cation algorithm. From a practical point of view, our rst experiments with a prototype implementation suggest the potential of this approach for optimising classi cation.
This paper is supplemented by an online Appendix containing additional technical details.1 2
We adopt standard DL notation, as well as standard notions of signature,
interpretations, entailment, satis ability and subsumption. We also assume basic
familiarity with the description logics SROIQ [11] and E L++ [
We denote with Sig(O) (respectively, Sig( )) the signature of an ontology O (respectively, of an axiom ). Furthermore, given an ontology O and a DL L SROIQ, we denote with OL the subset of L-axioms in O. 2.1
Intuitively, a module M for an ontology O w.r.t. a signature is an ontology M O such that M entails the same axioms over as O.
This intuition is typically formalised using di erent notions of a conservative extension [16, 4]. In this paper, we de ne modules in terms of a model-theoretic notion of conservative extension.
let Sig(O). We say that O is a model conservative extension of M O w.r.t. if, for every model I = ( I ; I ) of M, there exists a model J = ( J ; J ) of O such that I = J and XI = XJ for every symbol X 2 . De nition 2 (Module). Let O be an ontology and let be a signature. We say that M O is a module in O w.r.t. if O is a model conservative extension of M w.r.t. .
In particular, if M is a module in O w.r.t. , then the following condition holds: for each axiom with Sig( ) , we have M j= i O j= .
The problem of checking whether M is a module in O w.r.t. , however, is already undecidable for E L++ [17], so approximations are typically needed in practice. The following su cient condition for model conservativity is known to work well in practice [4].
De nition 3 (;-locality). Let be a signature and let O be an ontology. An interpretation I is ;-local for if for every atomic concept A 62 and every atomic role R 62 , we have AI = RI = ;. An axiom is ;-local for if I j= for each I that is ;-local for . An ontology O is ;-local for if every axiom in O is ;-local for . 1 http://www.cs.ox.ac.uk/files/4770/ModClassDL12.pdf
Checking ;-locality for SROIQ axioms is, however, a Pspace-complete problem [4]. Since our goal is to optimise classi cation, checking ;-locality might still be too costly. Instead, we will use ?-locality | a well-known su cient syntactic condition for ;-locality which has been successfully used for both ontology reuse and reasoning problems [4, 12, 18, 7].
The precise grammar de ning ?-locality for SROIQ is given for reference in the Appendix, and can also be found in the literature [7, 4]. It su ces to consider that, for each O and , ?-locality implies ;-locality and it can be checked in polynomial time. Furthermore, the following property holds [7, 4]:
w.r.t. 0 for any 0 .
is ?-local w.r.t. a signature , then is ?-local
We can use ?-locality to de ne the notion of a ?-module. The aforementioned properties of ?-locality ensure that, if M is a ?-module w.r.t. in O as de ned next, then it is also a module w.r.t. in O.
if O n M is ?-local for [ Sig(M).
O is a ?-module in O w.r.t.
Clearly, there is a unique smallest ?-module for a given O and (the smallest subset M O s.t. O n M is ?-local for [ Sig(M)). In what follows, we refer to such smallest module as the ?-module in O w.r.t. and we denote it M[O; ].
In addition to being modules as in De nition 2, ?-modules also enjoy an additional property that makes them especially well-suited for optimising ontology classi cation [7].
Proposition 2. Let O be an ontology, let A; B be concepts in Sig(O) [ f>; ?g, let Sig(O) with A 2 , and let M O be a ?-module in O w.r.t. . Then O j= A v B i M j= A v B. 2.2
The reasoner HermiT implements a classi cation algorithm [6] that di ers signi cantly from the standard Enhanced Traversal Algorithm [2] implemented in most other DL reasoners. The key feature of HermiT's classi cation algorithm that makes it especially well-suited for our purposes is that it exploits sets K and P of pairs hA; Bi of atomic concepts representing known subsumptions and possible subsumptions, respectively. These sets are used to reduce the number of required tests during classi cation. Information about non-subsumptions is implicitly stored in these sets (as it would be too costly to store it explicitly), i.e., if A = fhA; Bi j A; B are atomic concept names in Sig(O)g, then A n (K [ P) is the set of known non-subsumptions.
The algorithm works in two clearly distinct phases. In the initialisation phase, sets K and P are given initial values using information obtained from satis ability tests performed on atomic concepts. In the classi cation phase, K is augmented with pairs from P until K contains all the entailed subsumptions and P is empty.
Additional technical details about HermiT's classi cation algorithm are provided in the Appendix. 3
Given a SROIQ ontology O and a description logic L SROIQ, our rst goal is to identify a signature L Sig(O) such that M[O; L] OL. We call any such subset of Sig(O) an L-signature for O. Section 3.1 addresses the problem of identifying as large an L-signature as possible.
We can then use an L-reasoner to compute from M[O; L] complete classi cation information about the atomic concepts in L |by Proposition 2, given any A 2 L and B 2 Sig(O) [ f>; ?g we have O j= A v B i M[O; L] j= A v B.
HermiT's classi cation algorithm needs to be slightly modi ed in order to exploit the information computed by the L-reasoner. In section 3.2 we show how to adapt the initialisation phase to e ciently encode this information into K and P. Additional technical information about our modi cation of HermiT's algorithm (including a proof of correctness) is given in the Appendix. The de nition of ?-module immediately suggests a simple \guess and check" algorithm for computing a (maximal) L-signature for O: consider all subsets
Sig(O) in decreasing size order and, for each of them, check whether M[O; ] is an L-ontology.
Our goal in practice, however, is to optimise classi cation; hence, we propose a more practical algorithm. Although our algorithm is not guaranteed to compute a maximal L-signature, it can be implemented very e ciently and, as shown in the evaluation section, it typically computes large L-signatures, provided that OL is a large enough fragment of O.
We will exploit the fact that every L-signature L must satisfy the following property (?). If (?) does not hold, then M[O; L] will contain some non L-axiom.
Property (?):
O n OL is ?-local w.r.t.
L Example 1. Consider L = E L and the following ontology
Oex = fA v B; 9R:C v D; E v 8S:A; 9R:D v :Bg
Note that the set of L-axioms in Oex is OLex = fA v B; 9R:C v Dg. Furthermore, the signature of OLex, namely 1 = fA; B; C; D; Rg, is not an L-signature for Oex; indeed, the non L-axiom 9R:D v :B is not ?-local w.r.t 1.
In contrast, we have that Oex n OLex = fE v 8S:A; 9R:D v :Bg is ?-local w.r.t. 2 = (Sig(Oex) n Sig(OLex)) = fCg. Furthermore, M[Oex; 2] = ;; hence, 2 is an L-signature for Oex, and we can ensure that Oex 6j= C v X for each atomic concept X 2 Sig(Oex) di erent from C. }
Although Example 1 might suggest that property (?) is also a su cient condition for L to be an L-signature in O, this is unfortunately not the case. Example 2. Consider 3 = fA; C; D; R; Sg; clearly, Oex n OLex is ?-local w.r.t 3 and hence (?) holds for 3. However, 3 is not an L-signature for Oex.
By De nition 4, each axiom in OexnM[Oex; 3] must be ?-local w.r.t. signature 3 [ Sig(M[Oex; 3]) (and not just w.r.t 3). Axiom = A v B is not ?-local w.r.t. 3, so we have 2 M[Oex; 3]. But then, we have B 2 Sig(M[Oex; 3]) and hence the non L-axiom = 9R:D v :B is not ?-local w.r.t. 3 [Sig(M[Oex; 3]).
We can address this problem by reducing 3 to 4 = 3 n fAg. The corresponding ?-module for 4 then becomes M[Oex; 4] = f9R:C v Dg, which is an L-ontology; thus, 4 is an L-signature for Oex. }
Example 2 suggests an algorithm for computing an L-signature for O, which can be intuitively described as follows. 1. Reduce 0 = Sig(O) to a subset 1 of
w.r.t. 1 (thus satisfying (?)). 2. Compute the axioms S1 in M[O; 1] containing symbols not in 1. 3. Reduce 1 to a subset 2 of 1 such that S1 is ?-local w.r.t. 2. 4. Repeat Steps [2-4] until the set of axioms computed in Step 2 is empty. 0 such that S0 = O n OL is ?-local Note that there can be many ways to perform the signature reduction required in Steps 1 and 4. For instance, 2 and 3 in Examples 1 and 2 are both possible reductions of Sig(Oex) in Step 1. These acceptable reductions can be characterised using a function such that, given returns { if S = ;. { a subset 0
and 0 exists. { ; otherwise.
localise : P(Sig(O))
P(O) ! P(Sig(O)) 2 P(Sig(O)) and S 2 P(O) not ?-local w.r.t. , localise( ; S)
such that every axiom in S is ?-local w.r.t. 0 if S 6= ;
Given a particular localise function, Algorithm 1 accepts a SROIQ ontology O and returns either the pair hfalse; ;i or a pair htrue; Li with L Sig(O) an L-signature for Oex. Termination and correctness are granted by Theorem 1.
i (i
0) be de ned by the following construction: (i = 0): (i 1) : 0 = Sig(O)
S0 = O n OL i = localise( i 1; Si 1)
Si = f 2 M[O; i] j Sig( ) 6 ig Let
L := Ti 0 i. Then, the following properties hold: 1. There exists k < jSig(O)j such that either 2. Either
L = ; or M[O; L] Proof. We rst show Claim 1. Suppose i 6= ; for each i 0. A straightforward inductive argument would show that j i for each j > i 0. Furthermore, 0 = Sig(O), so it cannot be the case that j i for each 0 i < j jSig(O)j. Therefore, there must be some k < jSig(O)j such that k+1 = k; by the de nition of localise, this implies that Sk = ;.
We nally show Claim 2. Suppose L 6= ;. It is enough to prove that each 2 O n OL is ?-local w.r.t. L [ Sig(M[O; L]).
First, we are going to see that Sig(M[O; L]) L. According to Claim 1, there exists k < jSig(O)j such that Sk = ;. This implies that, for each axiom 2 M[O; k], we have Sig( ) k. It is easy to see that Sk = ; also implies that j = k for each j > k. Together with the fact that j i for each j > i 0, this implies L = Ti 0 i = k. But then for each 2 M[O; L] = M[O; k] we have Sig( ) k = L, and so Sig(M[O; L]) L.
Now we can just prove that each 2 O n OL is ?-local w.r.t. L. Because L = Ti 0 i 6= ;, in particular it must be the case that 0 6= ;. By de nition of localise, either O n OL = ; |in which case it is immediate that M[O; L] OL| or every axiom in S0 = O n OL is ?-local w.r.t. 1 = localise( 0; S0). Then, by Proposition 1, each 2 O n OL is ?-local w.r.t. L 1. tu
In practice, it is more convenient to use the L-reasoner to classify OL, instead of M[O; L]. Once L has been computed, the following proposition shows that OL provides as much information as M[O; L] about the classi cation of O. Furthermore, in general M[O; L] OL so additional subsumption relationships might be obtained by classifying OL.
atomic concept A 2
L be an L-signature for an ontology O. Then for each L and each B 2 Sig(O) [ f>; ?g we have
O j= A v B i
OL j= A v B Proof. Consider an atomic concept A 2 L and B 2 Sig(O) [ f>; ?g. By monotonicity, because OL O, we know that
O 6j= A v B implies OL 6j= A v B Algorithm 2 L-ModularClassi cation(O) Input: a SROIQ ontology O 1: OL := f 2 O j is an L-axiomg 2: L := L-signature(O) . See Algorithm 1 3: HOL := L-classi cation(OL) 4: H := HermiTclassi cation(OL; HOL ; L) . See Section 3.2 and Appendix
By monotonicity, because M[O; L] OL (by Theorem 1), it is the case that M[O; L] j= A v B implies OL j= A v B. Now M[O; L] is a ?-module in O w.r.t. L, so by Proposition 2, O j= A v B implies M[O; L] j= A v B, and
O j= A v B implies OL j= A v B Therefore, for each atomic concept A 2 L and B 2 Sig(O) [ f>; ?g we have O j= A v B if and only if OL j= A v B, as required. tu 3.2
As mentioned in Section 2.2, HermiT's classi cation algorithm works with (disjoint) sets K and P of known and possible subsumptions, respectively. We next discuss how we can use the information extracted from OL by the L-reasoner in the initialisation of K and P.
Let K0 = fhA; Bi 2 Sig(O) (Sig(O) [ f>; ?g) j OL j= A v Bg be the positive subsumptions extracted from OL by the L-reasoner. We can clearly complement the initialisation of K by simply adding K0 to K.
To improve the initialisation of P, we can simply make sure that no pair hA; Bi 2 L Sig(O) is ever added to P. Indeed, by Proposition 3, if O j= A v B then hA; Bi must already be in K0; otherwise, we must have O 6j= A v B and there is no need to consider the pair hA; Bi as a possible subsumption.
We include in the Appendix a slightly modi ed version of the intialisation algorithm in HermiT that is capable of exploiting the information extracted from OL by the L-reasoner in the way just explained.
Algorithm 2 describes, at an abstract level, how the entire classi cation process can be performed with our modular technique for a particular L SROIQ and a particular function localise. 4
We have implemented our algorithms in Java using the OWL API.2 Our implementation of the localise function is based on the locality module extractor described in [12], which is publicly available.3 2 http : ==owlapi:sourceforge:net= 3 http : ==www:cs:ox:ac:uk=isg=tools=ModuleExtractor
In the implementation of localise, symbols required to make a set of axioms ?-local are selected greedily axiom by axiom. When selecting symbols, we rely on heuristics that try to keep as many roles as possible within L. This is because ontologies contain many more concepts than roles, and each role typically occurs in a large number of axioms; thus, having a role outside L is likely to cause many other symbols to be left outside L.
In our experiments, we have used the ontologies given in Table 1: { SNOMEDt is a modi cation of the well-known SNOMED ontology (v. January 2010), where two axioms containing disjunction have been added (using feedback obtained from SNOMED's developers). { NCI is the latest version of the National Cancer Institute Thesaurus. This ontology contains 65 non E L++ axioms. { FMA-SNOMED is the ontology obtained from the integration of (a fragment of) the Foundational Model of Anatomy (FMA) and (a fragment of) SNOMED using ontology mappings [13]. In this case, all the non E L++ axioms come from FMA.
Our results are summarised in Table 2. The rst two columns in the table ++-signature. The third provide the total size and number of concepts in the E L ++-signature using the column indicates the time required to compute the E L algorithm described in Section 3.1. Finally, the last two columns provide the total classi cation time using (the latest version of) HermiT, and the classi cation time required to complete the classi cation of OL as described in Section 3.2. For convenience of implementation, we have also classi ed OL using HermiT (and this time has not been included in the table); however, the reasoner ELK can classify OL in all cases in just a few seconds (e.g., ELK can classify SNOMED using concurrent classi cation techniques in about 5 seconds [15]).
We can observe that 96% of the symbols in SNOMEDt (and 93% of the symbols in NCI) are included in the E L++-signature; thus, all subsumers of concepts in this signature can be completely determined using an E L++-reasoner. Note, however, that the size of the E L++-signature for FMA-SNOMED is comparatively much smaller. This is due to the structure of FMA, which contains several non E L++ axioms about roles that are widely used in the ontology. For example, the domain of the role hasMass is de ned as a disjunction of very general concepts, such as MaterialThing; since role hasMass is outside the E L++-signature, so will be MaterialThing (and, as a consequence, also the many concepts subsumed by MaterialThing).
Finally, concerning classi cation times, our results suggest the potential of our techniques. Improvements are especially substantial for both SNOMEDt and NCI, where the E L++-signature is very large. 5
In this paper, we have proposed a technique for classifying a SROIQ ontology O by exploiting a reasoner for a fragment L of SROIQ. Our technique allows us to show that the subsumers of many concepts in O can be completely determined using only the L-reasoner. Although our implementation is still at a very prototypical stage, our preliminary experiments show the potential of our approach in practice.
Our work is only very preliminary, and there are many interesting possibilities for future work.
{ Our heuristics for computing an L-signature L are rather naive and there is plenty of room for improvement. For example, it might be possible to explore modular decomposition techniques to compute larger L-signatures [22]. { HermiT's initialisation phase could be further improved to make better use of the information obtained from the L-reasoner. { We are using ?-modules, which provide very strong preservation guarantees (they preserve even models). It would be interesting to devise novel techniques for extracting modules that are more \permissive", in the sense that they only provide preservation guarantees for atomic subsumptions. { Our technique could also be applied to a di erent notion of locality, as long as it satis ed a result analogous to Proposition 2. { It would be interesting to explore ontology rewriting techniques that complement module extraction. For example, we could rewrite O into an L-ontology O0 such that O0 j= O, in which case the classi cation of O0 would provide an \upper bound" to the classi cation of O.
Acknowledgements. This work was supported by the Royal Society, the EU FP7 project SEALS and the EPSRC projects ConDOR, ExODA, and LogMap. 2. Baader, F., Franconi, E., Hollunder, B., Nebel, B., Pro tlich, H.: An empirical analysis of optimization techniques for terminological representation systems. Applied Intelligence 4(2), 109{132 (1994) 3. Baader, F., Lutz, C., Suntisrivaraporn, B.: CEL - a polynomial-time reasoner for life science ontologies. In: Proc. of IJCAR. pp. 287{291 (2006) 4. Cuenca Grau, B., Horrocks, I., Kazakov, Y., Sattler, U.: Modular reuse of ontologies: Theory and practice. JAIR 31, 273{318 (2008) 5. Cuenca Grau, B., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P.F., Sattler,
U.: OWL 2: The next step for OWL. J. Web Semantics (JWS) 6(4), 309{322 (2008) 6. Glimm, B., Horrocks, I., Motik, B., Shearer, R., Stoilos, G.: A novel approach to ontology classi cation. J. of Web Semantics 10(1) (2011) 7. Grau, B.C., Halaschek-Wiener, C., Kazakov, Y., Suntisrivaraporn, B.: Incremental classi cation of description logics ontologies. JAR 44(4), 337{369 (2010) 8. Haarslev, V., Moller, R.: High performance reasoning with very large knowledge bases: A practical case study. In: Proc. IJCAI. pp. 161{168 (2001) 9. Haarslev, V., Moller, R.: Racer system description. In: Proc. of IJCAR. pp. 701{705 (2001) 10. Horrocks, I.: Implementation and optimisation techniques. In: The Description Logic Handbook: Theory, Implementation, and Applications, chap. 9, pp. 306{346 (2003) 11. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc.
of KR. pp. 57{67 (2006) 12. Jimenez-Ruiz, E., Cuenca Grau, B., Schneider, T., Sattler, U., Berlanga, R.: Safe and economic re-use of ontologies: a logic-based methodology and tool support. In: Proc. of ESWC (2008) 13. Jimenez-Ruiz, E., Grau, B.C.: Logmap: Logic-based and scalable ontology matching. In: Proc. of ISWC (2011) 14. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: Proc. of KR. pp.
274{284 (2008) 15. Kazakov, Y., Krotzsch, M., Simanc k, F.: Concurrent classi cation of EL ontologies. In: Proc. of ISWC. vol. 7032 (2011) 16. Lutz, C., Walther, D., Wolter, F.: Conservative extensions in expressive description logics. In: Proc. of IJCAI. pp. 453{458 (2007) 17. Lutz, C., Wolter, F.: Conservative extensions in the lightweight description logic
EL. In: Proc. of CADE-21. vol. 4603 (2007) 18. Sattler, U., Schneider, T., Zakharyaschev, M.: Which kind of module should I extract? In: Proc. of DL (2009) 19. Sirin, E., Parsia, B., Cuenca Grau, B., Kalyanpur, A., Katz, Y.: Pellet: A practical
OWL DL reasoner. J. of Web Semantics 5(2), 51{53 (2007) 20. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description.
In: Proc. of IJCAR. vol. 4130, pp. 292{297 (2006) 21. Tsarkov, D., Horrocks, I., Patel-Schneider, P.: Optimizing terminological reasoning for expressive description logics. JAR 39(3), 277{316 (2007) 22. Vescovo, C.D., Parsia, B., Sattler, U., Schneider, T.: The modular structure of an ontology: Atomic decomposition. In: Proc. of IJCAI. pp. 2232{2237 (2011)