Quantomatic: A Proof Assistant for Diagrammatic Reasoning
Aleks Kissinger, Vladimir Zamdzhiev

TL;DR
Quantomatic is a proof assistant that uses string diagrams for diagrammatic reasoning in monoidal algebraic structures, enabling semi-automatic construction of equational proofs with a focus on graphical syntax.
Contribution
It introduces a novel tool supporting semi-automatic proof construction using string diagrams, bridging graphical reasoning with algebraic structures.
Findings
Supports semi-automatic proof construction
Provides a rewriting engine based on monoidal algebra
Demonstrates normal form computation for bialgebras
Abstract
Monoidal algebraic structures consist of operations that can have multiple outputs as well as multiple inputs, which have applications in many areas including categorical algebra, programming language semantics, representation theory, algebraic quantum information, and quantum groups. String diagrams provide a convenient graphical syntax for reasoning formally about such structures, while avoiding many of the technical challenges of a term-based approach. Quantomatic is a tool that supports the (semi-)automatic construction of equational proofs using string diagrams. We briefly outline the theoretical basis of Quantomatic's rewriting engine, then give an overview of the core features and architecture and give a simple example project that computes normal forms for commutative bialgebras.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
