In the ontology classification task, consequence-based reasoners are typically significantly faster while tableau-based reasoners can process more expressive DL languages. However, both of them have di culty to classify some available large and complex ALCH OI ontologies with complete results in acceptable time. We present a prototype hybrid reasoning system WSReasoner, which is built upon and takes advantages of both types of reasoners to provide e cient classification service. In our proposed approach, we approximate the target ontology O by a weakened version Owk and a strengthened version Ostr, 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 Ostr is to produce a superset of subsumptions of O. Additional subsumptions derived from Ostr may be unsound, so they are further verified by a tableau-based assistant reasoner. For the ALCH OI ontologies in our experiment, except for one for which WSReasoner has not obtained the result, (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 ALCH OI ontologies are large and complex.
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 subsumption 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. Initially developed for the family of tractable DLs like EL++ [1], these procedures were later extended to Horn-SH IQ [5] and ALCH [11] while preserving optimal computational 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.
We present a hybrid reasoning system that takes the advantages of both types of reasoners for e cient classification on large and complex ontologies in expressive DLs. Here “complex ontologies” refers to the ontologies which contains a considerable 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 ontology 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 axioms to simulate the e ects of those removed axioms in a model expansion process, constructing the strengthened ontology Ostr. 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 Ostr to contain all the subsumptions in O. In Fig. 1, the results of classification, named the class hierarchy, for ontology O, Owk, and Ostr are denoted by HO, Hwk and Hstr respectively. The subsumptions pairs in Hstr 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 accepts the full language of O, the assistant reasoner; it is potentially slower than the main reasoner.
Our main contributions are as follows:
a new hybrid reasoning approach by combining the tableau-based and consequencebased reasoning procedures for e cient classification on large and complex ontologies. Concretely, the hybrid reasoning is based on a weakening and strengthening approach and applied to classifying ALCH OI 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 ALCH OI, which is not fully supported by any current consequence-based reasoner. We evaluate our procedure with nine available, practical ALCH OI 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
The syntax of ALCH OI uses mutually disjoint sets of atomic concepts NC, atomic roles NR and individuals NI . The set of roles is NR [ fR j R 2 NRg. The set of concepts contains A, >, ?, :C, C u D, C t D, 9R:C, 8R:C, fag, for > the top concept, ? the bottom concept, A an atomic concept, C and D concepts, R a role, a an individual. We define NC> = NC [ f>g and N>;? = NC> [ f?g. An ontology O consists of a set of general
C 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 2 NC to a set AI I, each R 2 NR to a relation RI I I and each a 2 NI an element aI 2 I. The interpretation of concepts are defined in [2]. An interpretation I satisfies axioms C v D and R v S if CI 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 j= .
An ontology classification task is to compute the class hierarchy HO containing all the pairs hA; Bi such that A; B 2 N>;? and O j= A v B. We define the role hierarchy Hop
C as the pairs hR; S i such that R; S 2 NR [ fR j R 2 NRg and O j= 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 Ostr 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 Ostr need to be checked, analogously as queries lb that return “yes” need to be checked.
TrOWL [9] is a soundness-preserving approximate reasoner o ering tractable classification for SROIQ ontologies by an encoding into EL++ with additional data structures. Instead of merely preserving soundness, our algorithm also aims to achieve completeness, although we have not yet proven it. Another di erence lies in that the classification 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
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 supported 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 axioms in O n 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. – 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 di erence between two concept hierarchies produced by the first and second round of classifications, Hwk and Hstr 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 interactions with each other. 4
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 explains preprocessing and normalization. Section 4.2 gives a model-theoretic illustration of the weakening and strengthening approach using an example. And section 4.3 provides the details of the overall procedure and strengthening algorithms. 4.1
In the preprocessing phase, we rewrite the original ontology to make nominals and inverse roles occur only in the axioms of the forms Na = fag 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 Table 1. After that, for each fag, we replace all its occurrences by a new concept Na and add an axiom Na = fag. We call Na a nominal placeholder for a in the following sections. 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 = fag 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 d Ai v F B j, A v 9R:B, 9R:A v B, A v 8R:B, R v S , Na = fag and R = R0 , where A; B are atomic concepts and R; S ; R0 are atomic roles. 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 Ostr which satisfies HO Hstr. To achieve it, we try to ensure that for each hA; Bi < Hstr, there is a certain model I’ of Ostr for A u :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 HTcalculus) [8]. In the following we first describe strengthening for nominals, followed by strengthening for inverse roles.
Example 1. Consider a normalized ontology O containing the following axioms:
A v 9R:E (
A v C (
C v 8R:D (
E v Na (
Na = fag (
In Fig. 3 – 5 we give models of O, Owk and Ostr 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 9R:A v B corresponds to R(x; y) ^ A(x) ! B(x), etc.
Fig. 3 is a model of Owk, which removes the axiom (
Our strengthening step adds additional axioms Na v E and Na v D to Owk to simulate the main e ect 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 Fig. 3. Model of Owk
Fig. 4. Model of O
Fig. 5. Model of Ostr
without the nominal axiom (
To achieve the above-mentioned e ect, we calculate the “important” labels
appearing 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 8R:B. In other words, these labels
are added at initialization time or through a derivation which takes a label on a
predecessor 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 Ostr. 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 6j= 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:
(
Algorithm 1 gives the overall classification procedure for an ALCH OI ontology using the weakening and strengthening approach. In the procedure, MR is the main reasoner that provides e cient classification on an ALCH ontology, while AR is the assistant reasoner, which is slower but capable of classifying the original ALCH OI 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 hierarchy as O. To classify the ALCH O ontology Oistr, we get its weakened and strengthened versions Owk and Ostr for nominals and classify them with MR, as shown in lines 5 to 8. Computations of O+ and O+N will be explained in Sections 4.3.1 and 4.3.2. Subsumptions in Hstr n Hwk Iare 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 Hstr n 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 ALCH OI ontology O using the hybrid approach Input: An ALCH OI ontology O
Output: The classification hierarchy HO 1 preprocess and normalize O; 2 Hop := AR.classifyObjectProperties(O); 3 O+I := getStrAxiomsForInverseRoles(O, Hop); 4 Oistr := O [ O+I with inverse role axioms R = R0 removed; 5 Owk := Oistr with nominal axioms Na = fag removed; 6 O+N := getStrAxiomsForNominals(Oistr, Hop); 7 Hwk := MR.classify(Owk); 8 Hstr := MR.classify(Owk [ O+N ); 9 remove any hA; Bi from Hwk and Hstr if A < N>;? or B < NC>;?; C 10 HO := Hwk; 11 foreach hA; ?i 2 Hstr n Hwk do 12 if AR.isSatisfiable(O; A) then return AR.classify(O); 13 else add hA; ?i into HO; 14 foreach hA; Bi 2 Hstr n 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+ for inverse roles according to the following steps:
I 1. For each hR0; S i 2 Hop where S does not have an equivalent named role, introduce a new named role S 0 for S and update Hop. 2. Initialize O+ with all the subsumptions between named roles in Hop 3. for each hR;IR0i 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 8R:B , 9R0:A v B
4.3.2 Strengthening for Nominals This section explains the calculation of strengthening axioms O+N for nominals. According to Section 4.2, for each nominal placeholder 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 2 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: Case 1: (Line 7) If X is added to x by the axiom d 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 9S :Y v X, then x has an S successor, which must be introduced by some B v R:Z provided that hR; S i 2 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 8S :X, then it must have an S -predecessor in the model. Thus when x is created, the incoming role R satisfies hR; S i 2 Hop, and for all B v 9R: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
introduced through: (
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 9R:X and hR; S i 2 Hop, then Z may be added to X by the axiom Y v 8S :Z.
The test on line 5 prunes a search branch X in either of two cases: (
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 9R:E and C v 8R: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 na2x 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
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 hypertableau-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 ALCH OI. 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 ALCH OI, we had to make some adjustments. Galen5 and FMA-constitutionalPartForNS (FMAcPFNS) are currently available large and complex ontologies. We use three di erent 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/ Galen-EL-YN2. In addition, we produced Galen-EL-LN1 by introducing norminals only for leaf N-concepts of Galen-EL; and also add disjunction into Full-Galen and produced Galen-Full-UnionN2.
We also used two smaller complex ontologies, Wine and DOLCE. All our ontologies were reduced to ALCH OI and can be downloaded from our website.7
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 2 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
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 considerably 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.
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 Added-Axioms 36
Add-Pairs 0 True-Pairs 0 fast-role-T 0.16 com-role-T 6.50 Verify-Time 0
Table 3 shows some statistics of our reasoner on di erent 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 Hstr n 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 a ecting the reasoning time are: (
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 ontologies 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 ALCH OI ontologies in these datasets, respectively. As seen in the table, all the ALCH OI ontologies 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 DL dataset are not obtained because their languages are beyond ALCH OI. The largest ontology gazetteer in the OWL DL dataset (containing 150979 classes) causes a outof-memory exception. We present an approach combining two reasoners based on ontology weakening and strengthening to classify large and complex ontologies, for which tableau-based reasoners 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 reasoner 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 e ciency 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 ALCH OI are: (
In the future, we will try to prove the theoretical completeness of this weakening and strengthening approach for ALCH OI ontology classification while optimizing the algorithm. We will further try to apply the weakening and strengthening approach based on di erent reasoners and address more constructors for more expressive languages.