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

Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons