A Lambda-Superposition Tactic for Isabelle/HOL
summary
A new Isabelle/HOL tactic implements the λ-superposition calculus to avoid Metis’s first‑order encodings, runs proof search on Isabelle terms, and reconstructs proofs via the kernel after search. Evaluation on 8,000 goals uses Zipperposition which proves 47% of goals, and reconstruction yields Metis 88.7% vs slam 78.9% of those, with 30 proofs unique to slam and a 0.8 percentage‑point union gain. Implementation omits expensive rules, uses Isabelle pre‑unification, trades completeness for speed, and shows room for performance tuning.
AI-written summary · about
chapters (13)
- 0:00Lambda-Superposition tactic intro
- 0:24Isabelle/HOL & Sledgehammer
- 1:28Introducing SLAM tactic
- 3:57Limitations of Metis
- 5:49SLAM’s calculus & HOL
- 7:35SLAM’s pragmatic calculus
- 8:41SLAM’s core rules
- 11:52Higher-order & boolean reasoning
- 13:18Heuristics & term ordering
- 14:23SLAM’s proof search
- 17:18SLAM vs Metis evaluation
- 19:03Future work & improvements
- 19:25Q&A