Affiliated with the 27th International Conference on Automated Deduction (CADE-27)

26 August 2019, Natal, Brazil

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) or a regular paper (up to 15 pages). 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, at the PxTP'2019 workshop page. Accepted regular papers will appear in an EPTCS volume.

Abstract submission: | May 12, 2019 |

Paper submission: | May 19, 2019 |

Author notification: | June 21, 2019 |

Camera ready version due: | July 21, 2019 |

Workshop: | 26 August, 2019 |

- Thibault Gauthier (Czech Technical University)
- Assia Mahboubi (Inria)

**Monday, 26 August 2019**

Chair: | Giselle Reis |

9:00-10:00 | Invited speaker:
Assia MahboubiSystems for Doing Mathematics by Computer |

10:00-10:30 | break |

Chair: | Haniel Barbosa |

10:30-11:15 |
Mathias Fleury and Hans-Jörg SchurrReconstructing veriT Proofs in Isabelle/HOL |

11:15-11:45 |
Mohamed Yacine El Haddad, Guillaume Burel and Frédéric BlanquiEKSTRAKTO A tool to reconstruct proofs from TSTP traces in Dedukti |

11:45-12:15 |
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar and Clark BarrettDRAT-based Bit-Vector Proofs in CVC4 |

12:15-14:00 | lunch break |

Chair: | Stephan Schulz |

14:00-15:00 | Invited speaker:
Thibault GauthierLearning from Tactic Steps in Formal Proofs |

15:00-15:30 |
Jieying Chen, Ghadah Abdulrahman S Alghamdi, Renate A. Schmidt, Dirk Walther and Yongsheng GaoModularity Meets Forgetting: A Case Study with the SNOMED CT Ontology |

15:30-16:00 |
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett and Cesare TinelliVerifying Bit-vector Invertibility Conditions in Coq |

16:00-16:30 | break |

Chair: | Cesare Tinelli |

16:30-17:15 |
Fadil Kallat, Tristan Schäfer and Anna VasilevaCLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories |

17:15-18:00 |
Eunice Palmeira Silva, Fred Freitas and Jens OttenConverting ALC Connection Proofs into ALC Sequents |

18:00-18:45 | PxTP Business Meeting |

- Haniel Barbosa (University of Iowa),
**co-chair** - Giselle Reis (Carnegie Mellon University),
**co-chair**

- Roberto Blanco (Inria)
- Frédéric Blanqui (Inria)
- Simon Cruanes (Aesthetic Integration)
- Catherine Dubois (ENSIIE)
- Amy Felty (University of Ottawa)
- Mathias Fleury (Max-Planck-Institut für Informatik)
- Stéphane Graham-Lengrand (SRI)
- Cezary Kaliszyk (University of Innsbruck)
- Chantal Keller (LRI, Université Paris-Sud)
- Laura Kovács (TU Wien)
- Olivier Laurent (CNRS, ENS Lyon)
- Stefan Mitsch (Carnegie Mellon University)
- Carlos Olarte (UFRN)
- Bruno Woltzenlogel Paleo (IOHK)
- Florian Rabe (LRI, Université Paris-Sud)
- Martin Riener (University of Manchester)
- Geoff Sutcliffe (University of Miami)
- Josef Urban (Czech Technical University in Prague)
- Yoni Zohar (Stanford University)

- PxTP 2017 (affiliated to Tableaux 2017, FroCoS 2017 and ITP 2017)
- PxTP 2015 (affiliated to CADE-25)
- PxTP 2013 (affiliated to CADE-24)
- PxTP 2012 (affiliated to IJCAR 2012)
- PxTP 2011 (affiliated to CADE-23)