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.

• Type: Journal
• Year: 2011
• Where: FROCOS
• Authors: Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow
• Keywords: Automatic Proof, Control Systems, FROCOS 2011, Kodkod, Proof Search