Sciweavers

FROCOS
2011
Springer

Automatic Proof and Disproof in Isabelle/HOL

12 years 10 months ago
Automatic Proof and Disproof in Isabelle/HOL
Abstract. Isabelle/HOL is a popular interactive theorem prover based on higherorder 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.
Jasmin Christian Blanchette, Lukas Bulwahn, Tobias
Added 22 Dec 2011
Updated 22 Dec 2011
Type Journal
Year 2011
Where FROCOS
Authors Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow
Comments (0)