[Club2] PAAR talk rehearsal: This Friday 14:00 Turing

[Jasmin Blanchette]

Hi all,

I will have the honour of standing in for Larry at the PAAR workshop at FLoC, and will rehearse the talk on Friday at 14:00 in Turing (00.09.055). The talk is a one-hour invited talk about The Sledgehammer.


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

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.


I hope to see you there!

Jasmin