Programming language

Geometry

Mathematics

Scripting language

Visual arts

Proof assistant

Computer science

Architecture

Point (geometry)

Mathematical proof

Automated theorem proving

EPiC series in computing

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.

Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers