A string diagram is a two-dimensional graphical representation that can be described as a one-dimensional term generated from a set of primitives using sequential and parallel compositions. Since different syntactic terms may represent the same diagram, this syntax is quotiented by a collection of coherence equations expressing equivalence up to deformation. This work lays foundations for automated reasoning about diagrammatic equivalence, motivated primarily by the verification of quantum circuit equivalences. We consider two classes of diagrams, for which we introduce normalizing term rewriting systems that equate diagrammatically equivalent terms. In both cases, we prove termination and confluence with the help of the proof assistant Isabelle/HOL.

翻译：字符串图是一种二维图形表示，可被描述为由一组基元通过串行与并行组合生成的一维项。由于不同的语法项可能表示同一图形，该语法通过一系列表达形变等价性的协调方程进行商化。本研究为图等价性的自动推理奠定基础，主要受量子电路等价性验证的驱动。我们考虑两类图形，并为之引入规范化项重写系统，以将图等价的项等同起来。在两种情形下，我们均借助证明辅助工具Isabelle/HOL证明了系统的终止性与合流性。