### 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

- Tools

### Session Auto2_HOL

- Auto2_Setup
- Auto2_HOL_Extra_Setup
- HOL_Base
- Auto2_HOL_Setup
- Logic_Thms
- Order_Thms
- Arith_Thms
- Set_Thms
- Lists_Thms
- Auto2_Main
- Auto2_Test
- Pelletier
- Primes_Ex

### Used by

- Verifying Imperative Programs using Auto2

## Cite

×

Auto2_HOL-AFP

    @article{Auto2_HOL-AFP,
      author  = {Bohua Zhan},
      title   = {Auto2 Prover},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Auto2_HOL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Nov 29, 2018 : Isabelle2018