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

arXiv: https://arxiv.org/abs/2206.07711 · HTML: https://mlsanity.com/paper/2206.07711/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 32 references that are in the map.
- First posted on arXiv 15 Jun 2022.

## Builds on (most cited first, 4 of 4)

- [Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)](https://mlsanity.com/paper/2004.08311/) (2020)
- [Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report)](https://mlsanity.com/paper/2104.13138/) (2021)
- [Extending Consequence-Based Reasoning to SRIQ](https://mlsanity.com/paper/1602.04498/) (2016)
- [Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version](https://mlsanity.com/paper/2205.09583/) (2022)

## Built on by (most cited first, 2 of 2)

- [Can You Tell the Difference? Contrastive Explanations for ABox Entailments](https://mlsanity.com/paper/2511.11281/) (2025)
- [Why Not? Explaining Missing Entailments with Evee (Technical Report)](https://mlsanity.com/paper/2308.07294/) (2023)

## Abstract (arXiv)

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.