Measuring User Comprehension of Inference Rules in Euler Diagrams

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.