Automatic Proof and Disproof in Isabelle/HOL

Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow

Isabelle/HOL is a popular interactive theorem prover based on higher-order logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on resolution provers and SMT solvers for its proof search, the counterexample generator Quickcheck uses the ML compiler as a fast evaluator for ground formulas, and its rival Nitpick is based on the model finder Kodkod, which performs a reduction to SAT. Together with the Isar structured proof format and a new asynchronous user interface, these tools have radically transformed the Isabelle user experience. This paper provides an overview of the main automatic proof and disproof tools.



author={Jasmin Christian Blanchette and Lukas Bulwahn and Tobias Nipkow},
title={Automatic Proof and Disproof in Isabelle/HOL},
booktitle={Frontiers of Combining Systems (FroCoS 2011)},
editor={C. Tinelli and V. Sofronie-Stokkermans},