Classification is a key ontology reasoning task. Several highly-optimised OWL reasoners are designed for different fragments of OWL 2. Combining these delegate reasoners to classify one ontology gives potential benefits, but these may be offset by overheads or redundant subsumption tests. In this paper, we show that with the help of the atomic decomposition, a known ontology partition approach, these redundant subsumption tests can be avoided. We design and implement our classification algorithms and empirically evaluate them.
gies. Several classification algorithms have been implemented in highly-optimized
reasoners [
We assume the reader to be familiar with Description Logics (DLs), a family of
knowledge representation languages underlying OWL 2 that are basically decidable fragments
of First Order Logic [
To classify an ontology O, we first check whether O is consistent. If it is, we check for all
2 Oe \ NC, ≠ , whether O j=? v O j=? v ? and O j=? > v . Naively, this
results in a quadratic number of entailment tests. To avoid these, DL reasoners employ
a form of traversal algorithm to reduce the number of STs [
Throughout this paper, we concentrate on ?-locality based modules [
2. preserves all entailments of O over Mf, i.e., it is self-contained, 3. is unique, i.e., there is no other ?-locality based module of O for the signature Σ, and 4. is subsumer-preserving, i.e., if is a concept name in M and O j= v , then
M j= v .
The atomic decomposition (AD) ¹Oº [
Definition 1. [
M, M implies that M.
For an atom 2 ¹Oº, its principal ideal # = f 2 j 2 ¹Oº g is the union of all atoms it depends on, and this has been shown to be a genuine module, i.e., it cannot be decomposed into a union of independent modules.
In this section, we explain the foundations of using the AD for avoiding STs during classification. Using the AD, we identify a (hopefully small) set of subsumption tests 2We use module for it in the rest of this paper. that are sufficient for classification. Provided that the AD has a ’good’ structure (no big atoms), this results in a low number of STs for a reasoner to carry out, with the potential to use delegate reasoners for these or parallelisation.
First, we fix some notation. Let be a concept name. The set of atoms Ats¹ º of is defined as follows:
Ats¹ º := f 2 ¹Oº j 2 eg
MinAts¹ º := f 2 Ats¹ º j there is no 2 Ats¹ º with g
CanS¹º of is
CanS¹º := f j 2 MinAts¹ º and #MinAts¹ º = 1g
Please note that CanS¹º is a subset of the set of concept names of the atom, i.e., CanS¹º e \ NC.
The set of concept names below top BTop¹Oº is defined as follows:
BTop¹Oº := f j 2 Oe \ NC and #MinAts¹ º ¡ 1g
In Figure 1, these different definitions are shown in the example ontology. Lemma 1. For each concept name 2 Oe, we have 1. Oe \ NC = Ð
CanS¹º [ BTop¹Oº.
2¹ Oº 2. if 2 BTop¹Oº, there is no atom 2 ¹Oº with 2 CanS¹º.
3. if 2 CanS¹º, there is no atom ≠ with 2 CanS¹º.
Proof. (1). Since ¹Oº partitions O, we have that Oe \ NC = 2¹ Oº each concept name 2 Oe \ NC, #MinAts¹ º ¡ 0. Let 2 Oe \ NC. If MinAts¹ º = 1, we thus have some 2 ¹Oº with 2 MinAts¹ º and hence 2 CanS¹º. Otherwise, MinAts¹ º ¡ 1 and 2 BTop¹Oº. The “ ” direction holds by definition of CanS¹º and BTop¹Oº. Ð e \ NC, and thus for (2). This follows immediately from the facts that 2 BTop¹Oº implies that #MinAts¹ º ¡ 1 and 2 CanS¹º implies that #MinAts¹ º = 1.
(3). Let 2 CanS¹º. By definition, 2 MinAts¹ º. Assume there was some ≠ with 2 CanS¹º; this would mean 2 MinAts¹ º, contradicting #MinAts¹ º = 1. Theorem 2. Given an ontology O and a concept name 2 BTop¹Oº, we have 1. M ¹f g Oº = ;, 2. O 6j= v ?, and 3. there is no concept name ≠ , 2 Oe with O j= v .
Proof. (1). Let 2 BTop¹Oº. Hence #MinAts¹ º ¡ 1, and thus there are two atoms 2 MinAts¹ º. By definition of MinAts¹ º, and . Now assume M ¹f g Oº ≠ ;; hence there is some with M ¹f g Oº = # . Since ?-locality based modules are monotonic, M ¹f g Oº # and M ¹f g Oº # which, together with 2 MinAts¹ º and 2 e, contradicts the minimality condition in the definition of MinAts¹ º.
(2). This is a direct consequence of (1) M ¹f g Oº = ;: ?-locality based modules capture deductive (and model) conservativity, hence M ¹f g Oº = ; implies that O cannot entail v ?.
(3). This is also a direct consequence of (1) and the fact that ?-locality based
modules are closed under subsumers [
Next, we use the AD to identify a (hopefully small) set of STs that are sufficient for classification.
Definition 2. The set of STs Subs¹º of an atom is defined as follows: Subs¹º := f¹ º j 2 CanS¹º 2 #f and ≠ g [ f¹ ?º j 2 CanS¹ºg [ f¹> º j 2 CanS¹ºg
Given a module M = 1 [ 2 [ , the set of STs Subs¹Mº of M is defined as follows:
Subs¹Mº :=
Theorem 3. For 2 Oe \ NC with ≠ , ≠ ?. If O j= v then there is exactly one with ¹ º 2 Subs¹º.
Proof. Let be as described in Theorem 3 and let O j= v . Then ∉ BTop¹Oº by Theorem 2 (3). By Lemma 1 (1), there is an atom with 2 CanS¹º. By definition, CanS¹º e #f, and thus 2 #f and, by Section 2.2, # is a module. By Section 2.2, we have 2 #f. By definition of Subs¹ º, ¹ º 2 Subs¹º. By Lemma 1 (3), we know there is no another atom is unique.
In [
Assume we have, for 1 modules M O that are in a specific description logic L for which we have a specialised, optimised reasoner.3 Based on our observations in Section 3, we can partition our subsumption tests as follows:
Ø 2¹ Oº *M1[[M Subs¹Oº =
Subs¹º [ [
Ø 2¹ Oº M1[[M
Subs¹º If we have one reasoner optimised for L, the modules M1, M2...M can be classified by this reasoner. Based on Section 2.2, if we classify the union of L modules M1 [ [ M, these satisfiability tests Ð Subs¹º are checked. Then we just have Ð
2¹ Oº M1[[M
Subs¹º waiting to be checked. Next, we will explain it with 2¹ Oº*M1[[M examples.
Assume we have one ontology shown in Figure 2(a) with 7 atoms and these axioms in atoms 1, 2, 5, 6, 7 are in L. We also have four modules M1, M2, M6, M7 in L. Here M5 is not in L because the atom 3 M5 is not in L.
Now we can use a specific reasoner for L to classify a set of axioms M1 [ M2 [ M6. Because our ontology is monotonic, classify M1 [ M2 [ M6 means these subsumption tests Subs¹1º, Subs¹2º, Subs¹6º, Subs¹7º are checked. We still have subsumption tests Subs¹3º, Subs¹4º, Subs¹5º remaining. Now we can either check these tests in the ontology shown in Figure 2(b) left part or check them in several modules contain atoms 3, 4, 5. For example, we can check Subs¹3º in M3, check Subs¹4º in M4 and check Subs¹5º in M5 shown in Figure 2(b) right part. Similarly, we can also check Subs¹3º, Subs¹4º, Subs¹5º in M4 [ M5.
Here a union of modules sometimes is not a module. For example, if we have 1 = f v g 2 = f v g 3 = f u v t g and L = EL in our example ontology shown in Figure 2(a). Now the union of modules M1 [ M2 [ M6 is not a module. Because now , are all in the signature of this module. Based on Section 2.2, we put the axioms which entails the subsumption relation between u and its subsumers into the module. So if we want to fix M1 [ M2 [ M6 to a module, we put u v t into the module. Then the module is not even in EL. It means if we want a L module which is a superset of the union of L modules, we will have not only additional axioms in this module but also this L module is sometimes not in L. The evaluation of this phenomenon is shown in Section 6.2.
In this paper, we have L = EL¸¸ [
3It is straightforward to extend this to more than one DL and more than one specialised, optimised reasoner. (a) an AD with seven atoms in different Description Logics
(b) Different Choice for left subsumption tests
In this section, we introduce our the classification algorithm ReAD as sketched in Algorithm 1. Firstly, we compute the AD and get the union of E L¸¸ modules T . Then we use a reasoner specific for E L¸¸ to classify T and store the subsumption relation to hierarchy H . Then we use another reasoner for OWL DL to finish the rest of STs in left atoms. In order to do that, we modify the classification algorithm for the OWL DL reasoner. In this paper, we pick HermiT as the OWL DL reasoner. The modified classification algorithm of HermiT is shown in Algorithm 2.
In Algorithm 2 we modify the classification algorithm in HermiT in order to make
it AD-aware (recall that we assume that our ontology has already been tested for
consistency). If = >, we will not check T 0 6j= v ?. For every ST, HermiT uses a
wellorganized transitive closure and free results from ST to implement Prune() in order to
avoid STs. More details about Prune() are shown in [
Require: a set of atoms RemainingAtoms, ?-¹Oº, a hierarchy H 1: TopAtoms = f j 2 RemainingAtoms and there is no atom
RemainingAtoms with g 2: compute a set of axioms T 0 = #
Ð 2TopAtoms
In this section, we report on the empirical evaluation of our algorithm. In particular, we answer the following research questions: 1. Compared to the size of the whole ontology, what is the size of the union of EL¸¸ modules? This will help us to understand the potential benefits of using ELK. 2. How many EL¸¸ modules are in the union of modules? Are these modules a
EL¸¸ module? This will help us to understand potential overlap. 3. Compared to the classification time and the number of STs of HermiT, what is the classification time of ReAD and how many STs does ReAD run?
Corpus In our experiment, we use the snapshot of the NCBO BioPortal ontology repository4 by [24], which contains 438 ontologies. Firstly, we remove ABox axioms for these 438 ontologies since we want to know how the classification algorithm behaves on the TBox axioms. Then we remove those ontologies that have only ABox axioms or are not in OWL 2 DL. We also remove those ontologies for which we cannot compute an AD or which HermiT cannot handle. To concentrate on STs and traversal algorithms, we also remove deterministic ontologies using a test provided by HermiT.5 This leaves us with a corpus of 98 ontologies; the number of their TBox axioms and the length6 of these ontologies is summarised in Table 1.
Implementation The implementation of ReAD is based on the OWL API [25] Version 3.4.3, especially on the implementation of the AD7 that is part of the OWL API, namely the one available via Maven Central (maven.org) with an artifactId of owlapi-tools. We modify the code of reasoner HermiT in version 1.3.88 and use the reasoner ELK version 0.4.2 as a delegate reasoner. We also use the code from MORe9 for checking E L¸¸ axioms in used for ELK. All experiments have been performed on Intel(R) Core(TM) i7-6700HQ CPU 2.60GHz RAM 8GB, running Xms1G Xmx8G. Time is measured in CPU time. 6.2. The Size and Details of the Union of L modules In this section, we answer our research Questions 1 and 2. Using Algorithm 1, we implement and compute the union of E L¸¸ modules for these ontologies; in the following, we call this union the E L¸¸-part of an ontology. We have 34 ontologies that do not contain any E L¸¸ modules. Figure 3 shows scatter plots of the size of TBox axioms (each point) and the union of E L¸¸ modules (each x-mark) of each ontology (with the same x-axis value) among 64 ontologies which contain at least one E L¸¸ module in our corpus. We find that there are many ontologies in our corpus that have a large E L¸¸-part. These ontologies also distribute evenly among different sizes.
To answer our research question 2, we consider how the number of (subset-) maximal E L¸¸ modules in the E L¸¸-parts varies across the ontologies in our corpus in Table 2. Among our 64 ontologies, only one ontology has only one such maximal E L¸¸ module. In Table 2, we find most of ontologies have a large number of maximal E L¸¸ genuine modules (average 1,701).; half of our ontologies (32) have more than 69 maximal E L¸¸ genuine modules and 99% ontologies have 9,662 maximal E L¸¸ genuine modules.
As discussed at the end of Section 4, a union of E L¸¸ modules is not necessarily an E L¸¸ module. We tested, for our 64 ontologies, whether the E L¸¸-part is a module. It turns out that this is the case a surprisingly large proportion of our ontologies, i.e., 80% (13/64), which could be exploited further for classification.
5HermiT does not use a traversal algorithm for these.
6The length in this chapter is defined in [
7AD implementation now is only in OWL API version 5. In our implementation we compile one to OWL API version 3 8The code of this version can be found in http://www.hermit-reasoner.com 9http://owlapi.sourceforge.net/
In these experiments, we use HermiT version 1.3.8 to compare classification times with. First, we classify our 64 ontologies 5 times to understand the variation of classification time. Then we use ReAD to classify the 64 ontologies and record classification time data as a combination of ELK classification time and modified HermiT classification time.10 Inspired by [26,27], we split our classification data into three bins: (1) less than 1,000ms; (2) more than 1,000ms and less than 10,000ms; (3) more than 10,000ms. Then we discuss and compare the results for each bin.
We also want to know how the EL¸¸ modules size affect the our classification time. So we define EL¸¸ModulesPercentage as:
EL¸¸ = # EL¸¸ # The classification times measured in CPU Time (ms) versus EL¸¸ Modules percentage among 64 ontologies for HermiT and ReAD are shown in Figure 4. It shows scatter plots of the HermiT classification time (each point) and ReAD classification time (each x-mark) of each ontology (with the same x-axis value) among 64 ontologies. We find that for these ontologies which EL¸¸ModulesPercentage is more than 50% trends to have a classification time improvement. We also have some ontologies which have lower than 50% EL¸¸ModulesPercentage but also have a significant improvement, e.g. NCIT (47%) from around 75s to 47s, PHAGE (36%) from around 594s to 436s.
We also count the STs number of HermiT and modified HermiT in ReAD shown in Table 3. We find the number of STs decreases as we expected in theory. 10This excludes the time used for computation of AD. (a) Classification Time less than 1,000ms for HermiT(b) Classification Time less than 10,000ms for and ReAD HermiT and ReAD (c) Classification Time more than 10,000ms for
HermiT and ReAD
In this paper, we design and implement our approach for avoiding redundant STs during classification with the help of AD. We show how our algorithm interacts with the classification algorithm in HermiT. In the future, we also want to explore how our algorithm interacts with Enhanced Traversal algorithm. In Section 4, there are several choices for checking the remaining STs. In this paper, we use the union of modules of each atom if we have Subs¹º in our remaining STs for our experiment evaluation. We can also check these STs in the whole ontology or check each Subs¹º in its genuine module # . How to decide this is also related to easing the STs. In [28] Chapter 7, the author designs, categorizes and organizes how to make a choice of the set of axioms for STs. Using these strategies for checking left STs will tell us more about easification hypothesis: Using module than the whole ontology checking STs will make the STs easier and faster or not?
Since AD gives benefit for optimizing Classification. Optimizing the computation AD gives benefit. In [29], the author recommend that we can store the AD as a specific format for ontology. When we classify the ontology, we can use this pre-computed AD rather than computing AD every time.
Matentzoglu N, Parsia B. BioPortal Snapshot 30 March 2017 (data set). Zenodo; 2017. http://doi. org/10.5281/zenodo.439510.
Horridge M, Bechhofer S. The owl api: A java api for owl ontologies. Semantic web. 2011;2(1):11–21. Goncalves JR. Impact analysis in description logic ontologies. The University of Manchester; 2014. Gonc¸alves RS, Parsia B, Sattler U. Performance heterogeneity and approximate reasoning in description logic ontologies. In: International Semantic Web Conference. Springer; 2012. p. 82–98.
Matentzoglu NA. Module-based classification of OWL ontologies. University of Manchester; 2016. Del Vescovo C, Gessler DD, Klinov P, Parsia B, Sattler U, Schneider T, et al. Decomposition and modular structure of bioportal ontologies. In: International Semantic Web Conference. Springer; 2011. p. 130–145.