Total Functions for Automated Reasoning:Building Terminating Theorem Provers
summary
Builds terminating automated-reasoning cores in Agda and proves they halt by design, using Agda combinators and a boxed well‑founded fixed point to enforce progress. Implements a first‑order MGU unifier and an iterative DPLL SAT solver with a first‑class trail, proving termination via lexicographic measures and preserved invariants. Notes almost a thousand termination‑related security bugs in a 2022 study to motivate totality. Code and proofs are in the repo and the implementations succeed though they trade raw performance for verified termination.
AI-written summary · about
chapters (7)
- 0:00Automated reasoning intro
- 3:09Contexts and finite sets
- 6:19Termination guarantees
- 13:20Unification termination proof
- 20:25Boolean satisfaction DPLL
- 30:12Iterative DPLL trails
- 39:45Lessons from verification
related talks
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
19mAutomated Verification of Fundamental Algebraic Laws
18mDeferring the Details and Deriving Programs
20mTotal Outcome Logic: Termination and Nontermination Proving for Effectful Branching
23mProductivity Verification for Functional Programs by Reduction to Termination Ve...
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
46mMechanizing Abstract Interpretation
15mClosing Remarks