Published: 4th December 2017|
|Preface Catherine Dubois and Bruno Woltzenlogel Paleo||1|
|Invited Speaker: Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems Gilles Dowek||3|
|Invited Speaker: Increasing Automation in Coq via Trustworthy Cooperation with External Automated Reasoners Cesare Tinelli||13|
|Language and Proofs for Higher-Order SMT (Work in Progress) Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui and Pascal Fontaine||15|
|An Extensible Ad Hoc Interface between Lean and Mathematica Robert Y. Lewis||23|
|Counter Simulations via Higher Order Quantifier Elimination: a preliminary report Silvio Ghilardi and Elena Pagani||39|
|Determinism in the Certification of UNSAT Proofs Tomer Libal and Xaviera Steele||55|
|Alignment-based Translations Across Formal Systems Using Interface Theories Dennis Müller, Colin Rothgang, Yufei Liu and Florian Rabe||77|
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:
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
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.