REVIEW 1 cited by
Automating Equational Proofs in Dirac Notation
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Automating Equational Proofs in Dirac Notation
read the original 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.
Forward citations
Cited by 1 Pith paper
-
An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops
Integer hybrid path-sums plus a sound Hoare logic enable semi-automated functional verification and expected-cost analysis of hybrid quantum programs with unbounded while loops.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.