Auto2 Prover

Bohua Zhan 🌐

November 20, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Auto2_HOL