Equational reasoning is central to quantum circuit optimisation and verification: one replaces subcircuits by provably equivalent ones using a fixed set of rewrite rules viewed as equations. A finite rule set is most informative when it separates the genuine algebra of a circuit fragment from the structural treatment of wires. This paper gives six near-Clifford fragments a common PROP treatment, where wire permutations are structural: qubit Clifford, real Clifford, Clifford+T (up to two qubits), Clifford+CS (up to three qubits), CNOT-dihedral, and qutrit Clifford. Starting from prior completeness theorems, we transfer completeness into this setting and remove redundant non-structural rules, then check minimality by separating interpretations tailored to individual axioms; the resulting presentations are minimal in all arities for qubit Clifford, real Clifford, and CNOT-dihedral, minimal in bounded ranges for the remaining fragments, and comparable by one transfer-and-separation pattern.

翻译：等式推理是量子电路优化与验证的核心：通过一组固定的重写规则（视为等式），将子电路替换为可证明等价的形式。当有限规则集能将电路片段的代数本质与导线的结构处理相分离时，该规则集最具信息价值。本文为六个近克利福德片段赋予统一的PROP处理方法（其中导线置换为结构性的）：量子比特克利福德、实克利福德、克利福德+T（至多两量子比特）、克利福德+CS（至多三量子比特）、CNOT-二面体群以及qutrit克利福德。基于已有的完备性定理，我们将其转换到该框架中并删除冗余的非结构性规则，随后通过针对各公理定制的分离解释检验规则的最小性；所得表示对量子比特克利福德、实克利福德和CNOT-二面体群在所有元数上均为最小，对剩余片段在有界范围内达到最小，并可通过统一的转移-分离模式进行可比性分析。