Automatic Proof and Disproof in Isabelle/HOL
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.
pdf
BibTeX:
@inproceedings{BlanchetteBN-FROCOS11,
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},
publisher=Springer,series=LNCS,volume={6989},pages={12-27},year=2011}