Synthesizing Axiomatizations using Logic Learning
summary
A synthesis pipeline called the LAS framework combines a soundness checker, counterexample generator, independence checker and constraint-based logic learner using SMT and first-order solvers and a new modal completeness checker. It synthesizes complete axiomatizations for 17 common modal frame classes and the tool automatically verifies completeness for 14 of 17. It rediscovers human axioms, sometimes finds simpler equivalents (e.g. Diamond true for serial frames), and for Kleene-algebra languages it finds 15 equational axioms including five new, stronger ones.
AI-written summary · about
chapters (11)
- 0:00An Audacious Question
- 2:09Elements of an Axiomatization
- 3:47Model-Theoretic Axiomatizations
- 8:54Our Solution: Learning-based Axiom Synthesis
- 10:49LAS Algorithm
- 12:42Case Study: Modal Logic
- 13:48Axiomatizing Modal Frames
- 15:50Discovering Modal Axiomatizations using LAS
- 18:04Experiments on Modal Logics
- 19:50Case Study: Languages with Kleene Star
- 22:40Future Applications
related talks
14mLOUD: Synthesizing Strongest and Weakest Specifications
31mLetting users do the undecidable: lessons from program synthesis
17mCalculational design of Incorrectness Separation Logic
53mSemantics-based program manipulation in the age of LLMs
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
22mCounterexample-Guided Inference of Modular Specifications
22mSAIL: Sound Abstract Interpreters with LLMs