On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (Extended Version)

TL;DR

This paper introduces new tools, EVEE-LIBS and EVEE-PROTEGE, for generating and visualizing proofs in description logic ontologies up to ALCH, enhancing explainability beyond existing methods.

Contribution

It presents EVEE-LIBS and EVEE-PROTEGE, novel Java libraries and Protégé plugins for proof computation and visualization in more expressive description logics, advancing explainability tools.

Findings

EVEE-LIBS supports proof computation for DLs up to ALCH.

EVEE-PROTEGE enables proof visualization within Protégé.

EVONNE offers an interactive proof display application.

Abstract

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\'eg\'e 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\'eg\'e plugins for displaying those proofs in Prot\'eg\'e. 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.