[Club2] Reminder: Talk at 14:00 @ Turing

[Jasmin Christian Blanchette]

Hi all,

As previously announced, I will rehearse the following talk this this afternoon. The talk has nothing new to those of you who have already seen one of my previous Sledgehammer talks (PAAR, IWIL, NICTA), so feel free to skip it.


Sledgehammer: A Link between Interactive and Automatic Theorem Provers
======================================================================
Wed. March 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.


Jasmin