Proofs created by diagrammatic theorem provers are not de- signed with human readers in mind. We say that one proof, P1 , is more “readable” than another, P2 , if users make fewer errors in understanding which inference rules were applied in P1 than in P2 , and do so in a shorter time. We analysed the readability of individual rules in an empirical study which required users to identify the rules used in inferences. We found that increased clutter (redundant syntax) in the premiss diagrams affects readability, and that rule applications which require the user to combine information from several diagrams are sometimes less readable than those which focus on a single diagram. We provide an explanation based on mental models.
|Title of host publication||Diagrams 2016|
|Place of Publication||Berlin, Germany|
|Number of pages||8|
|Publication status||Published - 1 Aug 2016|
|Event||Diagrams 2016 - Philadelphia, USA, 7-10 August 2016,|
Duration: 1 Aug 2016 → …
|Period||1/08/16 → …|