Affiliated with the 28th International Conference on Automated Deduction (CADE-28)
July 11^{th} 2021, PittsburghVirtual
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 of interest for this workshop include all aspects of cooperation between reasoning tools, whether automatic or interactive. More specifically, some suggested topics are:
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)
Abstract submission: | ||
Paper submission: | ||
Author notification: | May 26, 2021 | |
Camera ready version due: | June 16, 2021 | |
Workshop: | July 11, 2021 | Virtual, like CADE |
Registration to PxTP is handled through CADE registration. Any non-CASC-only registration also includes PxTP and all workshops.
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 |