Abstract. We have developed a diagrammatic logic for theorem proving, focusing on the domain of metric-space analysis (a geometric domain, but traditionally taught using a dry algebraic formalism). To evaluate its pragmatic value, pilot experiments were conducted using this logic implemented in an interactive theorem prover - to teach undergraduate students (and comparing performance against an equivalent algebraic logic). Our results show significantly better performance for students using diagrammatic reasoning. We conclude that diagrams are a useful tool for reasoning in such domains.
Daniel Winterstein, Alan Bundy, Corin A. Gurr, Mat