TL;DR
AUTO2 is a new saturation-based heuristic prover for higher-order logic that leverages user-defined heuristics and best-first search to automate complex proofs in mathematics and computer science.
Contribution
It introduces a novel saturation-based heuristic approach for higher-order logic theorem proving, implemented in Isabelle/HOL, enhancing automation capabilities.
Findings
Effective in formalizing mathematical proofs
High automation in diverse proof tasks
Demonstrated success in real-world formalizations
Abstract
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of propositions derivable from the initial assumptions, where new propositions are added by user-defined functions called proof steps. We implemented the prover in Isabelle/HOL, and applied it to several formalization projects in mathematics and computer science, demonstrating the high level of automation it can provide in a variety of possible proof tasks.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
