Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

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.

Details

Original languageEnglish
Title of host publicationAutomated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings
EditorsAndré Platzer, Geoff Sutcliffe
Pages291–308
Number of pages18
Publication statusPublished - 2021
Peer-reviewedYes

External IDs

Scopus 85106082338
ORCID /0000-0001-9936-0943/work/142238103
ORCID /0000-0002-4049-221X/work/142247842

Keywords