Lemmas: Generation, Selection, Application
arXiv:2303.05854 · doi:10.1007/978-3-031-43513-3_9
Abstract
Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.
arXiv commentExtended version of the TABLEAUX 2023 contribution
References in corpus (5)
- PyTorch: An Imperative Style, High-Performance Deep Learning Library
- Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
- Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
- Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers
- CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)