无限族图方程的有穷验证

ZX、ZW 与 ZH 演算都是用于推理纯态量子比特量子力学的图形演算。这些语言都使用特定的图饰，称为 !-盒与相位变量，来不仅表示一个图而是无限族图。这些图饰足够强大，使得这些演算的完备规则集可用约十五条规则表达。历史上涉及 !-盒的规则无法由计算机验证。我们提出首个将涉及 !-盒的无限族方程归约为有穷验证子集的算法。该方法唯一的要求是 !-盒连通性上的一个温和性质。先前结果聚焦于 ZX 中相位变量的有穷情形分析，我们也将此结果推广到 ZW 与 ZH，并提供用于更多语言的通用框架。本文结果使证明助手能将无限族问题（涉及相位变量与 !-盒的组合）归约为无图饰的逐情形验证，这是以往不可能的。我们特别指出，在验证任务中无需直接对 !-盒进行推理，这是全新的。这构成了量子电路自动验证、猜想综合及一般图语言等更宏大工作的一部分。此处描述的方法可推广至任何满足某些简单条件的图语言。