[Club2] Wed. Feb 16 and Mar 16, 14:00: Jasmin Blanchette

[Alexander Krauss]

Dear all,

this Wednesday, Jasmin will give a preview of his talk at the Deduction 
Seminar. Another Sledgehammer talk rehearsal (this time for SVARM 2011) 
is scheduled for March 16.



Sledgehammer Hell: The Day after Judgement
====================================================
Wed. Feb 16, 14:00, MI 00.09.055 ("Alan Turing")

Sledgehammer is a component of Isabelle/HOL that employs resolution 
provers and SMT solvers to discharge goals arising in interactive 
proofs. The problems generated by Sledgehammer are unfriendly in many 
ways: They include hundreds of axioms (corresponding to HOL definitions 
and theorems), large terms, and lots of type information. In this talk, 
I will present empirical data to expose the main scalability issues in 
Sledgehammer, suggesting directions for future research.



Sledgehammer: A Link between Interactive and Automatic Theorem Provers
======================================================================
Wed. Feb 16, 14:00, MI 00.09.055 ("Alan Turing")

Sledgehammer is a component of Isabelle/HOL that employs resolution 
provers to discharge goals arising in interactive proofs. It 
heuristically selects relevant facts and, if a prover is successful, 
produces a snippet that reconstructs the proof in Isabelle. We recently 
extended Sledgehammer to invoke SMT (satisfiability modulo theories) 
solvers as well, with surprising results.