English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Logic-based approaches to AI have the advantage that their behaviour can inprinciple be explained by providing their users with proofs for the derivedconsequences. However, if such proofs get very large, then it may be hard tounderstand a consequence even if the individual derivation steps are easy tocomprehend. This motivates our interest in finding small proofs for DescriptionLogic (DL) entailments. Instead of concentrating on a specific DL and proofcalculus for this DL, we introduce a general framework in which proofs arerepresented as labeled, directed hypergraphs, where each hyperedge correspondsto a single sound derivation step. On the theoretical side, we investigate thecomplexity of deciding whether a certain consequence has a proof of size atmost $n$ along the following orthogonal dimensions: (i) the underlying proofsystem is polynomial or exponential; (ii) proofs may or may not reuse alreadyderived consequences; and (iii) the number $n$ is represented in unary orbinary. We have determined the exact worst-case complexity of this decisionproblem for all but one of the possible combinations of these options. On thepractical side, we have developed and implemented an approach for generatingproofs for expressive DLs based on a non-standard reasoning task calledforgetting. We have evaluated this approach on a set of realistic ontologiesand compared the obtained proofs with proofs generated by the DL reasoner ELK,finding that forgetting-based proofs are often better w.r.t. different measuresof proof complexity.

Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)