Certifying the decidability of the word problem in monoids at large
summary
Implements a Rocq-based toolbox that uses Rocq proof assistant certificates and proofs-by-reflection guided by an external oracle to certify decision procedures for one-relation monoids; applies polynomial filters plus Knuth‑Bendix traces and heuristics to a search reduced to one million presentations (binary alphabet, length ≤10) and settles all but 260 unsolved cases. Traces become thousands-line Rocq programs, checked in about seven hours after six days of untrusted computation; native_compute and tries give 10–20× speedups.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 3:18Word problem in monoids
- 7:12Computational approach
- 11:06Knuth-Bendix completion
- 14:17Proof certificates and efficiency
- 16:24Formalization results
- 17:32Future work
- 18:36Q&A
related talks
01h 03mTrustworthy Automated Reasoning
22mAutomated reasoning on consistency models with MONA
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
18mSureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…)
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
15mStatically Verified Refinements for Multiparty Protocols
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
25mProperty-agnostic base case extension for scalable verification of distributed systems