Understanding Justifications for Entailments in OWL

Presented at: 8th International Semantic Web Conference (ISWC2009)

by Matthew Horridge, Bijan Parsia, Ulrike Sattler

Webpage: http://kcap09.stanford.edu/share/posterDemos/138/index.html
Webpage: http://kcap09.stanford.edu/share/posterDemos/138/paper138.pdf
Webpage: https://github.com/lidingpku/iswc-archive/raw/master/paper/iswc-2009-poster/138/paper138.pdf

Recent work in explanation of entailments in ontologies has focused on justifications and their variants. While in many cases, just presenting the justification is sufficient for user understanding, and in all cases justifications are much better than nothing, we have empirically identified cases where understanding how a justification supports an entailment is inordinately difficult. Indeed there are naturally occurring justifications that people, with varying expertise in OWL, cannot understand. To address this problem, we have developed a novel conceptual framework for justification oriented proofs. Given a justification for an entailment in an ontology, intermediate inference steps, called lemmas, are automatically derived, that bridge the gap between the axioms in the justification and the entailment. The proof shows in a stepwise way how the lemmas and ultimately the entailment follow from the justification. At the heart of the framework is the notion of a ``complexity model'', which predicts how easy or difficult it is for a user to understand a justification, and is used for selecting the lemmas to insert into a proof. This poster and demo presents this framework backed by a prototype implementation.

Keywords: Semantic Web

Resource URI on the dog food server: http://data.semanticweb.org/conference/iswc/2009/paper/poster_demo/138

Explore this resource elsewhere: