Automating Equational Proofs in Dirac Notation

TL;DR

This paper demonstrates that the first-order theory of Dirac notation is decidable and introduces an efficient, implemented algorithm for automated equivalence checking of quantum states in Dirac notation.

Contribution

It proves the decidability of Dirac notation's first-order theory and develops an efficient, practical algorithm for automated reasoning in quantum physics.

Findings

Decidability of Dirac notation's first-order theory established.

Algorithm efficiently checks equation validity in Dirac notation.

Implementation successfully tested on over 100 literature examples.

Abstract

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.