COPLAS Talk: Łukasz Czajka
Date/time: March 2nd, 2018, 2:01-3:00 p.m.
Location: Universitetsparken 5, Room 01-0-029 (APL meeting room)
We present CoqHammer: the first full hammer system for the Coq proof assistant. The system translates Coq logic to untyped first-order logic and uses external automated theorem provers (ATPs) to prove the translations of user given conjectures. Based on the output of the ATPs, the conjecture is then re-proved in the logic of Coq using our proof search algorithm. Together with machine-learning based selection of relevant premises this constitutes a full hammer system.
The performance of the overall procedure has been evaluated in a bootstrapping scenario emulating the development of the Coq standard library. Over 40% of the theorems in the Coq standard library can be proved in a push-button mode in about 40 seconds of real time on an 8-CPU system.
In the talk we will describe the architecture of the system, discuss common use-case scenarios as well as some limitations, and give a live presentation of the tool.
Joint work with Cezary Kaliszyk, Univeristy of Innsbruck.
Łukasz Czajka received his PhD in Computer Science in 2015 from the University of Warsaw, Poland. He was supervised by Paweł Urzyczyn in the Logic and Type Theory group. Afterwards, he completed a one-year postdoc in Innsbruck under supervision of Cezary Kaliszyk, where he started working on the CoqHammer tool. Currently, he is a Marie-Curie postdoctoral fellow at the University of Copenhagen, supervised by Jakob Grue Simonsen. During his career so far he has been interested in a variety of topics, including confluence in term rewriting, combinatory logic, infinitary rewriting and lambda-calculus, implicit complexity via rewriting, and automated reasoning for the Coq proof assistant.
All are welcome. No registration required.