This volume of EPTCS contains the proceedings of the Seventh Workshop on Proof Exchange for Theorem Proving (PxTP 2021), held on 11 July 2021 as part of the CADE-28 conference, originally planned in Pittsburg, USA, but finally hold in cyberspace.
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.);
- metalanguages, 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 (i.e. interoperability of proofs between different proof calculi);
- 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 Wroclaw (2011), Manchester (2012), Lake Placid (2013), Berlin (2015), Brasília (2017), and Natal (2019).
This edition of the workshop received submissions of three regular papers and three extended abstracts. All submissions were evaluated by at least three anonymous reviewers. Two full papers and three extended abstracts were accepted in the post-proceedings.
The program committee had the following members: Chantal Keller (co-chair, LRI, Université Paris-Saclay), Mathias Fleury (co-chair, JKU Linz), Haniel Barbosa (Universidade Federal de Minas Gerai, Denis Cousineau (Mitsubishi Electric R&D Centre Europe), Stefania Dumbrava (ENSIIE, Télécom SudParis), Katalin Fazekas (TU Wien), Predrag Janićič (Univerzitet u Beogradu), Jens Otten (University of Oslo), Aina Niemetz (Stanford University), Giselle Reis (Carnegie Mellon University), Geoff Sutcliffe (University of Miami), François Thiré (Nomadic Labs), Sophie Tourret (Inria), and Josef Urban (Czech Technical University in Prague).
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-28 organizers who organized the conference in these challenging times.
We had the honor to welcome two invited speakers: Maria Paola Bonacina from the Università degli Studi di Verona gave a talk entitled Proof Generation in CDSAT and Giles Reger from the University of Manchester, presented a talk entitled Reasoning in many logics with Vampire: Everything's CNF in the end. The presentations from the invited speakers and the presentations from the accepted papers raised numerous, interesting, and fruitful discussions. We thank all the participants of the workshop.
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 infrastructure that they made available to us.
July 11, 2021
Chantal Keller and Mathias Fleury