Why Not? Explaining Missing Entailments with Evee (Technical Report)

TL;DR

This paper introduces an enhanced Protégé plugin, Evee, that explains both why certain logical entailments hold and why some expected entailments are missing, using abduction and counterexamples techniques.

Contribution

The paper presents a new version of Evee that provides explanations for missing consequences in ontologies, addressing a gap in existing explanation tools.

Findings

Evee now explains missing entailments using abduction.

The plugin incorporates counterexample-based explanations.

It improves user understanding of ontology reasoning outcomes.

Abstract

Understanding logical entailments derived by a description logic reasoner is not always straight-forward for ontology users. For this reason, various methods for explaining entailments using justifications and proofs have been developed and implemented as plug-ins for the ontology editor Prot\'eg\'e. However, when the user expects a missing consequence to hold, it is equally important to explain why it does not follow from the ontology. In this paper, we describe a new version of $\rm E{\scriptsize VEE}$, a Prot\'eg\'e plugin that now also provides explanations for missing consequences, via existing and new techniques based on abduction and counterexamples.