skip to content

Hammers and Model Finders, and Beyond

Presented by: 
Jasmin Blanchette INRIA Nancy - Grand Est, Max-Planck-Institut für Informatik, Saarbrücken
Wednesday 12th July 2017 - 11:30 to 12:30
INI Seminar Room 1
Integrations of automatic theorem provers in proof assistants -- in the form of "hammers" -- are useful to formalize arbitrary mathematics. 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 finding for counterexample generation (Nunchaku); and formalization of number theory together with a mathematician.

Related Links
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons