Preface

This volume of EPTCS contains the proceedings of the Fifth Workshop on Proof Exchange for Theorem Proving (PxTP 2017), held on September 23-24, 2017 as part of the Tableaux, FroCoS and ITP conferences in Brasília, Brazil.

The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a special focus on proofs.

The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation between such tools in larger systems has demonstrated the potential to reduce the amount of manual intervention.

Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop series strives to encourage such cooperation by inviting contributions on all aspects of cooperation between reasoning tools, whether automatic or interactive, including the following topics:

• applications that integrate reasoning tools (ideally with certification of the result);
• interoperability of reasoning systems;
• translations between logics, proof systems, models;
• distribution of proof obligations among heterogeneous reasoning tools;
• algorithms and tools for checking and importing (replaying, reconstructing) proofs;
• proposed formats for expressing problems and solutions for different classes of logic solvers (SAT, SMT, QBF, first-order logic, higher-order logic, typed logic, rewriting, etc.);
• meta-languages, logical frameworks, communication methods, standards, protocols, and APIs related to problems, proofs, and models;
• comparison, refactoring, transformation, migration, compression and optimization of proofs;
• data structures and algorithms for improved proof production in solvers (e.g. efficient proof representations);
• (universal) libraries, corpora and benchmarks of proofs and theories;
• alignment of diverse logics, concepts and theories across systems and libraries;
• engineering aspects of proofs (e.g. granularity, flexiformality, persistence over time);
• proof certificates;
• proof checking;
• mining of (mathematical) information from proofs (e.g. quantifier instantiations, unsat cores, interpolants, ...);
• reverse engineering and understanding of formal proofs;
• universality of proofs;
• origins and kinds of proofs (e.g. (in)formal, automatically generated, interactive, ...);
• Hilbert's 24th Problem (i.e. what makes a proof better than another?);
• social aspects (e.g. community-wide initiatives related to proofs, cooperation between communities, the future of (formal) proofs);
• applications relying on importing proofs from automatic theorem provers, such as certified static analysis, proof-carrying code, or certified compilation;
• application-oriented proof theory;
• practical experiences, case studies, feasibility studies;

Previous editions of the workshop took place in Wrocław (2011), Manchester (2012), Lake Placid (2013) and Berlin (2015).

This edition of the workshop received submissions of seven regular papers, one invited regular paper and two presentation-only extended abstracts. All submissions were evaluated by at least three anonymous reviewers and some papers went through two rounds of reviewing. Six papers were accepted in the post-proceedings.

The program committee had the following members: Christoph Benzmüller, Jasmin Christian Blanchette, Hans de Nivelle, Catherine Dubois (chair), Pascal Fontaine, Stéphane Graham-Lengrand, Hugo Herbelin, Olivier Hermant, Cezary Kaliszyk, Guy Katz, Chantal Keller, Tomer Libal, Mariano Moscato, Vivek Nigam, Andrei Paskevitch, Florian Rabe, Andrew Reynolds, Stephan Schulz, Geoff Sutcliffe, Josef Urban, Tjark Weber, Bruno Woltzenlogel Paleo (chair), and Akihisa Yamada.

We would like to thank all authors for their submissions and all members of the program committee for the time and energy they spent to diligently ensure that accepted papers were of high quality. We also thank Easychair for making it easy to chair the reviewing process.

In Brasília we had the honor to welcome two invited speakers: Gilles Dowek, from INRIA, gave a talk entitled Analyzing Logics, Analyzing Theories, and Analyzing Proofs and Cesare Tinelle, from Iowa University, presented a talk entitled Increasing Automation in Coq via Trustworthy Cooperation with External Automated Reasoners Eight contributed talks were presented. All these presentations raised numerous, interesting and fruitful discussions. We thank all the participants of the workshop. Furthermore, we are thankful to the Tableaux/FroCoS/ITP organizer, Claudia Nalon, for enabling a smooth local organization of the event.

The organization of this edition of PxTP stood on the shoulders of previous editions, and we are grateful to the chairs of previous editions for all the resources and infra-structure that they made available to us.

November 14, 2017

Catherine Dubois and Bruno Woltzenlogel Paleo

Increasing Automation in Coq via Trustworthy Cooperation with External Automated Reasoners

This talk describes recent work on SMTCoq, a plug-in for the integration of external automated reasoners into the Coq proof assistant originally developed at LIX and Inria, France. SMTCoq's main component is a checker for general first-order proof certificates that is fully implemented and proved correct in Coq. SMTCoq provides also vernacular commands and tactics to dispatch proof obligations to external proof-producing SAT and SMT solvers and check their answers. The tactics increase the level of automation in Coq by relying on such solvers while at the same time maintaining a high-level of trustworthiness thanks to SMTCoq's checker. We have recently extended SMTCoq to support, overall, proof certificates produced by the SAT solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier-free fragment of the combined theory of fixed-size bit vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols. New SMTCoq tactics capitalize on and combine the different scopes and strengths of the two SMT solvers by using them in cooperation. To account for solvers, like CVC4, that are not fully proof-producing the tactics allow them to return partial proofs, that is proofs including lemmas with no associated proof certificate. Such lemmas translate to subgoals for the other solvers or, failing that, for the user, providing a more flexible cooperation between Coq and the external solvers.

This is joint work with Burak Ekici, Alain Mebsout, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett, based on earlier work on by Chantal Keller with Michaël Armand, Germain Faure, Benjamin Grégoire, Laurent Théry, and Benjamin Werner.