Max-Planck-Institut für Informatik
max planck institut
informatik
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
Language:English
Date, Time and Location
Date:Wednesday, 2 September 2015
Time:12:15
Duration:60 Minutes
Location:Saarbrücken
Building:E1 5
Room:002
Abstract
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.

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

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