MORe exploits module extraction techniques to divide the workload of ontology classi cation between two reasoners: a reasoner for the lightweight pro le EL of OWL 2, and a fully edged OWL 2 reasoner. This division is carried out in such a way that the bulk of the workload is assigned, as much as possible, to the OWL 2 EL reasoner, in order to exploit the more e cient classi cation techniques speci c to this pro le.
Introduction
The Technique The main idea behind the technique implemented in MORe is to identify, given an ontology O with signature Sig(O), two subsets M1, M2 of O such that
the output of classifying M2 with the EL reasoner is complete for Sig(M2) w.r.t. O (i.e. it contains all subsumption relations A v B entailed by O such that A 2 Sig(M2)); the output of classifying M1 with the OWL reasoner is complete for Sig(M1) w.r.t. O; and Sig(M1) [ Sig(M2) = Sig(O).
Our implementation of MORe relies on ELK, which does not yet implement the whole of OWL 2 EL. The unsupported constructs are documented and hence we can identify the fragment LELK of OWL 2 EL implemented by ELK.
They key to identifying M1 and M2 is in computing an LELK-signature: a signature ELK Sig(O) such that the ?-module for ELK in O is an ontology in the language LELK for which ELK is complete.
The ?-module for O and , M[O; ], is the smallest subset of O such that all
axioms in O n M[O; ] are ?-local w.r.t. [ Sig(M[O; ]). Intuitively, an axiom
is ?-local w.r.t. if replacing by ? all occurrences in of symbols not in
would turn into a syntactically recognisable tautology; e.g., the axiom A v B
is ?-local w.r.t. = fBg. Cuenca Grau et al. [
(a) if A is unsatis able in O then it is also unsatis able in M[O; ] (b) if another class B in Sig(O) is a superclass of A in O, then it is so in
M[O; ] as well |and so B is in Sig(M[O; ]) too. 2. If 1 2, then if some axiom is ?-local w.r.t. 2, it is also ?-local w.r.t.
1, and therefore M[O; 1] M[O; 2]. 3. both checking ?-locality and extracting a ?-module can be done in polynomial time.
Property 1(b), in particular, is not shared by other kinds of modules, and makes ?-modules especially well suited for classi cation purposes. 2.1
Modular Combination of Reasoners
The integration of the two reasoners is performed as follows. Given an OWL 2
ontology O, MORe rst tries to compute a nonempty LELK-signature ELK for O
(details of how this is done are given in Section 2.2). If it suceeds, then ELK is
used to classify M[O; ELK], and HermiT or Pellet to classify M[O;Sig(O)n ELK];
nally, both partial hierarchies are uni ed into a single one. If MORe fails to nd
a nonempty LELK-signature, then it delegates the whole classi cation to either
HermiT or Pellet. Details about the correctness (soundness and completeness)
of this technique can be found in Armas Romero et al. [
Example 1. Consider the ontology Oex consisting of the following axioms: A
B t C
B
D u 9R:E
F v 9R:G All the axioms in Oex are in LELK except for = A B t C. Now, we have that is ?-local w.r.t. a signature i \ fA; B; Cg = ;, therefore, is ?-local w.r.t. = Sig(Oex) n fA; B; Cg. However, = B D u 9R:E is not ?-local w.r.t. , so 2 M[O; ] and B 2 Sig(M[O; ]), and therefore is not ?-local w.r.t. [ Sig(M[O; ]) and needs to be in M[O; ]. } All we need to do is progressively reduce be done as follows: until Sig(M[O; ]) . This can 1. Let S0 be the set of axioms in O that are not in LELK and let 0 = Sig(O). 2. Reduce 0 to some 1 0 such that S0 is ?-local w.r.t. 1. If this is not possible, then make 1 = ;. 3. Compute the set S1 of axioms in M[O; 1] containing symbols outside 1. 4. Repeat Steps 2{3 until Si = ; (i.e. until Sig(M[O; i]) i) or i = ;. It is important to note that, in some cases, there may be several di erent ways of obtaining i+1 from i.
Example 2. As shown in the previous example, taking = Sig(Oex)nfA; B; Cg is not enough to keep A B t C outside M[O; ]. We need to remove more symbols from to keep B D u 9R:E outside M[O; ] too. One possibility would be to remove D from , but we could also choose to remove R or E instead. It turns out that choosing one option over another can change things substantially.
If we chose to take 1 = Sig(Oex) n fA; B; C; Rg then, because F v 9R:G is not ?-local w.r.t. 1 and contains the symbol R, we would need to further reduce 1 to some 2 1.
However, if we took 1 = Sig(Oex)nfA; B; C; Dg or 1 = Sig(Oex)nfA; B; C; Eg, then we would already have Sig(M[Oex; 1]) = 1, and we would be done. }
The ?-module M[O;Sig(O)n EELLKK]ist.hTathetrheefoOreW,iLt irsedaesosinrearblneeteods to classify is likely to be smaller the larger nd heuristics to choose each i in a way that leads to an LELK-signature as large as possible. Below we describe the main heuristics that we have implemented in MORe. Keeping Properties As far as possible, we try not to remove properties from i. The reason for this is that most ontologies contain fewer properties than classes, and each property usually appears in more axioms than any class. Thus, removing a property from i is more likely to bring more axioms into the next Si+1 and lead to a smaller LELK-signature.
Global Symbols We perform a preprocessing stage to identify a (possibly empty) set of global symbols in Sig(O), such that either ELK or ELK = ;. For this, we rst nd the set G of all global axioms in O, i.e. those that cannot possibly be made ?-local, (e.g. axioms of the form > v C) and take = Sig(G). We then keep adding to the signatures of all the axioms in O that would only be ?-local w.r.t. ELK if some symbol in was left outside ELK, until no more symbols need to be added to .
Then, we will only ever consider sets i such that i. As the following example shows, this can sometimes mark the di erence between nding a nonempty LELK-signature or not.
Example 3. Consider the ontology Oe0x = Oex [ f> v 9R:Eg. In the previous example we saw how both Sig(Oex) n fA; B; C; Dg and Sig(Oex) n fA; B; C; Eg were equally good choices when choosing a suitable 1 for Oex . This is not the case any more with Oe0x, as after choosing Sig(Oe0x) n fA; B; C; Eg we would need to try to keep > v 9R:E outside M[Oe0x; ELK] too; but this is not possible, so in the end we would have ELK = ;. } Reducing Nondeterminism In each iteration of the algorithm, instead of considering the set Si as a whole, we split it into two subsets: Sinondet, containing those axioms in S for which there are several ways in which i can be reduced to make them ?-local, and Sidet, those for which there is only one way.
Whenever Sidet 6= ;, we obtain i+1 by removing from i the symbols required by each axiom in Sidet, and ignore Sinondet. When Sidet = ;, we deal with the axioms in Sinondet taking a greedy approach | nding the optimal solution is often too expensive.
The intuition behind this heuristic is that, by postponing making any nondeterministic decisions as much as possible, we might eliminate the need to make them altogether.
Note that, using this heuristic, we are not guaranteed to handle all the non LELK-axioms in the rst iteration any more, therefore we also have to consider in each Si those non-LELK axioms that are still not ?-local w.r.t. i. Example 4. Consider the ontology Oe00x consisting of all the axioms in Oex, plus the following additional axioms:
E v C
H v 9R:E
I (E u F) t (G u H) We rst get S0nondet = fI (E u F) t (G u H)g and S0det = fA B t Cg. The new non-LELK axiom, I (E u F) t (G u H), goes into S0nondet because it could be handled by removing any of the following sets of symbols: fI; E; Gg, fI; F; Gg, fI; E; Hg or fI; F; Hg. For now we only deal with S0det = fA B t Cg, and we do so by taking 0 = Sig(Oe00x) n fA; B; Cg.
Then we obtain the sets S1nondet = fB D u 9R:E; I (E u F) t (G u H)g and S1det = fE v Cg and we deal with E v C by taking 1 = Sig(Oe00x) n fA; B; C; Eg.
Metrics
Ontology
Gazetteer
We have tested MORe using an Ubuntu 12.04 64-bit machine with 7.8 GiB of
RAM (fully assigned to the JVM) and an Intel Core i7-3770 CPU @ 3.40GHz x
8 processor. Our test ontology suite includes six BioPortal ontologies5 [
We analyse our results by comparing the performance of MORe using HermiT vs. HermiT alone, and of MORe using Pellet vs. Pellet alone. A summary of all results can be found in Table 2. mem indicates an out of memory error.
When integrating HermiT, MORe is always able to improve, or at least maintain its performance. We remark the case of Cell Cycle v0.95, where the performance is improved from an out of memory error to termination in under 10s.
Integrating Pellet, however, sometimes has an unexpected e ect. In the cases of NCI v09.12d and Cell Cycle v2.01, Pellet takes longer to classify MOWL2 when integrated in MORe than to classify the whole ontology on its own. This however, does not happen when Pellet is used to classify MOWL2 independently of MORe. We are still unsure about the causes of this phenomenon. Apart from these two cases, MORe is still often able to improve on the performance of Pellet.
It is worth mentioning that the reason why, in the case of Cell Cycle v2.01, the portion of the ontology that the OWL reasoner has to process is so close to the whole ontology (98%) is because the 9 non LELK axioms are symmetric property axioms, which force their 9 respective properties out of ELK, reducing it to a very small set. 4
Conclusions and Future Directions We are continuing to develop MORe, exploring new ways of further reducing the workload assigned to a general purpose OWL 2 classi cation algorithm. We are looking into the possibility of alternative modularity notions speci c for this application, and also into exploiting computational properties of other lightweight ontology languages to combine our modular approach with one based on nding lower and upper bounds for the classi cation. This work was supported by the Royal Society, the Seventh Framework Program (FP7) of the European Commission under Grant Agreement 318338, "Optique", and the EPSRC projects Score!, ExODA and MaSI3.