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

TL;DR

This paper investigates the complexity of generating comprehensible proofs in Description Logic by analyzing recursive proof quality measures, including proof depth, and provides comprehensive complexity results across various calculi.

Contribution

It extends previous work by analyzing recursive proof measures, including proof depth, and offers a broad complexity analysis for proof generation in Description Logic.

Findings

Recursive measures lead to lower complexity bounds.

Proof depth is encompassed within the recursive measure framework.

The results provide a comprehensive understanding of proof complexity in Description Logic.

Abstract

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.