Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
summary
A unified proof framework uses matching logic as a base to build automated provers for multiple logics, implementing 11 generic rules (including LFP based on Park induction and WRAP/UNWRAP for contexts) and relying on SMT backends. A prototype prover handles separation logic, LTL, FO with least fixpoints and reachability; it passes 265/280 separation-logic benchmarks, proves the complete LTL axioms, and verifies a sum-from-1-to-n program, while noting limits in non‑fixpoint reasoning and simple DFS search.
AI-written summary · about
chapters (10)
- 0:00Start
- 2:32What Base Logic Should Be Used in this Architecture
- 2:49Matching Logic
- 3:35What Is Matching Logic
- 4:20Pattern Matching Semantics
- 4:33Examples of Matching Logic Patterns
- 5:53Hubert Style Proof System
- 8:37Context Reasoning Rule
- 10:40Contextual Implication
- 13:34Design Smarter Proof Strategies and Proof Characteristics
related talks
01h 03mMatching Logic: Foundation of the K Framework
30mNominal Matching Logic With Fixpoints
41mTotal Functions for Automated Reasoning:Building Terminating Theorem Provers
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
29mSynthesizing Axiomatizations using Logic Learning
01h 34mFormal Logic Undressed
19mAutomated Verification of Fundamental Algebraic Laws