z-logo
open-access-imgOpen Access
Three 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.
Having issues? You can contact us here