From justifications towards proofs for ontology engineering

Justifications are currently the dominant form of explanation provided by ontology engineering environments, especially those focused on the Web Ontology Language (OWL). However, justifications for entailments in real ontologies can be very difficult or impossible for a wide range of people to understand. In essence, justifications are merely the premises of a proof and, as such, do not articulate the, often non-obvious, reasoning which connect those premises with the conclusion. This paper looks at moving towards proofs to solve this problem. Since there are many naturally occurring justifications that people can understand, the ultimate goal is to create justification oriented proofs. The foundation of these proofs is justification lemmatisation, which is presented in this paper.