Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Making Theorem Provers Easier to Use
Speaker:Jasmin Christian Blanchette
coming from:Max-Planck-Institut für Informatik - RG 1
Speakers Bio:
Event Type:Joint Lecture Series
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 2 September 2015
Duration:60 Minutes
Building:E1 5
Theorem provers are computer programs that help prove logical formulas, whether they arise in mathematics,

in computer science, or elsewhere. The theorem proving community divided in two. Roughly speaking: (1) The
automatic subcommunity develops automatic theorem provers (ATPs; e.g., SPASS, Z3), with the very ambitious
goal of replacing mathematicians by machines. (2) The interactive subcommunity develops proof assistants
(e.g., Coq, Isabelle), with the goal of replacing LaTeX proofs by computer-checked documents.

In this talk, I present work on integrating ATPs in proof assistants and on enriching ATPs with features typical of
proof assistants. I argue in favor of a tighter integration of the two communities, to make theorem proving easier,
more productive, more enjoyable, and more useful.

Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):

Jennifer Müller/MPI-INF, 08/31/2015 11:57 AM
Last modified:
Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Jennifer Müller, 08/31/2015 12:44 PM -- Created document.