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.

翻译：狄拉克符号广泛应用于量子物理学和量子编程语言中，用于定义、计算和推理量子态。本文从自动推理的角度探讨狄拉克符号。我们证明了两个主要结果：首先，通过归约到实闭域理论和塔斯基定理，我们证明了狄拉克符号的一阶理论是可判定的。其次，我们利用项重写技术证明了等式有效性的判定可以在高效时间内完成。我们在 Mathematica 中实现了等价性检验算法，并通过文献中的 100 多个实例展示了其高效性。