Abstract
We introduce a new theorem prover for classical higherorder logic named auto2. The prover is designed to make use of humanspecified 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.
Cite
CITATION STYLE
Zhan, B. (2016). Auto2, a saturation-based heuristic prover for higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9807 LNCS, pp. 441–456). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
