![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Jasmin Blanchette (INRIA Nancy - Grand Est; Max-Planck-Institut für Informatik, Saarbrücken)
Wednesday 12 July 2017, 11:30-12:30
Hammers and Model Finders, and Beyond
⚠️ Important: BPRW01 - Computer-aided mathematical proof
- 👤 Speaker: Jasmin Blanchette (INRIA Nancy - Grand Est; Max-Planck-Institut für Informatik, Saarbrücken)
- 📅 Date & Time: Wednesday 12 July 2017, 11:30 - 12:30
- 📍 Venue: Seminar Room 1, Newton Institute
Questions? Contact
INI IT
Abstract
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
- http://matryoshka.gforge.inria.fr – Matryoshka project
Series This talk is part of the Isaac Newton Institute Seminar Series series.
Included in Lists
- All CMS events
- bld31
- dh539
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
Note: Ex-directory lists are not shown.