Open AccessThree Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
Author(s) -
Lawrence C. Paulson
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
SCImago Journal Rank - 0.21
H-Index - 7
ISSN - 2398-7340
DOI - 10.29007/tnfd
Subject(s) - hol , mathematical proof , computer science , scripting language , programming language , proof assistant , automated theorem proving , point (geometry) , mathematics , geometry
Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.