AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

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.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only