DL reasoners are complex pieces of software that work on even more complex input which makes manual veri cation di cult. A single ontology can have hundreds or thousands of classes and thus its classi cation involve an unsurveyable number of subsumption tests. We propose a new method for debugging classi cation across multiple reasoners which employs justi cations generated from the set of entailments that reasoners disagree upon to determine the cause of the disagreement.
One of the major advantages of description logic reasoning are the sound and complete decision procedures for the known fragments that underpin OWL 2 and its various pro les. However, implementing these procedures can be very di cult due to inter-related optimisations and language speci c limitations. It is very likely that no implementation is actually correct for all legal inputs. We have found that, in practice, reasoners do disagree on particular entailments in the inferred class hierarchy. The complexity of the implementation makes a formal veri cation of correctness, or even a generation of a non-arbitrary set of automated unit tests, a near impossibility. Thus, it is di cult to resolve disputes.
Majority voting (MV) is a resolution method used in reasoner competitions [4]. When a disagreement occurs over the inferred class hierarchy, the verdict of the majority of reasoners is taken as truth. In case of a tie, the correct reasoner is selected at random. This method has the key problem that it is not inherently sensitive to the truth of the matter.
We present a novel semi-automated method to determine reasoner correctness and narrow down potential causes of disagreement amongst a set of dissenting reasoners in an e cient manner. We have evaluated our method using a corpus of BioPortal ontologies.
Throughout, we denote R a description logic reasoner and E (O; R) the set of atomic subsumptions found by R (the class hierarchy ). J is a justi cation for O j= if J O, J j= and there is no J 0 J such that J 0 j= . We call a tuple < O; ; J ; Rjust; R > a case, where Rjust is the reasoner that generated the justi cation J for the entailment and R is the reasoner that veri ed it. Aside from these notions we assume a basic familiarity with description logics, OWL and reasoners (see [1]).
The method: First, for a given ontology O, we ask reasoners R1; :::; Rm, denoted R, to compute the E (O; Ri) for all Ri 2 R. From these, we compute the set of disagreed upon entailments, denoted D, by taking the union of all inferred class hierarchies and removing the intersection of them, S E (O; Ri)n T E (O; Ri).
Fix some n 2 N, as the upper bound on the number of generated justi cations. For each given entailment 2 D and every Ri 2 R, we generate a sequence of up to n many justi cations J1; J2; :::Jn. Note that we attempt to generate justi cations with all reasoners, including the ones for which 62 E (O; Ri).
For each justi cation Ji for and each reasoner Ri 2 R1 we check whether
follows directly from the given justi cation (justi cation veri cation). We then
classify all cases according to one of four categories. (
Corpus, Reasoners and Machines: For the experiment the OWL API (v. 3.5.0) implementations [6] of four state of the art reasoners were used: FaCT++ 1.6.3 [9], JFact 1.2.3, Pellet 2.3.1 [7] and HermiT 1.3.8 [3]. Aside from the fact that these are popular, FaCT++ and JFact were also picked because of their similarity, in an attempt to see if that similarity would produce any change to the MV and the results from the method. Moreover, the number of reasoners were set to 4 to provide enough variation between reasoners, but also to include the possibility of inducing a draw of two teams between them. Our corpus is a snapshot of 339 BioPortal ontologies (January 2015). All experiments are performed on a desktop computer running 4 i5-3479 CPU at 3.20 GHz with a 64 bit Ubuntu 14.04.
Identifying potential ontologies: From our corpus, we ltered out those ontologies that were merely RDFS or AL and the ones that do not fall under 1 For reliability, we let reasoners verify their own justi cations. OWL 2 DL. For the remaining 240, we computed the inferred class hierarchy (1 hour timeout) for all four reasoners. We excluded a further 80 ontologies, for which there was a timeout. The inferred hierarchies were normalised using default techniques for dealing with owl:Nothing, owl:Thing, atomic subsumptions and equivalent classes. For the 160 ontologies that remained, the reasoners agreed in 155 cases and disagreed in 5.
Identifying and classifying problem cases: For the remaining 5 ontologies, we generate and verify justi cations according to the method described above. We used the OWL Explanation Framework by Horridge [5]2 to generate explanations for each 2 D. For performance reasons, we generate only one justi cation per reasoner per entailment.
Each explanation is stored in .owl format allowing us to reload them to check
them against the reasoners and if needed, perform direct evaluation. For direct
evaluation cases, we generate a human readable version of the justi cation.
Testing hypotheses and generating patches: We test four hypotheses that
emerged from initial observations we will describe in more depth later: (
The 5 ontologies in our in-depth experiment were the Biological Collections Ontology (BCO), the Gene Regulation Ontology (GRO), the Sysmo Jerm Ontology of Systems Biology for Micro Organism (JERM), the Clusters of Orthologous Groups Cog Analysis Ontology (CAO) and the Cell Culture Ontology (CCONT).
Across these 5 ontologies there was one instance of total disagreement in the Class Hierarchy and 4 partial majorities. With respect to the total disagreement, it was found that 3 out of the 4 reasoners veri ed a justi cation for an entailment missing from their class hierarchy. HermiT, at least for our small set, did not exhibit any buggy behaviour. Table 1 shows for each ontology and reasoner R and ontology O: { Was the reasoner part of the majority (MAJ) according to the MV method? { Did total disagreement (tie on Class Hierarchy level) occur? (DIS) { If there was an unclear entailment in D (possible bug /consistent no) involving R, was the reasoner generating the justi cation (TIE (J )) or verifying it (TIE (R))? { Was there one or more case for R which implicated a bug (BUG)? { Does the verdict di er from simple majority voting (d 2MV)? 2 https://github.com/matthewhorridge/owlexplanation
As we can see, BCO produced at least one unclear case. According to MV, FaCT and HermiT's inferred hierarchy would be in the majority. However Pellet produced unclear consistent no cases, which meant that we needed further analysis to determine which entailment was correct. Expert review showed that Pellet in fact failed to entail something correctly, as detailed in Section 4.1. In the case of the CAO ontology (total disagreement), we could identify clear bug cases for all reasoners except HermiT. A MV based technique would chose the victor randomly, which disadvantages HermiT. Reasoning over the other three ontologies each produced a majority that we could successfully provide further con dence for. For each, any dissenting reasoner was found to have produced a bug case and hence missed an entailment in its overall class hierarchy. 4.1
Analysis of Errors and Method for Patching
Of the 5336 cases generated by our method, 3718 were classed as consistent
yes, 1590 were classed as bug and 28 as consistent no. A further diagnostic
investigation was carried out on the 1618 error cases. This diagnosis found four
di erent types of problem for the reasoners. These are, (
This suggests a pre-processing bug on the part of FaCT++ and JFact. Of the bug cases, 1440 cases (approximately 90 %) rely upon these 28 axioms. This suggests that the vast majority of our bug cases are down to this error.
Further support for this hypothesis comes from analysis of the overall cases. 400 out of the total 5336 cases had justi cations of size 1. 4640 require these 400 cases to hold in the sample overall. This suggests that most of work was generated by FaCT++ and JFact failing to entail the result.
Data Type errors: FaCT++, JFact From the consistent no cases, we found two justi cations produced by FaCT and JFact that asserted a particular class was unsatis able. Direct examination showed that the class Decrease was classi ed as unsatis able because of the speci cations of the data type.
Decrease had for its data property polarity a speci ed datatype of rdf:PlainLiteral. This was distinct from the speci ed range of the polarity datatype, which were all xs:string. The actual possible value was correct, but the types di ered. According to W3C speci cations on plain literals, such a substitution is allowed: rdf plain literals should be interpreted as xs:strings [10]. Consequently, \negative" cast as plainLiteral would be accepted as a string. This suggested that JFact and FaCT++ had problems with particular data types. We veri ed this fact with a pair of minimal test cases.
Wrongly Missing Entailment: Pellet The 24 additional cases classed as consistent no were all generated by Pellet asserting that a particular entailment did not follow from a given justi cation. These cases could be collapsed into 8 unique justi cations (in-between reasoner redundancy). Interestingly, each of these justi cations took on a similar structural form.
All 8 justi cations were veri ed as correct for their entailment (expert review). They had structural similarities and upon examination we discovered them to have class names from each entailment also occurring in the axioms of justi cations for all other entailments. Because of this interaction, we found that inserting one of these missing entailments removed the disagreements and forced Pellet to produce the same Class Hierarchy as the other reasoners. In this case inserting IAO 109 v BF O 40 into the ontology allowed Pellet to infer the correct Class Hierarchy and eliminate all problematic cases from the ontology. This was as precise as we were able to point to the problematic area. Note that this produces an O0 = O [ f g on which all reasoners agree, but where O0 is not necessarily equivalent to O.
Classi cation bugs: Pellet All bug cases generated by Pellet were found to have justi cations of size 5 and to have entailments of the form A v CAO 323 (the RHS is a named class in the CAO). These similarities made us suspect that the justi cations might be structurally similar and possibly share axioms.
Checking the intersection of all the justi cations produced three shared axioms, Inverse(CAO 52; CAO 59), CAO 55 v 9CAO 59:CAO 323, CAO 323 CAO 48 u 8CAO 52:CAO 171.
We suspected that one of these axioms caused Pellet the di culty. We singled out the problematic axiom with the following procedure: for a given set of justi cations J1; :::Jn take S = Ti Ji. For each 2 S and for each reasoner Rj infer the class hierarchy from O0 := O n . If no disagreements on the Class Hierarchy occur then stop. We call the removal of a patch for the problem case.
The problematic axiom was singled out as CAO 55 v 9CAO 59:CAO 323. This provided a minimal axiom that a developer can use to understand the problematic reasoner behaviour. Note that as above, it might be that O0 6 O. 5
One important consequence of our justi cation based method is its implications for majority voting. In two of the cases we found reasons to suspect that the majority (or lack of) might lead to wrong reasoners being classi ed as \correct". Moreover, we could produce information to justify the choices picked through our method and those cases where our method agreed with MV. The evidence shows a clear di erence between the method stipulated and MV.
A general shortcoming of this system is that it does not catch all errors generated by the reasoners in particular those where the reasoners are all in agreement (which is the majority of the time). A more arti cial problem is our restriction to a single justi cation per reasoner entailment pair. This problem is avoidable with greater computational resources.
To our knowledge, there is little similar work. The JustBench benchmarking methodology [2], veri es the justi cations being used as benchmarks by cross checking them against all reasoners (this also emerges naturally when benchmarking). Similar work for automated reasoners has been performed with respect to queries [8]. The authors create test units (A-Boxes representations of the query) to form a test base. For certain benchmark ontologies that are used to assess reasoners, this provides a metric that evaluates the completeness of the reasoners. Importantly they also stress the need for such methods to be invariant or independent of the ontology being tested against.
In this paper, we have presented a justi cation based method to reliably identify bugs in the classi cation algorithm of OWL reasoners. Our method allows us to narrow down possible sources of bugs, providing a starting point for reasoner debugging. We have evaluated the method in a medium sized setting and showed that it functions as desired. We are now currently evaluating the feasibility of the method on a larger scale.
In the future, we would like to provide the method as a web service. Developers would be able to test their reasoners against a set of standard reasoners and then obtain cases that pinpoint potential bugs consisting of justi cations, missing entailments and ontology patches (that make the problem disappear).