[Club2] Wed. June 22, 14:00: Jasmin Blanchette and Sascha Böhme

Andrei Popescu uuomul at yahoo.com
Sat Jun 18 17:45:19 CEST 2011


Hello, 

The coming Wednesday, we have a talk from Jasmin Blanchette and Sascha Böhme.  

Extending Sledgehammer with SMT Solvers
(joint work with Larry Paulson)
================================================================
Wed. Jun 22, 14:00, MI 00.09.055 ("Alan Turing")

Sledgehammer is a component of Isabelle/HOL that employs first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs' reach. Remarkably, the best SMT solver performs better than the best ATP on most of our benchmarks.

CADE-23 http://www4.in.tum.de/~blanchet/cade2011-sledge-smt.pdf








More information about the Club2 mailing list