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:Stronger Higher-order Automation
Speaker:Sophie Tourret
coming from:Max-Planck-Institut für Informatik - RG 1
Speakers Bio:
Event Type:Joint Lecture Series
Visibility:D1, D2, D3, INET, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 4 December 2019
Duration:60 Minutes
Building:E1 5
Automated reasoning in first-order logic (FOL) is becoming a mature
research domain. It has led to the development of powerful tools such as
superposition-based theorem provers and SMT solvers (Satisfiability
Modulo Theory solvers), that have found and continue to find many
applications in industry and research.

One such application is the automation of proofs in interactive theorem
proving (ITP), where proof assistants are used to write computer-checked
proofs of theorems, generally expressed in a variant of higher-order
logic (HOL). This automation is realised via "hammers", that attempt to
delegate the proof obligations to first-order automated provers.
However, in the translation from HOL to FOL, hammers obfuscate the
structure of terms and formulas through the application of a sequence of
encodings, although it is this very structure that the provers exploit
to find proofs efficiently.

This situation is less than ideal, and if until a few years ago, the ITP
and ATP communities were working in parallel, mostly ignoring each
other, there is nowadays a trend pushing to bring the two communities
closer. The work that I will present in this talk is part of this trend.
It includes ongoing research that is either improving higher-order
automation with respect to ITP applications or using ITP as a vehicle
for ATP research.
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, 11/04/2019 03:47 PM
  • Jennifer Müller, 08/26/2019 11:51 AM -- Created document.