AUTO2, a saturation-based heuristic prover for higher-order logic
Logic in Computer Science
2016-08-30 v1
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.
Cite
@article{arxiv.1605.07577,
title = {AUTO2, a saturation-based heuristic prover for higher-order logic},
author = {Bohua Zhan},
journal= {arXiv preprint arXiv:1605.07577},
year = {2016}
}
Comments
16 pages, accepted for ITP 2016