BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Hammers and Model Finders\, and Beyond - Jasmin Blanchette (INRIA 
 Nancy - Grand Est\; Max-Planck-Institut für Informatik\, Saarbrücken)
DTSTART:20170712T103000Z
DTEND:20170712T113000Z
UID:TALK73255@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Integrations of automatic theorem provers in proof assistants 
 -- in the form of "hammers" -- are useful to formalize arbitrary mathemati
 cs. I will briefly talk about the experience we have with Sledgehammer and
  then focus on two ongoing project in which I am involved and a future one
  (modulo funding): automation of higher-order logic (Matryoshka)\; model f
 inding for counterexample generation (Nunchaku)\; and formalization of num
 ber theory together with a mathematician. <br><br>Related Links<ul><li><a 
 target="_blank" rel="nofollow" href="http://www-old.newton.ac.uk/cgi/http%
 3A%2F%2Fmatryoshka.gforge.inria.fr">http://matryoshka.gforge.inria.fr</a> 
 - Matryoshka project</li></ul>
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR