In order to effectively communicate information, the choice of representation is important. Ideally, a chosen representation will aid readers in making desired inferences. In this paper, we develop the theory of observation: what it means for one statement to be observable from another. Using observability, we give a formal characterization of the observational advantages of one representation of information over another. By considering observational advantages, people will be able to make better informed choices of representations of information. To demonstrate the (...) benefit of observation and observational advantages, we apply these concepts to set theory and Euler diagrams. In particular, we can show that Euler diagrams have significant observational advantages over set theory. This formally justifies Larkin and Simon’s claim that “a diagram is worth ten thousand words”. (shrink)

The development of diagrammatic logics is strongly motivated by the desire to make formal reasoning accessible to broad audiences. One major research problem, for which surprisingly little progress has been made, is to understand how to choose between semantically equivalent diagrams from the perspective of human cognition. The particular focus of this paper is on choosing between diagrams that represent either the presence or absence of individuals. To understand how to best make this choice, we conducted an empirical study. We (...) found that representing the presence of individuals supported task performance either significantly better than, or no worse than, representing the absence of individuals. The particularly striking feature of our results was that representing the absence of individuals in a way that makes the diagram highly cluttered is detrimental to human cognition. As a result, diagrams with this feature should be avoided, but diagrams using presence or low-cluttered absence can be used to support cognition in the context of the tasks performed in our study. (shrink)

Free rides and observational advantages occur in visualizations when they reveal facts that must be inferred from an alternative representation. Understanding whether these concepts correspond to cognitive advantages is important: do they facilitate information extraction, saving the ‘deductive cost’ of making inferences? This paper presents the first evaluations of free rides and observational advantages in visualizations of sets compared to text. We found that, for Euler and linear diagrams, free rides and observational advantages yielded significant improvements in task performance. For (...) Venn diagrams, whilst their observational advantages yielded significant performance benefits over text, this was not universally true for free rides. The consequences are two-fold: more research is needed to establish when free rides are beneficial, and the results suggest that observational advantages better explain the cognitive advantages of diagrams over text. A take-away message is that visualizations with observational advantages are likely to be cognitively advantageous over competing representations. (shrink)

In this paper, we introduce Speedith which is an interactive diagrammatic theorem prover for the well-known language of spider diagrams. Speedith provides a way to input spider diagrams, transform them via the diagrammatic inference rules, and prove diagrammatic theorems. Speedith’s inference rules are sound and complete, extending previous research by including all the classical logic connectives. In addition to being a stand-alone proof system, Speedith is also designed as a program that plugs into existing general purpose theorem provers. This allows (...) for other systems to access diagrammatic reasoning via Speedith, as well as a formal verification of diagrammatic proof steps within standard sentential proof assistants. We describe the general structure of Speedith, the diagrammatic language, the automatic mechanism that draws the diagrams when inference rules are applied on them, and how formal diagrammatic proofs are constructed. (shrink)