  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.
