Automating equational proofs in Dirac notation
summary
Proves that Dirac notation’s first-order theory is decidable by reducing formulas to the theory of real closed fields (Tarski) and shows practical equivalence checking via a specialized AC term‑rewriting system. Implementation in Mathematica normalizes terms with a rule set of 150+ rewrite rules, checks confluence and termination with automated proof tools, and resolves equivalence on 100+ literature examples efficiently.
AI-written summary · about
chapters (12)
- 0:00Automating Dirac proofs
- 1:48Dirac notation in quantum theory
- 3:33Equational reasoning challenges
- 5:39Universal algebra formalization
- 7:27Equational logic for linear algebra
- 9:18Term rewriting solution
- 11:58Verifying rewriting properties
- 13:03Extending with big operators
- 14:53Benchmark evaluation
- 16:40Development challenges
- 17:43Future directions
- 18:03Q&A
related talks
41mWar Time Proofs and Futuristic Programs
55mProving Theorems and Certifying Programs with Coq
22mTowards Verified Linear Algebra Programs Through Equivalence
01h 00mLogic and Probabilistic Circuits 3
19mPositive Almost-Sure Termination – Complexity and Proof Rules
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
13mFormalizing a First-order Differentiable Logic with MathComp
25mLearning Formulas in Finite Variable Logics