Many algebraic structures, such as Frobenius algebras, or quasi-triangular Hopf algebras, can be formulated in an arbitrary symmetric monoidal category. They are given by a collection of morphisms, and a collection of axioms, which are equations between two different string diagrams.
There are many theorems which hold for any symmetric monoidal category, such as that the antipode of a quasi-triangular Hopf algebra is involutive. Such theorems are themselves equations between two string diagrams. They can be proven by a sequence of axioms translating the one string diagram into the other. Applying an axiom $A=B$ to a string diagram $X$ means identifying $A$ with a part of $X$, and replacing this part by $B$.
Are there any implementations for algorithms which automatically find such a sequence proving an algebraic statement?
I'm aware that something very similar is known as "double-pushout graph rewriting", for which some implementations exist. However, there is a subtle difference between string diagrams and graphs: Whereas in a string diagram, each morphism has different input and output components (e.g., the multiplication of an algebra has a "left" and a "right" input, and we cannot exchange left and right if the algebra is not commutative), there is no distinction between the different edges adjacent to a vertex in a graph.
Is there any implementation of graph rewriting which allows distinguishing the edges adjacent to a vertex?
