Affiliated to the Tableaux, FroCoS and ITP conferences

23-24 September 2017, Brasilia, 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 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 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 also collaboration between HOL Light and Isabelle in the formal proof of the Kepler conjecture.

Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange 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 the interested 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 also interested both in success stories and in descriptions of the 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'2017 workshop page. Accepted regular papers will appear in an EPTCS volume.

- Abstract submission: Monday, June 26, 2017
- Paper submission: Monday, June 26, 2017
- Notification: Friday, July 7, 2017
- Camera ready versions due: Friday, July 21, 2017
- Workshop: 23-24 September 2017

- Gilles Dowek (INRIA)
- Cesare Tinelli (The University of Iowa)

Registration to PxTP is part of the Tableaux/FroCoS/ITP registration process.

**Saturday, 23 September 2017**

9:00-10:30 | Invited speaker:
Gilles DowekAnalyzing logics, analyzing theories, and analyzing proofs |

10:30-11:00 | break |

11:00-11:45 |
Haniel Barbosa, Jasmin Christian Blanchette and Pascal FontaineScalable Fine-Grained Proofs for Formula Processing |

11:45-12:30 |
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui and Pascal FontaineLanguage and proofs for Higher-order SMT (work in progress) |

12:30-14:00 | lunch break |

14:00-14:45 |
Tomer Libal and Xaviera SteeleDeterminism in the Certification of UNSAT Proofs |

14:45-15:30 |
Eunice Palmeira, Fred Freitas and Jens OttenConverting ALC Connection Proofs into ALC Sequents |

15:30-16:00 | break |

16:00-16:45 |
Giselle Reis and Bruno Woltzenlogel PaleoComplexity of Translations from Resolution to Sequent Calculus |

16:45-17:30 |
Dennis Müller, Colin Rothgang, Yufei Liu and Florian RabeAlignment-based Translations Across Formal Systems Using Interface Theories |

17:30-18:15 | PxTP Business Meeting |

**Sunday, 24 September 2017**

9:00-10:30 | Invited speaker:
Cesare TinelliIncreasing automation in Coq via trustworthy cooperation with external automated reasoners |

10:30-11:00 | break |

11:00-11:45 |
Robert LewisAn extensible ad hoc interface between Lean and Mathematica |

11:45-12:30 |
Silvio Ghilardi and Elena PaganiCounter Simulations via Higher Order Quantifier Elimination: a preliminary report |

12:30-14:00 | lunch break |

- Christoph Benzmüller (Freie Universität Berlin)
- Jasmin Blanchette (TU München)
- Hans De Nivelle (Institute of Computer Science, University of Wroclaw)
- Catherine Dubois (ENSIIE),
**co-chair** - Pascal Fontaine (Loria, INRIA, University of Lorraine)
- Stéphane Graham-Lengrand (CNRS - INRIA - Ecole Polytechnique)
- Hugo Herbelin (INRIA)
- Olivier Hermant (MINES ParisTech)
- Cezary Kaliszyk (University of Innsbruck)
- Guy Katz (Stanford University)
- Chantal Keller (LRI, Université Paris-Sud)
- Tomer Libal (INRIA)
- Mariano Moscato (National Institute of Aerospace)
- Vivek Nigam (Universidade Federal da Paraíba)
- Andrei Paskevich (LRI, Université Paris Sud)
- Florian Rabe (Jacobs University Bremen )
- Andrew Reynolds (University of Iowa )
- Stephan Schulz (DHBW Stuttgart)
- Geoff Sutcliffe (University of Miami)
- Josef Urban (Czech Technical University in Prague)
- Tjark Weber (Uppsala University)
- Bruno Woltzenlogel Paleo,
**co-chair** - Akihisa Yamada (University of Innsbruck)