| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Auto2 Prover
| Title: | Auto2 Prover |
| Author: | Bohua Zhan |
| Submission date: | 2018-11-20 |
| 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. |
| BibTeX: |
@article{Auto2_HOL-AFP,
author = {Bohua Zhan},
title = {Auto2 Prover},
journal = {Archive of Formal Proofs},
month = nov,
year = 2018,
note = {\url{https://isa-afp.org/entries/Auto2_HOL.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Auto2_Imperative_HOL |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |