On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (Extended Version)
This addresses the need for better explainability tools in ontology engineering, particularly for users working with expressive description logics, though it appears incremental as it builds on existing proof concepts.
The paper tackles the problem of limited tool support for explaining inferences in expressive description logic ontologies by introducing EVEE-LIBS, a Java library for computing proofs up to ALCH, and EVEE-PROTEGE plugins for displaying them in Protégé, along with a glimpse of the advanced EVONNE application.
When working with description logic ontologies, understanding entailments derived by a description logic reasoner is not always straightforward. So far, the standard ontology editor Protégé offers two services to help: (black-box) justifications for OWL 2 DL ontologies, and (glass-box) proofs for lightweight OWL EL ontologies, where the latter exploits the proof facilities of reasoner ELK. Since justifications are often insufficient in explaining inferences, there is thus only little tool support for explaining inferences in more expressive DLs. In this paper, we introduce EVEE-LIBS, a Java library for computing proofs for DLs up to ALCH, and EVEE-PROTEGE, a collection of Protégé plugins for displaying those proofs in Protégé. We also give a short glimpse of the latest version of EVONNE, a more advanced standalone application for displaying and interacting with proofs computed with EVEE-LIBS.