=Paper=
{{Paper
|id=None
|storemode=property
|title= WSReasoner: A Prototype Hybrid Reasoner for ALCHOI Ontology Classification using a Weakening and Strengthening Approach
|pdfUrl=https://ceur-ws.org/Vol-858/ore2012_paper6.pdf
|volume=Vol-858
|dblpUrl=https://dblp.org/rec/conf/ore/SongSD12
}}
== WSReasoner: A Prototype Hybrid Reasoner for ALCHOI Ontology Classification using a Weakening and Strengthening Approach==
https://ceur-ws.org/Vol-858/ore2012_paper6.pdf
WSReasoner: A Prototype Hybrid Reasoner for
ALCHOI Ontology Classification using a
Weakening and Strengthening Approach
Weihong Song1 , Bruce Spencer1,2 , and Weichang Du1
1
Faculty of Computer Science, University of New Brunswick, Fredericton, Canada
{song.weihong, bspencer, wdu}@unb.ca,
2
National Research Council, Canada
Abstract. In the ontology classification task, consequence-based reasoners are
typically significantly faster while tableau-based reasoners can process more ex-
pressive DL languages. However, both of them have difficulty to classify some
available large and complex ALCHOI ontologies with complete results in ac-
ceptable time. We present a prototype hybrid reasoning system WSReasoner,
which is built upon and takes advantages of both types of reasoners to provide
efficient classification service. In our proposed approach, we approximate the tar-
get ontology O by a weakened version Owk and a strengthened version O str , both
are in a less expressive DL ALCH and classified by a consequence-based main
reasoner. Classification of Owk produces a subset of subsumptions of ontology O
and the target of the classification of O str is to produce a superset of subsumptions
of O. Additional subsumptions derived from O str may be unsound, so they are fur-
ther verified by a tableau-based assistant reasoner. For the ALCHOI ontologies
in our experiment, except for one for which WSReasoner has not obtained the re-
sult, (1) the number of subsumptions derived from WSReasoner is no fewer than
from the reasoners that could finish the classification; (2) WSReasoner takes less
time than tableau-based reasoners when the ALCHOI ontologies are large and
complex.
1 Introduction
Ontology classification — computing the subsumption relationships between classes —
is one of the foundational reasoning tasks provided by many reasoners. Tableau-based
and consequence-based reasoners are two dominant types of reasoners that provide the
ontology classification service. Tableau-based reasoners, such as HermiT [8],
Fact++ [13] and Pellet [12], try to build counter-models A u ¬B for candidate sub-
sumption relations, based on sound and complete calculi such as [4] and [8]. These
reasoners are able to classify ontologies in expressive DLs like SROIQ(D).
Consequence-based reasoners classify the ontology based on specifically designed
inference rules for deriving logical consequences of the axioms in the ontology. Initial-
ly developed for the family of tractable DLs like EL++ [1], these procedures were later
extended to Horn-SHIQ [5] and ALCH [11] while preserving optimal computation-
al complexity. Reasoners belonging to this category, such as CB, ConDOR, ELK [6],
CEL [1] and TrOWL [9], are usually very fast and use less memory.
2 Weihong Song, Bruce Spencer, and Weichang Du
Fig. 1. Subsumption Diagram
We present a hybrid reasoning system that takes the advantages of both types of
reasoners for efficient classification on large and complex ontologies in expressive
DLs. Here “complex ontologies” refers to the ontologies which contains a consider-
able amount of cyclic definitions, which usually causes large models constructed by the
tableau procedures. In our approach, for the main reasoner we choose one that supports
a less expressive language, which we call the base language. From the original onto-
logy O, we first remove the axioms that are beyond the base language, and so construct
a weakened ontology Owk . In the second stage, we then inject into Owk additional ax-
ioms to simulate the effects of those removed axioms in a model expansion process,
constructing the strengthened ontology O str . These injected axioms are expressed in
the base language so they may not perfectly represent the original axioms. We call the
stages weakening and strengthening, respectively. After applying these changes to the
ontology, we still would like the subsumptions in O str to contain all the subsumptions
in O. In Fig. 1, the results of classification, named the class hierarchy, for ontology O,
Owk , and O str are denoted by HO , Hwk and H str respectively. The subsumptions pairs
in H str may be unsound with respect to O. If this occurs, we will need again to verify
these suspected pairs by reasoning in the language of the given ontology to remove any
unsound subsumptions and other maintenance tasks. We name the reasoner that accept-
s the full language of O, the assistant reasoner; it is potentially slower than the main
reasoner.
Our main contributions are as follows:
Hybrid Reasoning using Weakening and Strengthening Approach: We propose
a new hybrid reasoning approach by combining the tableau-based and consequence-
based reasoning procedures for efficient classification on large and complex ontologies.
Concretely, the hybrid reasoning is based on a weakening and strengthening approach
and applied to classifying ALCHOI ontologies, for which we choose ALCH as the
base language to take advantage of the recently developed consequence-based reasoning
technique which is able to classify non-Horn ontologies [11].
Implementation and Evaluation: Our system is able to classify ontologies in DL
ALCHOI, which is not fully supported by any current consequence-based reasoner.
We evaluate our procedure with nine available, practical ALCHOI ontologies. Except
for one ontology we have not gotten the classification result, we are able to achieve
soundness with no fewer subsumptions and a better performance than the tableau-based
reasoners on large ontologies.
2 Preliminaries and Related Work
The syntax of ALCHOI uses mutually disjoint sets of atomic concepts NC , atomic
roles NR and individuals NI . The set of roles is NR ∪ {R− | R ∈ NR }. The set of concepts
contains A, >, ⊥, ¬C, C u D, C t D, ∃R.C, ∀R.C, {a}, for > the top concept, ⊥ the
WSReasoner: A Prototype Hybrid Reasoner 3
bottom concept, A an atomic concept, C and D concepts, R a role, a an individual. We
define NC> = NC ∪ {>} and NC>,⊥ = NC> ∪ {⊥}. An ontology O consists of a set of general
concept inclusions C v D and role inclusions R v S . A concept equivalence C = D is
a shortcut for C v D and D v C.
An interpretation I of O is a pair (∆I , ·I ) where ∆I is a non-empty set, ·I maps each
A ∈ NC to a set AI ⊆ ∆I , each R ∈ NR to a relation RI ⊆ ∆I × ∆I and each a ∈ NI an
element aI ∈ ∆I . The interpretation of concepts are defined in [2]. An interpretation I
satisfies axioms C v D and R v S if C I ⊆ DI and RI ⊆ S I , respectively. I is a model
of O if I satisfies every axiom in O. If every model of O satisfies an axiom α, we say O
entails α and write O |= α.
An ontology classification task is to compute the class hierarchy HO containing all
the pairs hA, Bi such that A, B ∈ NC>,⊥ and O |= A v B. We define the role hierarchy Hop
as the pairs hR, S i such that R, S ∈ NR ∪ {R− | R ∈ NR } and O |= R v S .
Our work can be placed in the Theory Approximation setting [10], where a theory
Σ is approximated by a lower bound Σlb , whose models are a subset of the models of
Σ, and an upper bound Σub whose models are a superset. Our weakening step creates
Owk which is an upper bound Σub . Instead of creating a lower bound Σlb , the target of
our strengthening step is to generate an O str of which some “important” models can
be transformed to models of O so that completeness can be achieved. The details will
be explained in Section 4.2. Subsumption results from Owk are guaranteed to be sound,
exactly as queries asked of Σub that return “yes” can be taken also as “yes” from Σ. New
candidate subsumption results from O str need to be checked, analogously as queries Σlb
that return “yes” need to be checked.
TrOWL [9] is a soundness-preserving approximate reasoner offering tractable clas-
sification for SROIQ ontologies by an encoding into EL++ with additional data struc-
tures. Instead of merely preserving soundness, our algorithm also aims to achieve com-
pleteness, although we have not yet proven it. Another difference lies in that the classi-
fication procedure of TrOWL is an extension of [1], while our procedure treats both the
main and the assistant reasoners as black boxes without changing them.
3 System Overview
The diagram of our system is shown in Fig. 2. The input is an OWL 2 ontology in any
syntax supported by the OWL API.3 The output is the class hierarchy HO that can be
accessed through the OWL API reasoning interfaces. We explain all the components in
the following, among which the ones in white boxes are mainly implemented by us:
– The preprocessor rewrites some axioms containing constructors that are not sup-
ported by the main reasoner.
– The indexer normalizes the ontology O and builds an internal representation of it
which is suitable for finding axioms and concept expressions. The index speeds up
search for strengthening axioms.
– The axiom injector calculates the strengthening axioms that approximate the ax-
ioms in O \ Owk . The algorithm will be illustrated in Section 4.
3
Since our algorithm is designed for DL ALCHOI, the unsupported anonymous concepts are
replaced with artificial atomic concepts and the unsupported axioms are ignored.
4 Weihong Song, Bruce Spencer, and Weichang Du
Fig. 2. Key components of WSReasoner
– The main and assistant reasoners perform the main reasoning tasks. They can be
customized by the settings in the configuration instance of each WSReasoner object.
– The comparer calculates the difference between two concept hierarchies produced
by the first and second round of classifications, Hwk and H str respectively.
The arrows in the Fig. 2 represent the data flow of the overall reasoning procedure. The
numbers on the arrow denote the execution order, and the symbols represent the data.
The arrows between the axiom injector and the main reasoner indicates their interac-
tions with each other.
4 The Hybrid Classification Procedure
In this section we give details of the hybrid classification procedure used in WSReasoner.
The major phases include preprocessing, normalization and reasoning. Section 4.1 ex-
plains preprocessing and normalization. Section 4.2 gives a model-theoretic illustration
of the weakening and strengthening approach using an example. And section 4.3 pro-
vides the details of the overall procedure and strengthening algorithms.
4.1 Preprocessing and Normalization
In the preprocessing phase, we rewrite the original ontology to make nominals and in-
verse roles occur only in the axioms of the forms Na = {a} and R = R0− , respectively.
For nominals, we first rewrite the related OWL 2 DL class expressions and axioms by
their equivalent forms containing only singleton nominal concepts, according to Ta-
ble 1. After that, for each {a}, we replace all its occurrences by a new concept Na and
add an axiom Na = {a}. We call Na a nominal placeholder for a in the following sec-
tions. For inverse roles, we replace each occurrence of R0− in an axiom by a named role
R and add an axiom R = R0− .
After preprocessing, apart from the axioms of the forms Na = {a} and R = R0− ,
the remaining axioms in the ontology are in DL ALCH. These axioms are normalized
using a procedure identical to [11]. The result ontology O contains axioms of the forms
Ai v B j , A v ∃R.B, ∃R.A v B, A v ∀R.B, R v S , Na = {a} and R = R0− , where
d F
A, B are atomic concepts and R, S , R0 are atomic roles.
WSReasoner: A Prototype Hybrid Reasoner 5
Table 1. Rewriting Nominals in OWL 2
OWL 2 Syntax Equivalent Forms
Class Expressions
ObjectHasValue (R a) ∃R.{a}
ObjectOneOf (a1 . . . an ) {a1 } t . . . t {an }
Axioms
ClassAssertion (C a) {a} v C
SameIndividual (a1 . . . an ) {a1 } = . . . = {an }
DifferentIndividuals (a1 . . . an ) {ai } u {a j } = ⊥
1≤i< j≤n
ObjectPropertyAssertion (R a b) {a} v ∃R.{b}
NegativeObjectPropertyAssertion (R a b) {a} u ∃R.{b} v ⊥
4.2 Model-Theoretic View of the Strengthening Step
Before going into the details of the reasoning procedure, we give a model-theoretic
explanation of the motivation of the strengthening step. Given an ontology O, we want
to create its strengthened version O str which satisfies HO ⊆ H str . To achieve it, we try
to ensure that for each hA, Bi < H str , there is a certain model I’ of O str for Au¬B which
can be transformed to a model I of O and (A u ¬B)I , ∅, so that hA, Bi < HO . Such
models I’ and I can be constructed using the hypertableau calculus (abbreviated as HT-
calculus) [8]. In the following we first describe strengthening for nominals, followed by
strengthening for inverse roles.
4.2.1 Strengthening for Nominals
Example 1. Consider a normalized ontology O containing the following axioms:
A v ∃R.E (1) A v C (2) C v ∀R.D (3) E v Na (4) Na = {a} (5)
A v ∃S .Na (6) ∃S .D v F (7) F v B0 t B (8) D v G (9)
In Fig. 3 – 5 we give models of O, Owk and O str for the concept Au¬B constructed by
the HT-calculus. In the figures, each node x denotes an individual and its tags represent
the concepts that it belongs to, which we call labels of x. Each edge hx, yi denotes a role
relation between two individuals x and y, and its labels are the roles that it belongs to.
We say that a label B of x is added by an axiom α in a normalized ontology if B(x) is
added into the model by a derivation corresponding to α in the HT-calculus, e.g. A v B
corresponds to A(x) → B(x) and ∃R.A v B corresponds to R(x, y) ∧ A(x) → B(x), etc.
Fig. 3 is a model of Owk , which removes the axiom (5) from O. In the model both of
the individuals x2 , x3 have the label Na . To build a model of O based on the HT-calculus,
x2 and x3 need to be merged into one instance to satisfy the axiom (5). After that, labels
F and B0 of x1 will be added by the axioms (7) and (8), yielding the model I in Fig. 4.
Our strengthening step adds additional axioms Na v E and Na v D to Owk to
simulate the main effect of the merge operation in the HT-calculus, i.e. making all the
instances of Na have the same labels. With these axioms added, labels D, E and G are
added to x3 , and labels F and B0 of x1 can be further introduced by the HT-calculus
6 Weihong Song, Bruce Spencer, and Weichang Du
Fig. 3. Model of Owk Fig. 4. Model of O Fig. 5. Model of O str
without the nominal axiom (5). The resulting model I’ in Fig. 5 can be transformed to
I by simply merging the instances x2 and x3 without extra derivations.
To achieve the above-mentioned effect, we calculate the “important” labels appear-
ing on the instances of Na in the model of Owk , which we call major coexisting labels
of Na . For each instance x, such an important label is the label when x is created by
the HT-calculus or a label added by an axiom A v ∀R.B. In other words, these labels
are added at initialization time or through a derivation which takes a label on a prede-
cessor of x as a premise, thus they cannot be introduced based on x’s own labels. Note
that the label G of x2 in Fig. 3 is not a major coexisting label since it is added by the
axiom D v G. For each major coexisting label X of Na , we choose either Na v X or
Na u X v ⊥ as the strengthening axiom, so that X is either added to or prohibited on all
the instances of Na in the model I’ of O str . With these axioms added, all the instances
of Na in I’ are likely to have identical labels so that I’ can be easily transformed to I
to prove O 6|= A v B.
4.2.2 Strengthening for Inverse Roles Regarding inverse roles, the corresponding
derivation of an axiom R = R0− in HT-calculus adds R(x, y) if R0 (y, x) exists, or vice
versa. The new assertion R(x, y) may lead to the following types of further derivations:
(1) a label B is added to x by ∃R.A v B; (2) a label B is added to y by axioms A v ∀R.B;
(3) labels are added to edges through axioms R v S and S = S 0− . To simulate these
effects without deriving R(x, y) using R = R0− , the following types of axioms are added
respectively: (1) A v ∀R0 .B; (2) ∃R0 .A v B; (3) all the role subsumptions based on the
computed role hierarchy Hop . Similar axioms need to be added for the assertion R0 (y, x).
With these axioms added, the model I’ of O str can be transformed to a model I of O
by simply satisfying R = R0− without extra derivations. Notice that all the strengthening
axioms to handle inverse roles are implied by O, so we have O |= O str and H str ⊆ HO ,
thus H str = HO holds and no verifications are needed.
4.3 Classification Procedure
Algorithm 1 gives the overall classification procedure for an ALCHOI ontology using
the weakening and strengthening approach. In the procedure, MR is the main reasoner
that provides efficient classification on an ALCH ontology, while AR is the assistant
reasoner, which is slower but capable of classifying the original ALCHOI ontology
O. Function classify computes the class hierarchy.
After normalization, the algorithm computes the role hierarchy Hop . Line 3 and 4
compute the strengthened ontology Oistr for inverse roles, which has the same hierar-
chy as O. To classify the ALCHO ontology Oistr , we get its weakened and strengthened
WSReasoner: A Prototype Hybrid Reasoner 7
versions Owk and O str for nominals and classify them with MR, as shown in lines 5 to 8.
Computations of O+I and O+N will be explained in Sections 4.3.1 and 4.3.2. Subsump-
tions in H str \ Hwk are verified by AR in line 11 to 15. Note that if some A v ⊥ is
disproved in line 12, A v B needs to be verified for almost every B in NC . In this case
the workload of verification for AR may exceed that of classifying O, thus we choose
to use AR to get HO directly. Our approach does not add value in this case. Line 14
to 15 verifies each pair in H str \ Hwk one by one. The verification process can be further
improved using a procedure similar to the optimized KP alorithm [3].
Algorithm 1: Classify an ALCHOI ontology O using the hybrid approach
Input: An ALCHOI ontology O
Output: The classification hierarchy HO
1 preprocess and normalize O;
2 Hop := AR.classifyObjectProperties(O);
+
3 O := getStrAxiomsForInverseRoles(O, Hop );
I
+
4 Oistr := O ∪ O with inverse role axioms R = R removed;
0−
I
5 Owk := Oistr with nominal axioms Na = {a} removed;
+
6 ON := getStrAxiomsForNominals(Oistr , Hop );
7 Hwk := MR.classify(Owk );
+
8 H str := MR.classify(Owk ∪ ON );
>,⊥
9 remove any hA, Bi from Hwk and H str if A < NC or B < NC>,⊥ ;
10 HO := Hwk ;
11 foreach hA, ⊥i ∈ H str \ Hwk do
12 if AR.isSatisfiable(O, A) then return AR.classify(O);
13 else add hA, ⊥i into HO ;
14 foreach hA, Bi ∈ H str \ Hwk do
15 if not AR.isSatisfiable(O, A u ¬B) then add hA, Bi into HO ;
16 return HO
4.3.1 Strengthening for Inverse Roles Based on the discussions in Section 4.2, we
calculate the strengthening axioms O+I for inverse roles according to the following steps:
1. For each hR0 , S − i ∈ Hop where S − does not have an equivalent named role, intro-
duce a new named role S 0 for S − and update Hop .
2. Initialize O+I with all the subsumptions between named roles in Hop
3. for each hR, R0 i such that R = R0− is implied by Hop , if either of the following two
equivalent forms is used, add the other to O+I :
A v ∀R.B ⇔ ∃R0 .A v B
Here hR, R0 i and hR0 , Ri are treated as different pairs.
4.3.2 Strengthening for Nominals This section explains the calculation of strength-
ening axioms O+N for nominals. According to Section 4.2, for each nominal placeholder
8 Weihong Song, Bruce Spencer, and Weichang Du
Na , we need to compute its major coexisting label set LS Na , and choose to add Na v X
or Na u X v ⊥ into O+N for each X ∈ LS Na .
Algorithm 2: Calculate the potential major coexisting label set of Na in O
Input: Normalized ALCHOI ontology O and a concept Na ∈ NC
Output: Major coexisting label set LS Na
1 Initialize a queue Q with label Na ;
2 CoreNa := ∅; visited := ∅;
3 repeat
4 poll a label X from Q; d F
5 if X is not introduced by some Ai v M X and X < visited then
6 add X tod proc;
F
7 foreach Ai v M X ∈ O do add each Ai into Q;
8 foreach ∃S .Y v X ∈ O and hR, S i ∈ Hop and B v ∃R.Z ∈ O do
9 add B into Q;
10 foreach Y v ∀S .X ∈ O and hR, S i ∈ Hop and B v ∃R.Z ∈ O do
11 add Z to CoreNa ;
12 if X ∈ NC> or some B v ∃R.X ∈ O then add X to CoreNa ;
13 until Q is empty;
14 LS Na := CoreNa ;
15 foreach X ∈ CoreNa do
16 foreach B v ∃R.X ∈ O and hR, S i ∈ Hop and Y v ∀S .Z ∈ O do
17 add Z to LS Na ;
18 return LS Na
Algorithm 2 illustrates the computation of LS Na in Example 1. From line 3 to 13
we search for the potential core label set CoreNa of Na , i.e., the concepts that may label
an individual of Na when it is created by the HT-calculus. CoreNa is a subset of LS Na .
We search in the converse direction of the model construction process for the labels X
that may cause the appearance of label Na , which we denote by X 7→ Na . and put the
potential core labels into CoreNa . There are three cases that X is added to an individual
x according to the calculus:
d
Case 1: (Line 7) If X is added to x by the axiom Ai v M t X, then for every conjunct
condition Ai we have Ai 7→ X.
Case 2: (Line 8-9) If X is added to x to by the axiom ∃S .Y v X, then x has an S -
successor, which must be introduced by some B v R.Z provided that hR, S i ∈ Hop .
For every such B there is a potential that B 7→ X.
Case 3: (Line 10) X is added to x by the axiom Y v ∀S .X, then it must have an
S -predecessor in the model. Thus when x is created, the incoming role R satisfies
hR, S i ∈ Hop , and for all B v ∃R.Z, Z is a potential core label of x.
Line 12 checks whether X itself can be a core label. A core label can only be in-
troduced through: (1) the initialization step, for which X must be atomic in O; (2) an
individual-adding derivation, for which there must be some B v ∃R.X ∈ O.
WSReasoner: A Prototype Hybrid Reasoner 9
On line 15 to 17 we follow the model construction process to find other major
coexisting labels. Similarly to case 3 above, if x has a core label X added by the axiom
B v ∃R.X and hR, S i ∈ Hop , then Z may be added to X by the axiom Y v ∀S .Z.
The test on line 5 dprunes a search branch X in either of two cases: (1) X has been
visited. (2) An axiom Ai v M t X has been d used on the search path from Na to X. In
case (2), when the model expands, the axiom Ai v M t X has been satisfied and no
new labels that potentially introduces Na will be added.
We show the calculation of the strengthening axioms for Na in Example 1. Q is
initialized with Na . E is added to Q according to Case 1 based on the axiom E v Na .
When E is processed, it is added to CoreNa in line 12 and also to LS Na in line 14. D is
added to LS Na in the next loop from line 15 to 17, based on the axioms A v ∃R.E and
C v ∀R.D. Finally we choose to add Na v D and Na v E based on some heuristic rules.
Termination of the outer loop from line 3 to 13 is ensured by keeping a visited set
so that any label will only be processed at most once in the loop. Let nc and nax be the
number of concepts and axioms in O. One can see that the inner loop on line 7 runs
at most nax times, while the number of runs of the next two inner loops is bounded by
the number n2ax of pairs of axioms. So the worst-case complexity of the outer loop is
O(nc · n2ax ). The case is similar for the loop from 15 to 17. This procedure needs to be
invoked for each concept Na , the number of invocations is less than nc . Since nc ≤ nax
in the normalized ontology, the worst-case number of executions is polynomial in nax .
5 Evaluation
We have implemented our proposed approach in a prototype reasoner WSReasoner. We
use the consequence-based reasoner ConDOR r.12 as the main reasoner and the hyper-
tableau-based reasoner HermiT 1.3.64 as the assistant reasoner. ConDOR supports DL
SH (ALCH + transitivity axioms), and HermiT supports DL SROIQ(D), which is
more expressive than the ALCHOI. We compared the performance of WSReasoner
with the latest versions of mainstream reasoners, including tableau-based reasoners
HermiT 1.3.6, Fact++ 1.5.3 and Pellet 2.3.0, as well as a consequence-based reasoner
TrOWL 0.8.2. All the experiments were run on a laptop with an Intel Core i7-2670QM
2.20GHz quad core CPU and 16GB RAM running Java 1.6 under Windows 7. We set
the Java heap space to 12GB. We did not set the time limit.
We tried all the commonly used, widely available large and complex ontologies that
we have access to. Since none of these expressive ontologies are modeled in ALCHOI,
we had to make some adjustments. Galen5 and FMA-constitutionalPartForNS (FMA-
cPFNS) are currently available large and complex ontologies. We use three different
version of Galen, which are Full-Galen, Galen-Heart, and Galen-EL.6 We modify them
by introducing nominals. In Galen, the concepts starting with a lower case letter and
subsumed by SymbolicValueType could be nominals which are modeled as concepts.
For Galen-Heart and Galen-EL, we used published methods [7] to produce two versions
for each of them, which are Galen-Heart-YN1, Galen-Heart-YN2, Galen-EL-YN1, and
4
HermiT 1.3.6 build 1054, 04/18/2012 release
5
http://www.co-ode.org/galen/
6
http://code.google.com/p/condor-reasoner/downloads/list/
10 Weihong Song, Bruce Spencer, and Weichang Du
Galen-EL-YN2. In addition, we produced Galen-EL-LN1 by introducing norminals on-
ly for leaf N-concepts of Galen-EL; and also add disjunction into Full-Galen and pro-
duced Galen-Full-UnionN2.
We also used two smaller complex ontologies, Wine and DOLCE. All our onto-
logies were reduced to ALCHOI and can be downloaded from our website.7
Table 2. Comparison of classification performance
T: Time(seconds); MS: (# of subsumption pairs missing) / (# of total subsumption pairs)
Ontology Criteria (Hyper) tableau Consequence-based WSReasoner
HermiT Pellet FaCT++ TrOWL com-role fast-role
T 29.11 377.88 7.33 0.81 7.34 1.22
Wine MS 0/968 0/968 0/968 1/968 0/968 0/968
T 5.64 8.40 0.92 0.55 8.84 2.09
DOLCE MS 0/2595 0/2595 0/2595 390/2595 0/2595 0/2595
Galen- T 115.10 - - - 7.59 6.94
Heart-YN1 MS 0/45,513 - - - 0/45,513 0/45,513
Galen- T 63.52 - - - 9.50 7.19
Heart-YN2 MS 0/45,914 - - - 0/45,914 0/45,914
Galen-EL T 197,090 - - - 345,600+ 345,600+
-YN1 MS 0/431,990 - - - / /
Galen-EL T 289,637 - - - 38,350 38,272
-YN2 MS 0/457,779 - - - 0/457,779 0/457,779
Galen-EL T 188,018 - - - 771 755
-LN1 MS 0/431,990 - - - 0/431,990 0/431,990
Galen-Full T 604,800+ - - - 1625 1478
-UnionN2 MS / - - - x/(431,255+x) x/(431,255+x)
T 667,430 - - 429.65 21,362 45
FMA-cPFNS MS 0/481,967 - - 70/481,967 0/481,967 0/481,967
Note: “-” entry means that the reasoner was unable to classify the ontology due to some problems.
“/” entry means the number is not available.
The results of our experiment are shown in Table 2. Since the time limit is not
set, some tasks may take several days or more to finish. The ‘+’ sign indicates the
tasks are not finished within the time shown before ‘+’. We also report the number of
missed subsumptions, since some of the reasoners are not complete, such as TrOWL
and possibly ours. # represents number in Table 2 and 3. The total number includes all
pairs of subsumptions between any A, B ∈ NC>,⊥ except for ⊥ v A and A v >. The
complete result is obtained from HermiT. For Galen-Full-UnionN2, HermiT does not
get the results, while WSReasoner gets 431,255 subsumptions, but we do not know the
number of missed pairs, so we denote it by x.
Since computing complete role hierarchy Hop takes a considerable amount of time
for our assistant reasoner HermiT, we implement two versions of WSReasoner. The
version ‘fast-role’ simply computes the reflexive-transitive relations between roles,8
while the version ‘com-role’ request HermiT for a complete Hop on O.
7
http://isew.cs.unb.ca/wsreasoner/resources/ontologies/
8
to simplify implementation, we extract all object property axioms and request HermiT for Hop
WSReasoner: A Prototype Hybrid Reasoner 11
As we can see in Table 2, WSReasoner is able to classify eight of nine ontologies,
and get no fewer subsumptions than any other reasoners. On various FMA-cPFNS and
versions of Galen ontologies, WSReasoner outperforms all the other reasoners consid-
erably except for Galen-EL-YN1, on which the verification stage has more than 320,000
pairs to verify, however, it takes only several minutes to determine that WSReasoner is
likely to be slower than HermiT. For the two smaller ontologies Wine and DOLCE, the
fast-role approach still outperforms HermiT and Pellet and even com-role outperforms
the two reasoners on Wine.
Table 3. Statistics of WSReasoner
Added-axioms: # of axioms in O+N Add-pairs: # of pairs in H str \ Hwk
True-pairs: # of pairs verified to be correct Verify-time: verification time
fast-role-T: The role classification time using the fast-role approach (Seconds)
com-role-T: The role classification time using the comp-role approach (Seconds)
Ontology Wine DOLCE Galen- Galen- Galen- Galen- Galen- Galen-Full FMA
Heart-YN1 Heart-YN2 EL-YN1 EL-YN2 EL-LN1 -UnionN2 -cPFNS
Added-Axioms 36 95 2 50 79,594 981 12 1100 0
Add-Pairs 0 0 2 403 323,294 28,287 45 259 0
True-Pairs 0 0 2 403 - 25,789 0 0 0
fast-role-T 0.16 0.77 0.639 0.56 1.60 1.25 1.63 2.82 0.39
com-role-T 6.50 7.37 2.09 2.53 22.99 19.57 19.37 15.30 21322.54
Verify-Time 0 0 3.39 3.84 - 38,252 649.24 793.26 0
Table 3 shows some statistics of our reasoner on different phases. FMA-cPFNS only
needs one round of classification. Wine and DOLCE need two rounds of classification
but no verifications are needed, which indicates the nominals does not bring any new
subsumptions. The number of strengthening axioms added for these ontologies varies a
lot. The verification time becomes larger as the size of H str \ Hwk increases. Comparing
the role classification time, fast-role is considerably faster than com-role, especially for
the ontology FMA-cPFNS on which the com-role approach takes 5 hours to finish. In
summary, the main factors affecting the reasoning time are: (1) The approach to choose
for role hierarchy calculation. (2) the number of pairs in H str \ Hwk .
To evaluate the performance on other existing ontologies, we also ran WSReasoner
on a test suite provided by ORE 2012.9 We used the RDF version of the ontologies
in the OWL DL and OWL EL datasets, which contains 107 and 8 real-world onto-
logies respectively. We set the maximum Java heap space to 1GB and add an additional
JVM setting -DentityExpansionLimit=480000 to ensure successful loading of all
the ontologies using OWL API. The time limit is set to 1 hour.
The results are shown in Table 4. The columns “OWL DL” and “OWL EL” refer
to the two datasets, while “DL-ALCHOI” and “EL-ALCHOI” refer to the ALCHOI
ontologies in these datasets, respectively. As seen in the table, all the ALCHOI onto-
logies have been correctly classified. Complete hierarchies of 5 ontologies in the OWL
9
http://www.cs.ox.ac.uk/isg/conferences/ORE2012/datasets/classification.zip
12 Weihong Song, Bruce Spencer, and Weichang Du
DL dataset are not obtained because their languages are beyond ALCHOI. The largest
ontology gazetteer in the OWL DL dataset (containing 150979 classes) causes a out-
of-memory exception.
Table 4. Evaluation results on the ORE test suite
ALT: Average Loading Time ART: Average Reasoning Time
TOTAL: # of ontologies in the dataset
CORRECT: # of correctly classified ontologies
INCORRECT: # of incorrectly classified ontologies
NO-REF: # of ontologies with no reference results
EXCEPTION: # of ontologies that cause an exception
TIMEOUT: # of ontologies that cause a timeout
Outcomes DL-ALCHOI OWL DL EL-ALCHOI OWL EL
ALT (ms) 105 323 320 454
ART (ms) 632 1263 277 503
TOTAL 34 107 6 8
CORRECT 18 47 5 6
INCORRECT 0 5 0 0
NO-REF 16 54 1 2
EXCEPTION 0 1 0 0
TIMEOUT 0 0 0 0
6 Conclusions and Future Work
We present an approach combining two reasoners based on ontology weakening and
strengthening to classify large and complex ontologies, for which tableau-based rea-
soners may take a long time or use much memory while consequence-based reasoners
cannot support all the constructors in the target language. We use a consequence-based
reasoner supporting a DL less expressive than the target language as the main reason-
er to do the majority (sometimes all) of the work, and a more expressive but slower
tableau-based reasoner to assist it in verifying the results. In the experiment dataset
shown in Table 2, WSReasoner’s results show better efficiency than the tableau-based
reasoners in most large and complex ontologies, and no fewer subsumptions than other
reasoners except for one ontology for which the result is not obtained by WSReasoner.
The weaknesses of this WSreasoner for ALCHOI are: (1) the complete role hier-
archy classification may take a lot of time; (2) if the number of pairs verified is large,
the procedure still takes a lot of time in the verification stage. The advantages of the WS
approach are: (1) it may achieve better classification efficiency than tableau-based rea-
soners; (2) it extends the capability of consequence-based reasoners; (3) the reasoners
underneath can be customized to classify different ontologies.
In the future, we will try to prove the theoretical completeness of this weakening
and strengthening approach for ALCHOI ontology classification while optimizing the
WSReasoner: A Prototype Hybrid Reasoner 13
algorithm. We will further try to apply the weakening and strengthening approach based
on different reasoners and address more constructors for more expressive languages.
References
1. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: IJCAI 2005, Proceedings of
the 19th International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK,
July 30-August 5, 2005. pp. 364–369 (2005)
2. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.: The Description
Logic Handbook: Theory, Implementation, and Applications. Cambridge Univ Pr (2010)
3. Glimm, B., Horrocks, I., Motik, B., Stoilos, G.: Optimising ontology classification. In: Patel-
Schneider, P., Pan, Y., Hitzler, P., Mika, P., Zhang, L., Pan, J., Horrocks, I., Glimm, B. (eds.)
The Semantic Web - ISWC 2010, Lecture Notes in Computer Science, vol. 6496, pp. 225–
240. Springer Berlin / Heidelberg (2010)
4. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. Journal of Automated
Reasoning 39, 249–276 (October 2007)
5. Kazakov, Y.: Consequence-driven reasoning for horn SHIQ ontologies. In: IJCAI 2009,
Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena,
California, USA, July 11-17, 2009. pp. 2040–2045 (2009)
6. Kazakov, Y., Krötzsch, M., Simanc̆ı́k, F.: Concurrent classification of EL ontologies. In:
ISWC 2011, 10th International Semantic Web Conference, Bonn, Germany, October 23-27,
2011. Lecture Notes in Computer Science, vol. 7031, pp. 305–320. Springer (2011)
7. Kazakov, Y., Krötzsch, M., Simančı́k, F.: Practical reasoning with nominals in the EL family
of description logics. In: Proceedings of the 13th International Conference on Principles of
Knowledge Representation and Reasoning (KR’12) (2012)
8. Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics. Journal
of Artificial Intelligence Research 36, 165–228 (September 2009)
9. Ren, Y., Pan, J.Z., Zhao, Y.: Soundness preserving approximation for TBox reasoning. In:
AAAI 2010, Proceedings of the 24th AAAI Conference on Artificial Intelligence, Atlanta,
Georgia, USA, July 11-15, 2010. AAAI Press 2010 (2010)
10. Selman, B., Kautz, H.: Knowledge compilation and theory approximation. Journal of the
ACM (JACM) 43(2), 193–224 (1996)
11. Simanc̆ı́k, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond horn onto-
logies. In: IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial
Intelligence, Barcelona, Catalonia, Spain, 2011. pp. 1093–1098 (July 2011)
12. Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A Practical OWL-DL Rea-
soner. Web Semantics: Science, Services and Agents on the World Wide Web 5(2), 51–53
(2007)
13. Tsarkov, D., Horrocks, I.: FaCT++ Description Logic Reasoner: System Description. Auto-
mated Reasoning pp. 292–297 (2006)