In the Eye of the Beholder: Which Proofs are Best?

Stefan Borgwardt, Anke Hirsch, Alisa Kovtunova, Frederik Wiehr

In: Stefan Borgwardt, Thomas Meyer (editor). Proceedings of the 33rd International Workshop on Description Logics (DL 2020). International Workshop on Description Logics (DL-2020) 33rd located at International Conference on Principles of Knowledge Representation and Reasoning September 12-14 Rhodes/Virtual Greece CEUR Workshop Proceedings 2663 CEUR 2020.


Although logical entailments are often considered “explainable”, experience with justifications in DLs has shown that explaining why a logical consequence holds still requires some effort. However, a full formal proof of a DL entailment may be considered too long-winded, and a textual representation of a proof may be preferred. It may also depend on the user’s experience and individual preferences which representation of a proof constitutes a good explanation for them. Building on previous work on explaining DL consequences to users, we ran an experiment to compare 4 different forms of proofs: formal proofs and textual proofs, which are either very detailed or condensed. A multiple linear regression with contrast coding revealed that the participants rated short proofs as being easier than long proofs, independent of their representation. On the other hand, we could not verify any influence of prior experience with logic on how easy or difficult the different kinds of proofs were considered.

Weitere Links

BorgwardtHKW20.pdf (pdf, 470 KB )

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz