一句话：证明 Dirac 记号的一阶理论可判定，并用项重写高效判定等式，实现等价性检查器。
本文从自动推理角度研究量子物理与量子编程语言中广泛使用的 Dirac 记号。作者首先将 Dirac 记号的一阶理论归约到实闭域理论，并借助 Tarski 定理证明其可判定性。随后，他们利用项重写技术证明等式有效性可以被高效判定。作者在 Mathematica 中实现了该等价性检查算法，并在文献中的 100 多个例子上展示了其效率。
Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the perspective of automated reasoning. We prove two main results: first, the first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski’s theorem. Then, we prove that validity of equations can be decided efficiently, using term-rewriting techniques. We implement our equivalence checking algorithm in Mathematica, and showcase its efficiency across more than 100 examples from the literature.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{XuBZ25,
title = {Automating Equational Proofs in Dirac Notation},
author = {Yingte Xu and Gilles Barthe and Li Zhou},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704878}
}