A Multi-reasoner, Justification-Based Approach to Reasoner Correctness
OWL 2 DL is a complex logic with reasoning problems that have a high worst case complexity. Modern reasoners perform mostly very well on naturally occurring ontologies of varying sizes and complexity. This performance is achieved through a suite of comple
- PDF / 201,682 Bytes
- 16 Pages / 439.37 x 666.142 pts Page_size
- 40 Downloads / 186 Views
Abstract. OWL 2 DL is a complex logic with reasoning problems that have a high worst case complexity. Modern reasoners perform mostly very well on naturally occurring ontologies of varying sizes and complexity. This performance is achieved through a suite of complex optimisations (with complex interactions) and elaborate engineering. While the formal basis of the core reasoner procedures are well understood, many optimisations are less so, and most of the engineering details (and their possible effect on reasoner correctness) are unreviewed by anyone but the reasoner developer. Thus, it is unclear how much confidence should be placed in the correctness of implemented reasoners. To date, there is no principled, correctness unit test-like suite for simple language features and, even if there were, it is unclear that passing such a suite would say much about correctness on naturally occurring ontologies. This problem is not merely theoretical: Divergence in behaviour (thus known bugginess of implementations) has been observed in the OWL Reasoner Evaluation (ORE) contests to the point where a simple, majority voting procedure has been put in place to resolve disagreements. In this paper, we present a new technique for finding and resolving reasoner disagreement. We use justifications to cross check disagreements. Some cases are resolved automatically, others need to be manually verified. We evaluate the technique on a corpus of naturally occurring ontologies and a set of popular reasoners. We successfully identify several correctness bugs across different reasoners, identify causes for most of these, and generate appropriate bug reports and patches to ontologies to work around the bug. Keywords: OWL
1
· Reasoning · Debugging · Justifications
Introduction
A key advantage of expressive description logic ontologies (such as those encoded into OWL 2 DL) is that automated reasoners help. As often stated, reasoners make implicit knowledge explicit and this has benefits both at development time and at run time. One of the most obvious development time uses is for debugging ontologies. Reasoners detect faulty entailments (e.g., contradictions or unsatisfiable classes) and are a key component in explaining them. At runtime, c Springer International Publishing Switzerland 2015 M. Arenas et al. (Eds.): ISWC 2015, Part II, LNCS 9367, pp. 393–408, 2015. DOI: 10.1007/978-3-319-25010-6 26
394
M. Lee et al.
reasoners enable new sorts of functionality such as post-coordination [7,11,12] of terminologies as well as the discovery of new knowledge [17] or on the fly data integration [3]. Reasoners are complex pieces of software and their behaviour is opaque even to experts. Modern ontologies are typically too large and complex for any reasonable verification of the reasoners behaviour: Indeed, we rely on reasoners to help us manage those ontologies in the first place. Thus, we need techniques to help verify reasoner correctness. This is not merely a theoretical issue (as bug lists for various reasoners attest). The complexity of the impleme
Data Loading...
