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. We study such reasoning through finite equational theories, presenting restricted quantum gate fragments as symmetric monoidal categories (PROPs), where wire permutations are treated as structural and separated cleanly from fragment-specific gate axioms. For six widely used near-Clifford fragments: qubit Clifford, real Clifford, Clifford+T (up to two qubits), Clifford+CS (up to three qubits) and CNOT-dihedral, we transfer the completeness results of prior work into our PROP framework. Beyond completeness, we address minimality (axiom independence). Using uniform separating interpretations into simple semantic targets, we prove minimality for several fragments (including all arities for qubit Clifford, real Clifford, and CNOT-dihedral), and bounded minimality for the remaining cases. Overall, our presentations significantly reduce rule counts compared to prior work and provide a reusable categorical framework for constructing complete and often minimal rewrite systems for quantum circuit fragments.

翻译：等式推理在量子电路优化与验证中具有核心地位：通过将一组固定的重写规则视为等式，用可证明等价的子电路进行替换。本研究通过有限等式理论探讨此类推理，将受限量子门片段呈现为对称幺半范畴（PROP），其中导线置换被视为结构元素并与片段特定的门公理清晰分离。针对六个广泛使用的近克利福德片段：量子比特克利福德、实克利福德、克利福德+T（至二量子比特）、克利福德+CS（至三量子比特）以及CNOT-二面体群，我们将既有研究的完备性结果迁移至PROP框架。除完备性外，我们还探讨了极小性（公理独立性）问题。通过构建到简单语义目标的统一分离解释，我们证明了多个片段（包括量子比特克利福德、实克利福德及CNOT-二面体群的所有元数情形）的极小性，并对其余情形证明了有界极小性。总体而言，相较于既有研究，我们的表示法显著减少了规则数量，并为构建量子电路片段的完备且通常极小的重写系统提供了可复用的范畴论框架。