Measuring User Comprehension of Inference Rules in Euler Diagrams
Sven Linker, Jim Burton, Andrew Blake · Lecture notes in computer science · 2016
Proofs created by diagrammatic theorem provers are not designed with human readers in mind. We say that one proof, $$P_1$$ , is more “readable” than another, $$P_2$$ , if users make fewer errors in understanding which inference rules were applied in $$P_1$$ than in $$P_2$$ , 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.