Deduction is decisive but nonetheless mysterious, as I argue in the introduction. I identify the mystery of deduction as surprise-effect and demonstration-difficulty. The first section delves into how the mystery of deduction is connected with the representation of information and lays the groundwork for our further discussions of various kinds of representation. The second and third sections, respectively, present a case study for the comparison between symbolic and diagrammatic representation systems in terms of how two aspects of the mystery of (...) deduction – surprise-effect and demonstration-difficulty – are handled. The fourth section illustrates several well-known examples to show how diagrammatic representation suggests more clues to the mystery of deduction than symbolic representation and suggests some conjectures and further work. (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)