Published: 23rd August 2019
DOI: 10.4204/EPTCS.301
ISSN: 2075-2180

EPTCS 301

Proceedings Sixth Workshop on
Proof eXchange for Theorem Proving
Natal, Brazil, August 26, 2019

Edited by: Giselle Reis and Haniel Barbosa

Preface
Giselle Reis and Haniel Barbosa
Invited Talk: Systems for Doing Mathematics by Computer
Assia Mahboubi
1
Invited Talk: Learning from Tactic Steps in Formal Proofs
Thibault Gauthier
2
Converting ALC Connection Proofs into ALC Sequents
Eunice Palmeira, Fred Freitas and Jens Otten
3
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett and Cesare Tinelli
18
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
Mohamed Yacine El Haddad, Guillaume Burel and Frédéric Blanqui
27
Reconstructing veriT Proofs in Isabelle/HOL
Mathias Fleury and Hans-Jörg Schurr
36
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
Fadil Kallat, Tristan Schäfer and Anna Vasileva
51

Preface

This volume of EPTCS contains the proceedings of the Sixth Workshop on Proof Exchange for Theorem Proving (PxTP 2019), held on 26 August 2019 as part of the CADE-27 conference in Natal, 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 Wroclaw (2011), Manchester (2012), Lake Placid (2013), Berlin (2015) and Brasília (2017).

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

The program committee had the following members: Haniel Barbosa (co-chair), Giselle Reis (co-chair), Rob Blanco, Frédéric Blanqui, Simon Cruanes, Catherine Dubois, Amy Felty, Mathias Fleury, Stéphane Graham-Lengrand, Cezary Kaliszyk, Chantal Keller, Laura Kovács, Olivier Laurent, Stefan Mitsch, Carlos Olarte, Bruno Woltzenlogel Paleo, Florian Rabe, Martin Riener, Geoff Sutcliffe, Josef Urban and Yoni Zohar.

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. Furthermore, we are thankful to the CADE-27 organizer, Elaine Pimentel, for enabling a smooth local organization of the event.

In Natal we will have the honor to welcome two invited speakers: Assia Mahboubi, from Inria and Vrije Universiteit Amsterdam, giving a talk entitled Systems for Doing Mathematics by Computer and Thibault Gauthier, from Czech Technical University, presenting a talk entitled Learning from Tactic Steps in Formal Proofs.

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.

August 4, 2019

Giselle Reis and Haniel Barbosa


Systems for Doing Mathematics by Computer

Assia Mahboubi (Inria, France and Vrije Universiteit Amsterdam, The Netherlands)

In the late 80s, Wolfram describes the Mathematica computer algebra system as a system for doing mathematics by computer [1]. Since, a broad spectrum of tools have been designed for computer-aided mathematics: computer algebra systems offer sophisticated algorithms for symbolic computations; scientific computing builds on the implementation of powerful numerical analysis algorithms; high-performance automated provers have produced proofs for long-standing mathematical conjectures [3]; proof assistants are mature enough for the formalization of contemporary mathematics [2,5], etc. The ever eased access to the computational power of machines has changed the face of experimentation in mathematics.

But the status of proofs in the mathematical literature has been transformed as well, as these can themselves be computer-aided [4,2]. Proof assistants provide both the most expressive language to represent mathematical objects, and the highest possible guarantee on the correctness of formalized proofs. They could thus in principle be used to organize a fruitful cooperation among all these systems. But delicate software engineering problems, as well as more fundamental translation issues often hinder this collaboration [6]. In this talk we will try to discuss and illustrate the different views these different software may have on various mathematical objects, in particular from the perspective of proof exchange and verification.

[1] Stephen Wolfram. Mathematica: A System for Doing Mathematics by Computer. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1988.
[2] Fabian Immler. A verified ODE solver and the lorenz attractor. J. Autom. Reasoning, 61(1-4):73--111, 2018. [ DOI ]
[3] Marijn J. H. Heule. Schur number five. In AAAI, pages 6598--6606. AAAI Press, 2018.
[4] Thomas C. Hales. A proof of the Kepler conjecture. Annals of Mathematics, 162(3):1065--1185, 2005. [ DOI ]
[5] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 163--179. Springer, 2013. [ DOI ]
[6] Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi. A computer-algebra-based formal proof of the irrationality of ζ(3). In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 160--176. Springer, 2014. [ DOI ]

Learning from Tactic Steps in Formal Proofs

Thibault Gauthier (Czech Technical University in Prague, Czech Republic)

TacticToe is a machine-learning guided tactical prover which works as follows. By mining a proof assistant library and modifying its proof scripts, tactic invocations are recorded. Abstraction and orthogonalization techniques improve the quality of the created database. A predictor trained on these examples guides TacticToe proof attempts by biasing its searches towards the most promising tactics for each situation. The efficiency of TacticToe is demonstrated on the HOL4 standard library and part of CakeML. By construction, proof scripts generated by TacticToe can be easily inspected and analyzed.