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

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 25 references that are in the map.
- First posted on arXiv 14 Aug 2023.

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

- [Signature-Based Abduction for Expressive Description Logics -- Technical Report](https://mlsanity.com/paper/2007.00757/) (2020)
- [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)
- [Signature-Based Abduction with Fresh Individuals and Complex Concepts for Description Logics (Extended Version)](https://mlsanity.com/paper/2105.00274/) (2021)
- [Connection-minimal Abduction in EL via Translation to FOL -- Technical Report](https://mlsanity.com/paper/2205.08449/) (2022)
- [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)

## Abstract (arXiv)

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 Escriptsize VEE, a Prot'eg'e plugin that now also provides explanations for missing consequences, via existing and new techniques based on abduction and counterexamples.