Published: 23rd August 2019|
|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|
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:
Abstract: Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is translated into a Boolean satisfiability (SAT) problem and delegated to a SAT solver. Consequently, producing bit-vector proofs in an SMT solver requires incorporating SAT proofs into its proof infrastructure. In this paper, we describe three approaches for integrating DRAT proofs generated by an off-the-shelf SAT solver into the proof infrastructure of the SMT solver CVC4 and explore their strengths and weaknesses. We implemented all three approaches using CryptoMiniSat as the SAT back-end for its bit-blasting engine and evaluated performance in terms of proof-production and proof-checking.
Abstract: Catering for ontology summary and reuse, several approaches such as modularisation and forgetting of symbols have been developed in order to provide users smaller sets of relevant axioms. We consider different module extraction techniques and show how they relate to each other. We also consider the notion of uniform interpolation that is underlying forgetting. We show that significant improvements in the performance of forgetting can be obtained by applying the forgetting tool to ontology modules instead of the entire ontology. We investigate combining several module notions with uniform interpolation and we provide a preliminary evaluation forgetting signatures based on the European Renal Association subset from SNOMED CT.
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
In the late 80s, Wolfram describes the Mathematica computer algebra system as a system for doing mathematics by computer . 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 ; 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 . 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.
|||Stephen Wolfram. Mathematica: A System for Doing Mathematics by Computer. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1988.|
|||Fabian Immler. A verified ODE solver and the lorenz attractor. J. Autom. Reasoning, 61(1-4):73--111, 2018. [ DOI ]|
|||Marijn J. H. Heule. Schur number five. In AAAI, pages 6598--6606. AAAI Press, 2018.|
|||Thomas C. Hales. A proof of the Kepler conjecture. Annals of Mathematics, 162(3):1065--1185, 2005. [ DOI ]|
|||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 ]|
|||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 ]|
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.