# Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report)

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 39 references that are in the map.
- First posted on arXiv 27 Apr 2021.

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

- [Explainable Artificial Intelligence (XAI): Concepts, Taxonomies, Opportunities and Challenges toward Responsible AI](https://mlsanity.com/paper/1910.10045/) (2019)
- [Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)](https://mlsanity.com/paper/2004.08311/) (2020)

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

- [Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended algorithms and examples)](https://mlsanity.com/paper/2303.11712/) (2023)
- [CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)](https://mlsanity.com/paper/2207.08453/) (2022)
- [Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version](https://mlsanity.com/paper/2205.09583/) (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)
- [Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving](https://mlsanity.com/paper/2209.12592/) (2022)
- [Efficiently Explaining CSPs with Unsatisfiable Subset Optimization](https://mlsanity.com/paper/2105.11763/) (2021)
- [Why Not? Explaining Missing Entailments with Evee (Technical Report)](https://mlsanity.com/paper/2308.07294/) (2023)

## Abstract (arXiv)

Logic-based approaches to AI have the advantage that their behavior can in principle be explained to a user. If, for instance, a Description Logic reasoner derives a consequence that triggers some action of the overall system, then one can explain such an entailment by presenting a proof of the consequence in an appropriate calculus. How comprehensible such a proof is depends not only on the employed calculus, but also on the properties of the particular proof, such as its overall size, its depth, the complexity of the employed sentences and proof steps, etc. For this reason, we want to determine the complexity of generating proofs that are below a certain threshold w.r.t. a given measure of proof quality. Rather than investigating this problem for a fixed proof calculus and a fixed measure, we aim for general results that hold for wide classes of calculi and measures. In previous work, we first restricted the attention to a setting where proof size is used to measure the quality of a proof. We then extended the approach to a more general setting, but important measures such as proof depth were not covered. In the present paper, we provide results for a class of measures called recursive, which yields lower complexities and also encompasses proof depth. In addition, we close some gaps left open in our previous work, thus providing a comprehensive picture of the complexity landscape.