# Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 27 references that are in the map.
- First posted on arXiv 19 May 2022.

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

- [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)

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

- [On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (Extended Version)](https://mlsanity.com/paper/2206.07711/) (2022)
- [Recovering Explanations from Transformed Rule-Based Ontologies](https://mlsanity.com/paper/2608.06399/) (2026)

## Abstract (arXiv)

Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The "justifications" usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which visualizes proofs of consequences for ontologies written in expressive DLs. We describe the methods used for computing those proofs, together with a feature called signature-based proof condensation. Moreover, we evaluate the quality of generated proofs using real ontologies.