Auto2 Prover

Bohua Zhan

20 November 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.
BSD License

Used by

Topics

Theories