  This article presents a novel algorithmic methodology for performing
automated diagrammatic deductions over combinatorial structures, using a
combination of modified equational theorem-proving techniques and the extended
Wolfram model hypergraph rewriting formalism developed by the authors in
previous work. We focus especially upon the application of this new algorithm
to the problem of automated circuit simplification in quantum information
theory, using Wolfram model multiway operator systems combined with the
ZX-calculus formalism for enacting fast diagrammatic reasoning over linear
transformations between qubits. We show how to construct a generalization of
the deductive inference rules for Knuth-Bendix completion in which equation
matches are selected on the basis of causal edge density in the associated
multiway system, before proceeding to demonstrate how to embed the higher-order
logic of the ZX-calculus rules within this first-order equational framework.
After showing explicitly how the (hyper)graph rewritings of both Wolfram model
systems and the ZX-calculus can be effectively realized within this formalism,
we proceed to exhibit comparisons of time complexity vs. proof complexity for
this new algorithmic approach when simplifying randomly-generated Clifford
circuits down to pseudo-normal form, as well as when reducing the number of
T-gates in randomly-generated non-Clifford circuits, with circuit sizes ranging
up to 3000 gates, illustrating that the method performs favorably in comparison
with existing circuit simplification frameworks, and also exhibiting the
approximately quadratic speedup obtained by employing the causal edge density
optimization. Finally, we present a worked example of an automated proof of
correctness for a simple quantum teleportation protocol, in order to
demonstrate more clearly the internal operations of the theorem-proving
procedure.
