Auto2 Prover

Bohua Zhan 🌐

November 20, 2018

Abstract

Auto2 is a saturation-based heuristic prover for higher-order logic, implemented as a tactic in Isabelle. This entry contains the instantiation of auto2 for Isabelle/HOL, along with two basic examples: solutions to some of the Pelletier’s problems, and elementary number theory of primes.

License

BSD License

Topics

Session Auto2_HOL