skip to content

Hammers and Model Finders, and Beyond

Presented by: 
Jasmin Blanchette
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
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons