Ribbon Proofs
Jules Bean · Electronic Notes in Theoretical Computer Science · 2003
We present ‘Ribbon Proofs’, a graphical proof system for the Logic of Bunched Implications (BI). We give the informal, graphical, notation, we formalise the system algebraically and sketch the proof of its soundness and completeness. We discuss the spatial and geometrical nature of the proof system and its relation to BI's spatial model theory.