=Paper=
{{Paper
|id=Vol-2708/womocoe2
|storemode=property
|title=ReAD: Delegate OWL Reasoners for Ontology Classification with Atomic Decomposition
|pdfUrl=https://ceur-ws.org/Vol-2708/womocoe2.pdf
|volume=Vol-2708
|authors=Haoruo Zhao,Bijan Parsia,Uli Sattler
|dblpUrl=https://dblp.org/rec/conf/jowo/ZhaoPS20
}}
==ReAD: Delegate OWL Reasoners for Ontology Classification with Atomic Decomposition==
https://ceur-ws.org/Vol-2708/womocoe2.pdf
ReAD: Delegate OWL Reasoners for
Ontology Classification with Atomic
Decomposition1
Haoruo ZHAO a , Bijan PARSIA a and Uli SATTLER a
a University of Manchester, United Kingdom
{ haoruo.zhao, bijan.parsia, uli.sattler } @manchester.ac.uk
Abstract. 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.
Keywords. OWL, Description Logic, Classification, Delegate Reasoner
1. Introduction
Classification is a core reasoning task for Web Ontology Language (OWL) 2 [1] ontolo-
gies. Several classification algorithms have been implemented in highly-optimized rea-
soners [2,3,4,5] for different fragments [6,7,8] of OWL 2. For OWL 2, these use a traver-
sal algorithm which determines which subsumptions to test next, ideally avoiding most
of them [9,10]. Ontology modularisation [11,12,13,14], especially locality-based mod-
ules [15] (logical approximations of conservative extension-based modules) and Atomic
Decomposition (AD) [16] (an ontology partition algorithm), have already been used for
optimizing the classification [17,18,19,20] by easing subsumption test (STs) or avoiding
them. But checking STs with modules or AD rather than the whole ontology causes re-
dundant STs. In this paper, we design and implement our algorithm with no redundant
STs and also evaluate our algorithm with a corpus of BioPortal ontologies.
2. Background Knowledge
We assume the reader to be familiar with Description Logics (DLs), a family of knowl-
edge representation languages underlying OWL 2 that are basically decidable fragments
of First Order Logic [21], and only fix the notation used. In this paper, we use O for an
1 Copyright Β© 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution
4.0 International (CC BY 4.0).
ontology and M β O for a β₯-syntactic locality-based module.2 A signature Ξ£ is a set of
concept names and role names. For an axiom, a module, or an ontology π, we use π e to
denote its signature.
2.1. Classification
To classify an ontology O, we first check whether O is consistent. If it is, we check for all
π΄, π΅ β Oe β© NC , π΄ β π΅, whether O |=? π΄ v π΅, O |=? π΄ v β₯ and O |=? > 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 [9,10]. In practice, these are
highly effective, almost always reducing the quadratic number of STs to at most π β log π
tests [19]. In this paper, we concentrate on ST avoidance and assume all ontologies to be
consistent.
2.2. Modules and AD
Throughout this paper, we concentrate on β₯-locality based modules [22]. These are sub-
sets of an ontology that have certain properties which are important for their use in AD
and, in turn, for classification optimization. Let M = M (Ξ£, O) be such a β₯-locality based
module of O for the signature Ξ£. Then M
1. preserves all entailments of O over Ξ£, i.e., it covers Ξ£,
2. preserves all entailments of O over M, f 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 |= π΄ v π΅, then
M |= π΄ v π΅.
The atomic decomposition (AD) π(O) [16] partitions an ontology into logically
inseparable sets of axioms, so-called atoms π, and relates these atoms via a dependency
relation . In the rest of paper, we use π(O) to represent the β₯-AD because in [23], we
find these to be mostly fine-grained than other ADs.
Definition 1. [23] Given two axioms πΌ, π½ β O, we say πΌ βΌ O π½ if for all modules M of O,
we have πΌ β M iff π½ β M. The atoms of an ontology O are the equivalence classes βΌ O .
Given two atoms π, π, we say that π is dependent on π, written π π if, for any module
M, π β M implies that π β M.
For an atom π β π(O), its principal ideal βπ = {πΌ β π | π β π(O), π π} 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.
3. The set of STs of an atom, a module and an atomic decomposition
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
2 We use module for it in the rest of this paper.
Figure 1. the example of different definitions of O
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( π΄) := {π β π(O) | π΄ β e
π}.
The set of lowest atoms MinAts( π΄) of π΄ is defined as follows:
MinAts( π΄) := {π β Ats( π΄) | there is no π β Ats( π΄) with π π}.
For an atom π, the candidate set of concept names to be tested is defined as follows:
CanS(π) of π is
CanS(π) := { π΄ | π β MinAts( π΄) and #MinAts( π΄) = 1}.
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) := { π΄ | π΄ β O
e β© NC and #MinAts( π΄) > 1}.
In Figure 1, these different definitions are shown in the example ontology.
Lemma 1. For each concept name π΄ β O,
e we have
e β© NC = Γ CanS(π) βͺ BTop(O).
1. O
πβπ( O)
2. if π΄ β BTop(O), there is no atom π β π(O) with π΄ β CanS(π).
3. if π΄ β CanS(π), there is no atom π β π with π΄ β CanS(π).
Proof. (1). Since π(O) partitions O, we have that Oe β© NC = Γ e π β© NC , and thus for
πβπ( O)
each concept name π΄ β O e β© NC , #MinAts( π΄) > 0. Let π΄ β O
e β© NC . If MinAts( π΄) = 1,
we thus have some π β π(O) with π β MinAts( π΄) and hence π΄ β CanS(π). Otherwise,
MinAts( π΄) > 1 and π΄ β BTop(O). The βββ direction holds by definition of CanS(π) and
BTop(O).
(2). This follows immediately from the facts that π΄ β BTop(O) implies that
#MinAts( π΄) > 1 and π΄ β CanS(π) implies that #MinAts( π΄) = 1.
(3). Let π΄ β CanS(π). By definition, π β MinAts( π΄). Assume there was some π β π
with π΄ β CanS(π); this would mean π β MinAts( π΄), contradicting #MinAts( π΄) = 1.
Theorem 2. Given an ontology O and a concept name π΄ β BTop(O), we have
1. M ({ π΄}, O) = β
,
2. O 6 |= π΄ v β₯, and
3. there is no concept name π΅ β π΄, π΅ β O
e with O |= π΄ v π΅.
Proof. (1). Let π΄ β BTop(O). Hence #MinAts( π΄) > 1, and thus there are two atoms π, π β
MinAts( π΄). By definition of MinAts( π΄), π π and π π. Now assume M ({ π΄}, O) β β
;
hence there is some π with M ({ π΄}, O) = βπ . Since β₯-locality based modules are mono-
tonic, M ({ π΄}, O) β βπ and M ({π΄}, O) β βπ which, together with π, π β MinAts( π΄) and
π΄ βeπ , contradicts the minimality condition in the definition of MinAts( π΄).
(2). This is a direct consequence of (1) M ({π΄}, O) = β
: β₯-locality based modules
capture deductive (and model) conservativity, hence M ({ π΄}, O) = β
implies that O can-
not entail π΄ v β₯.
(3). This is also a direct consequence of (1) and the fact that β₯-locality based mod-
ules are closed under subsumers [22].
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(π) := {( π΄, π΅) | π΄ β CanS(π), π΅ β βπ,
f and π΄ β π΅} βͺ
{( π΄, β₯) | π΄ β CanS(π)} βͺ
{(>, π΅) | π΅ β CanS(π)}.
Given a module M = π1 βͺ π2 ... βͺ ππ , the set of STs Subs(M) of M is defined as
follows:
Γ
Subs(M) := Subs(ππ¦ ).
π=1,...,π
Γ
Analogously, Subs(O) := πβπ( O) Subs(π).
The following theorem states a set of STs that tests are sufficient for classification,
and thus also which can be avoided/are redundant.
Theorem 3. For π΄, π΅ β O e β© NC with π΄ β π΅, π΄ β β₯. If O |= π΄ v π΅ then there is exactly
one π with ( π΄, π΅) β Subs(π).
Proof. Let π΄, π΅ be as described in Theorem 3 and let O |= π΄ v π΅. Then π΄ β BTop(O)
by Theorem 2 (3). By Lemma 1 (1), there is an atom π with π΄ β CanS(π). By definition,
CanS(π) β e π β βπ,
f and thus π΄ β βπ f and, by Section 2.2, βπ is a module. By Section 2.2,
we have π΅ β βπ. By definition of Subs(Β·), ( π΄, π΅) β Subs(π). By Lemma 1 (3), we know
f
there is no another atom π is unique.
In [23], we have shown that the AD of many ontologies results in many small atoms
with a rather shallow and wide dependency relation. As a consequence, we should be able
to exploit the AD and the insights captured in Theorem 3 to avoid almost all subsumption
tests in a novel, AD-informed alternative to well-known enhanced traversal algorithms
[9,10].
4. How the set of satisfiability tests of an AD interacts with delegate reasoners
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:
Γ Γ
Subs(O) = Subs(ππ ) βͺ . . . βͺ Subs(ππ )
ππ βπ( O) , ππ βπ( O),
ππ *M1 βͺ...βͺM π ππ βM1 βͺ...βͺM π
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
Γ π π βπ( O),ππ βM 1 βͺ...βͺM π
have Subs(ππ ) waiting to be checked. Next, we will explain it with
ππ βπ( 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 = { π΄ v π΅}, π2 = {πΆ v π·}, π3 = {π΅ u π· v πΈ t πΉ} and L = EL in our example ontol-
ogy 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 ++ [6] and we use ELK [5] for classifying the union
of EL ++ modules M1 βͺ . . . βͺ M π .
3 It is straightforward to extend this to more than one DL and more than one specialised, optimised reasoner.
(a) an AD with seven atoms in (b) Different Choice for left subsumption tests
different Description Logics
Figure 2. a example for dealing with Subs( O)
5. How the set of satisfiability tests of an AD interacts with classification algorithm
In this section, we introduce our the classification algorithm ReAD as sketched in Algo-
rithm 1. Firstly, we compute the AD and get the union of EL ++ modules T . Then we use
a reasoner specific for EL ++ 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.
Algorithm 1 AD-aware Classification
Require: an ontology O
1: initialize a hierarchy H
2: compute the β₯-π(O)
3: compute a set of atoms SetAtoms = {π | π β β₯-π(O) and βπ is in EL ++ }
Γ
4: compute a set of axioms T = π
πβSetAtoms
5: Classify(T ) {use a reasoner specific for T }
6: add π΄ v π΅ into H if T |= π΄ v π΅ and π΄ β π΅
7: RemainingAtoms = β₯-π(O) \ SetAtoms
8: CheckRemainingSTs(RemainingAtoms, β₯-π(O), H ) {use a modified reasoner }
9: return H
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 con-
sistency). If π΄ = >, we will not check T 0 6 |= π΄ v β₯. For every ST, HermiT uses a well-
organized transitive closure and free results from ST to implement Prune() in order to
avoid STs. More details about Prune() are shown in [10].
Algorithm 2 CheckRemainingSTs
Require: a set of atoms RemainingAtoms, β₯-π(O), a hierarchy H
1: TopAtoms = {π | π β RemainingAtoms and there is no atom π β
RemainingAtoms with π π}
2: compute a set of axioms T 0 =
Γ
βπ
πβTopAtoms
3: pre-processing
4: compute CanS(π) for π β RemainingAtoms and BTop(O)
5: for every concept name π΄ β BTop(O) do
6: add β₯ v π΄ and π΄ v > to H .
7: end for
8: unclassifiedCon = β
9: for every concept name π΄ β CanS(π) with π β RemainingAtoms or π΄ = > do
10: if T 0 6 |= π΄ v β₯ then
11: for every concept name π΅ β βπ,
f and π΄ β π΅ do
12: if π΄ v π΅ β H then
13: Check O |=? π΄ v π΅. If yes, add π΄ v π΅ to H
14: Prune()
15: end if
16: end for
17: else
18: add π΄ v β₯ to H
19: end if
20: end for
21: return the hierarchy
6. Evaluation
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?
6.1. Experiment Setting
Corpus In our experiment, we use the snapshot of the NCBO BioPortal ontology repos-
itory4 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
4 https://bioportal.bioontology.org
Table 1. A summary of 98 ontologies. The 50th (median), 90th, 95th, 99th, 100th (maximum) percentiles are
shown for the size (i.e. number of axioms) and the length (i.e., sum of length of axioms) of ontologies.
Mean StdDev P50 P90 P95 P99 P100
Size 7,154 23,219 911 13,223 26,540 117,375 167,022
Length 19,897 72,366 2,266 27,633 53,188 444,713 511,147
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] Ver-
sion 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 EL ++ axioms in used for ELK. All experiments have been performed on In-
tel(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 imple-
ment and compute the union of EL ++ modules for these ontologies; in the following, we
call this union the EL ++ -part of an ontology. We have 34 ontologies that do not contain
any EL ++ modules. Figure 3 shows scatter plots of the size of TBox axioms (each point)
and the union of EL ++ modules (each x-mark) of each ontology (with the same x-axis
value) among 64 ontologies which contain at least one EL ++ module in our corpus. We
find that there are many ontologies in our corpus that have a large EL ++ -part. These
ontologies also distribute evenly among different sizes.
To answer our research question 2, we consider how the number of (subset-) max-
imal EL ++ modules in the EL ++ -parts varies across the ontologies in our corpus in Ta-
ble 2. Among our 64 ontologies, only one ontology has only one such maximal EL ++
module. In Table 2, we find most of ontologies have a large number of maximal EL ++
genuine modules (average 1,701).; half of our ontologies (32) have more than 69 max-
imal EL ++ genuine modules and 99% ontologies have 9,662 maximal EL ++ genuine
modules.
As discussed at the end of Section 4, a union of EL ++ modules is not necessarily an
EL module. We tested, for our 64 ontologies, whether the EL ++ -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.
5 HermiT does not use a traversal algorithm for these.
6 The length in this chapter is defined in [23] Page 24.
7 AD implementation now is only in OWL API version 5. In our implementation we compile one to OWL
API version 3
8 The code of this version can be found in http://www.hermit-reasoner.com
9 http://owlapi.sourceforge.net/
Figure 3. The size of the ontologies and their L-part in our corpus.
Table 2. A summary of 64 ontologies. The 50th (median), 90th, 95th, 99th, 100th (maximum) percentiles are
shown for the number of L modules of ontologies.
Mean StdDev P50 P90 P95 P99 P100
The number of E L ++ modules 1,701 8,311 69 1,363 5,055 9,662 66,050
6.3. The Classification Time and CTs number during Classification
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.
10 This 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
Figure 4. Classification Time measured in CPU Time (ms) versus E L ++ Modules percentage among 64 on-
tologies for HermiT and ReAD
Table 3. A summary of 64 ontologies. The 50th (median), 90th, 95th, 99th, 100th (maximum) percentiles are
shown for the STs number in HermiT and modified HermiT of ontologies.
Mean StdDev P50 P90 P95 P99 P100
#STs in HermiT 387 834 64 849 2,359 4,094 4,130
#STs in modified HermiT 178 528 11 481 660 2,730 3,465
7. Summary and Future Work
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 classi-
fication 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.
References
[1] Grau BC, Horrocks I, Motik B, Parsia B, Patel-Schneider P, Sattler U. OWL 2: The next step for OWL.
Journal of Web Semantics. 2008;6(4):309β322.
[2] Glimm B, Horrocks I, Motik B, Stoilos G, Wang Z. HermiT: an OWL 2 reasoner. Journal of Automated
Reasoning. 2014;53(3):245β269.
[3] Steigmiller A, Liebig T, Glimm B. Konclude: system description. Journal of Web Semantics.
2014;27:78β85.
[4] Sirin E, Parsia B, Grau BC, Kalyanpur A, Katz Y. Pellet: A practical owl-dl reasoner. Journal of Web
Semantics. 2007;5(2):51β53.
[5] Kazakov Y, KroΜtzsch M, SimancΜΔ±Μk F. The incredible elk. Journal of automated reasoning. 2014;53(1):1β
61.
[6] Baader F, Brandt S, Lutz C. Pushing the E L envelope further. In: OWLED; 2008. .
[7] Horrocks I, Kutz O, Sattler U. The Even More Irresistible S R O I Q. In: KR-06; 2006. p. 57β67.
[8] Hustadt U, Motik B, Sattler U. Data complexity of reasoning in very expressive description logics. In:
IJCAI; 2005. p. 466β471.
[9] Baader F, Hollunder B, Nebel B, Profitlich HJ, Franconi E. An empirical analysis of optimization
techniques for terminological representation systems. Applied Intelligence. 1994;4(2):109β132.
[10] Glimm B, Horrocks I, Motik B, Shearer R, Stoilos G. A novel approach to ontology classification.
Journal of Web Semantics. 2012;14:84β101.
[11] Grau BC, Parsia B, Sirin E, Kalyanpur A. Modularity and Web Ontologies. In: KR; 2006. p. 198β209.
[12] Romero AA, Kaminski M, Grau BC, Horrocks I. Module extraction in expressive ontology languages
via datalog reasoning. Journal of Artificial Intelligence Research. 2016;55:499β564.
[13] Lutz C, Walther D, Wolter F. Conservative Extensions in Expressive Description Logics. In: IJCAI;
2007. p. 453β458.
[14] Ghilardi S, Lutz C, Wolter F. Did I Damage My Ontology? A Case for Conservative Extensions in
Description Logics. In: KR. AAAI Press; 2006. p. 187β197.
[15] Cuenca Grau B, Horrocks I, Kazakov Y, Sattler U. A Logical Framework for Modularity of Ontologies.
In: IJCAI; 2007. p. 298β303.
[16] Del Vescovo C, Parsia B, Sattler U, Schneider T. The Modular Structure of an Ontology: Atomic
Decomposition. In: IJCAI; 2011. p. 2232β2237.
[17] Tsarkov D, Palmisano I. Chainsaw: a Metareasoner for Large Ontologies. In: ORE; 2012. .
[18] Romero AA, Grau BC, Horrocks I. MORe: Modular combination of OWL reasoners for ontology
classification. In: International Semantic Web Conference. Springer; 2012. p. 1β16.
[19] Matentzoglu N, Parsia B, Sattler U. OWL reasoning: Subsumption test hardness and modularity. Journal
of automated reasoning. 2018;60(4):385β419.
[20] Zhao H, Parsia B, Sattler U. Avoiding Subsumption Tests During Classification Using the Atomic
Decomposition. In: DL-19. vol. 573; 2019. .
[21] Baader F, Horrocks I, Lutz C, Sattler U, editors. An Introduction to Description Logic. Cambridge
University Press; 2017.
[22] Cuenca Grau B, Horrocks I, Kazakov Y, Sattler U. Modular reuse of ontologies: Theory and practice.
Journal of Artificial Intelligence Research. 2008;31(1):273β318.
[23] Del Vescovo C, Horridge M, Parsia B, Sattler U, Schneider T, Zhao H. Modular Structures and Atomic
Decomposition in Ontologies (to be published). Journal of Artificial Intelligence Research.
[24] Matentzoglu N, Parsia B. BioPortal Snapshot 30 March 2017 (data set). Zenodo; 2017. http://doi.
org/10.5281/zenodo.439510.
[25] Horridge M, Bechhofer S. The owl api: A java api for owl ontologies. Semantic web. 2011;2(1):11β21.
[26] Goncalves JR. Impact analysis in description logic ontologies. The University of Manchester; 2014.
[27] Gonç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.
[28] Matentzoglu NA. Module-based classification of OWL ontologies. University of Manchester; 2016.
[29] 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.