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

TL;DR

Evonne is an interactive visualization system that helps users explore and understand proofs of entailments in expressive description logics, aiding ontology maintenance and comprehension.

Contribution

The paper introduces Evonne, a novel interactive tool for visualizing and analyzing DL proofs, including a new signature-based proof condensation method.

Findings

Proof visualization improves understanding of DL entailments.

Signature-based proof condensation reduces proof complexity.

Evaluation shows high quality of generated proofs on real ontologies.

Abstract

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.