Graphical logic

Linear syntax, it is often been felt, obscures the combinatorics of proof. The graphical representation of logic thus has a long history. The latest attempt to capture these combinatorics is Dominic Hughes' Proof without Syntax. Here is the abstract:

"[M]athematicians care no more for logic than logicians for mathematics." Augustus de Morgan, 1868.
Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract mathematical formulation of propositional calculus (propositional logic) in which proofs are combinatorial (graph-theoretic), rather than syntactic. It defines a *combinatorial proof* of a proposition P as a graph homomorphism h : C -> G(P), where G(P) is a graph associated with P and C is a coloured graph. The main theorem is soundness and completeness: P is true iff there exists a combinatorial proof h : C -> G(P).