Background

The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms.

The progress in computer-aided reasoning, both automatic and interactive, during the past decades, has 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 of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and collaboration of the HOL Light and Isabelle systems in the formal proof of the Kepler conjecture.

Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools for exchanging problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation, and communication methods, standards, protocols, and programming interfaces. The workshop welcomes developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. We are interested both in success stories and descriptions of current bottlenecks and proposals for improvement

Topics

Topics of interest for this workshop include all aspects of cooperation between reasoning tools, whether automatic or interactive. More specifically, some suggested topics are:

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 (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.

Submissions

Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages, excluding bibliography) or a regular paper (up to 15 pages, excluding bibliography). Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. We expect that one author of every accepted paper will present their work at the workshop.

Submitted papers should describe previously unpublished work, and must be prepared using the LaTeX EPTCS class. Papers should be submitted via EasyChair Accepted regular papers will appear in an EPTCS volume (TO BE CONFIRMED)

Important Dates

Abstract submission:	April 21 April 28, 2021
Paper submission:	April 28 May 5, 2021
Author notification:	May 26, 2021
Camera ready version due:	June 16, 2021
Workshop:	July 11, 2021	Virtual, like CADE

Invited speakers

• Proof Generation in CDSAT, Maria Paola Bonacina (Università degli Studi di Verona)
• Reasoning in many logics with Vampire: Everything's CNF in the end, Giles Reger (The University of Manchester)

Registration

Registration to PxTP is handled through CADE registration. Any non-CASC-only registration also includes PxTP and all workshops.

Accepted papers

A framework for proof-carrying logical transformations, by Quentin Garchery

General automation in Coq through modular transformations, by Valentin Blot, Louise Dubois de Prisque, Chantal Keller and Pierre Vial

Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract), by Stephan Gocht, Ruben Martins and Jakob Nordstrom

Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract), by Nicolas Magaud

Alethe: Towards a Generic SMT Proof Format (Extended Abstract), by Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa and Pascal Fontaine

Proceedings

The PxTP 2021 proceedings are now available. You can also download a PDF copy.

Program Committee

• Chantal Keller (LRI, Université Paris-Saclay), co-chair
• Mathias Fleury (Johannes Kepler University Linz), co-chair

• 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)
• Aina Niemetz (Stanford University)
• Jens Otten (University of Oslo)
• Giselle Reis (Carnegie Mellon University)
• Geoff Sutcliffe (University of Miami)
• François Thiré (Nomadic Labs)
• Sophie Tourret (Inria)
• Josef Urban (Czech Technical University in Prague)

Program

Sunday, 11 July 2021. All times are EDT.

Session	Invited talk
Chair:	Mathias Fleury
8:00-9:00	Invited speaker: Maria Paola Bonacina Proof Generation in CDSAT
Session	Certifying Transformations
Chair:	Mathias Fleury
9:00-9:30	Quentin Garchery A framework for proof-carrying logical transformations
9:30-10:00	Valentin Blot, Louise Dubois de Prisque, Chantal Keller and Pierre Vial General automation in Coq through modular transformations
10:00-10:30	break
Session	Invited talk
Chair:	Chantal Keller
10:30-11:30	Invited speaker: Giles Reger Reasoning in many logics with Vampire: Everything's CNF in the end
Session	Use cases
Chair:	Chantal Keller
11:30-11:50	Nicolas Magaud Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant
11:50-12:30	break
Session	Generating and Using Proofs
Chair:	Katalin Fazekas
12:30-12:50	Stephan Gocht, Ruben Martins and Jakob Nordstrom Certifying CNF Encodings of Pseudo-Boolean Constraints
12:50-13:10	Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa and Pascal Fontaine Alethe: Towards a Generic SMT Proof Format
13:10-13:15	short break
Business Meeting
13:15-14:00	PxTP Business Meeting

Previous Editions

See main here.