Publication
In the Eye of the Beholder: Which Proofs are Best?
Stefan Borgwardt; Anke Hirsch; Alisa Kovtunova; Frederik Wiehr
In: Stefan Borgwardt; Thomas Meyer (Hrsg.). 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, Vol. 2663, CEUR, 2020.
Abstract
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.