COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Hammers and Model Finders, and Beyond

## Hammers and Model Finders, and BeyondAdd to your list(s) Download to your calendar using vCal - Jasmin Blanchette (INRIA Nancy - Grand Est; Max-Planck-Institut für Informatik, Saarbrücken)
- Wednesday 12 July 2017, 11:30-12:30
- Seminar Room 1, Newton Institute.
If you have a question about this talk, please contact INI IT. BPRW01 - Computer-aided mathematical proof 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. - http://matryoshka.gforge.inria.fr – Matryoshka project
This talk is part of the Isaac Newton Institute Seminar Series series. ## This talk is included in these lists:- All CMS events
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
- bld31
Note that ex-directory lists are not shown. |
## Other listsMartin Centre Research Seminar Series - 47st Annual Series of Lunchtime Lectures MRI Physics and Analysis for Cognitive Neuroscientists Wellcome Lecture in the History of Medicine MARLEN KHUTSIEV IN CAMBRIDGE AND LONDON Annual Race Equality Lecture 80000 Hours Cambridge## Other talksPlayer 2 has entered the game - ways of working towards open science Pruning and grafting syntactic trees for cross-lingual transfer tasks Biomolecular Thermodynamics and Calorimetry (ITC) Panel comparisons: Challenor, Ginsbourger, Nobile, Teckentrup and Beck |