Sat 13 Jan 2018 09:00 - 10:00 at Watercourt A - Keynote Chair(s): Yves Bertot

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 an eauto-type 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 a 8-CPU system. This offers a huge saving of human work in programming language formalizations.

Sat 13 Jan

09:00 - 10:00: - Keynote at Watercourt A
Chair(s): Yves Bertot
CoqPL-2018151583040000009:00 - 10:00
File Attached