Designing inference rules for spider diagrams

Diagrammatic modes of communication have long been recognized for their accessible representations of information. One area in which they have been developed is that of logical reasoning, where symbolic notations are perceived by many as difficult to use. Significant progress has been made on formalizing diagrammatic logics and proving formal properties of their inference rules. To-date, most inference rules for diagrammatic logics have been designed from the perspective of a logician, aiming for the essential and, thus, desirable properties of soundness and completeness. However, this approach overlooks a fundamental goal of providing diagrammatic logics: to overcome barriers posed by symbolic logics to non-mathematicians. Even if the diagrams themselves are accessible, having inference rules that result in unwieldy proofs will fail to fulfil this fundamental goal. Thus, the time is ripe to fully address this goal and show how to design inference rules that give rise to more natural proofs. In this paper we take significant steps towards this ambitious target by devising new inference rules for spider diagrams. We demonstrate that they allow substantially shorter proofs to be written and, we argue, the resulting proofs are more natural.