Workshop Description

The PxTP workshop welcomes contributions on various aspects of communication, integration, and cooperation between reasoning systems and formalisms. The workshop's mission is to facilitate communication between reasoning tools, building of complex reasoning applications, and reuse of reasoning tools by developing and discussing suitable integration, translation and communication methods, standards, protocols, and programming interfaces.

It is becoming clear that the success of deduction tools will not only depend on their power to solve large and difficult problems in an isolated manner, but it will also rely on their ability to cooperate. The PxTP workshop wants to encourage such cooperation by inviting contributions on various aspects of communication, integration, and cooperation between systems and formalisms. The workshop's mission is to facilitate building of complex reasoning applications and reuse of reasoning tools by developing and discussing suitable integration, translation and communication methods, standards, protocols, and application programming interfaces (APIs). The workshop would like to bring together the interested developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and APIs, and producers of standards and protocols. We are interested both in success stories and in descriptions of the current bottlenecks and proposals for improvement.

Proceedings

The PxTP 2013 proceedings are published electronically as volume 14 in the EasyChair Proceedings in Computing (EPiC) series. The entire proceedings can also be downloaded as a single PDF file.

Invited Speaker

• Thomas C. Hales, University of Pittsburgh, USA

Submission

Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages) via EasyChair. 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.

Submissions should be in PDF. Final versions should be prepared in LaTeX using the "easychair.cls" class file. Paper should be submitted through the EasyChair page. PxTP proceedings will be published electronically in the EasyChair Proceedings in Computing (EPiC) series or in the CEUR workshop proceedings.

Important Dates

Paper submission deadline:	April 11, 2013 April 22, 2013
Author notification:	May 2, 2013 May 9, 2013
Camera-ready paper versions due:	May 9, 2013 May 23, 2013
Workshop:	June 10, 2013 June 9 (from 14:00) and 10 (whole day), 2013

Registration

Registration to PxTP is part of the CADE registration process.
Delegates registering for either June 9 or June 10 are welcome to all sessions of PxTP.

Program

June 9

14:00-16:00	Christoph Benzmueller and Nik Sultana LEO-II version 1.5 Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler Efficient and Verified Checking of Unsatisfiability Proofs [presentation only] Geoff Sutcliffe The TPTP Jungle and the TPI Language [presentation only] Josef Urban An Overview of Human-Oriented Proof Transformation Attempts [presentation only]
16:00-16:30	coffee break
16:30-17:30	Jasmin Christian Blanchette Redirecting Proofs by Contradiction Panel discussion—possible topics: cooperation between reasoning (and related) tools common formats for problems and proofs proof presentation and manipulation (e.g. compression, redirection)

June 10

9:00-10:30	Invited Speaker: Thomas C. Hales External Tools for the Formal Proof of the Kepler Conjecture Cezary Kaliszyk and Josef Urban Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
10:30-11:00	coffee break
11:00-12:30	Ramana Kumar Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4 Cezary Kaliszyk and Alexander Krauss Towards Scalable HOL Import [presentation only] Steffen Juilf Smolka and Jasmin Christian Blanchette Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
12:30-14:00	lunch break
14:00-16:00	Guillaume Burel A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo Nada Habli and Amy Felty Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs Chantal Keller Extended Resolution as Certificates for Propositional Logic Zakaria Chihani, Dale Miller, and Fabien Renaud Checking foundational proof certificates for first-order logic
16:00-16:30	coffee break
16:30-18:00	Chad E. Brown and Christine Rizkallah From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction Cezary Kaliszyk and Thomas Sternagel Initial experiments on deriving a complete HOL simplification set Panel discussion—possible topics: cooperation between reasoning (and related) tools common formats for problems and proofs proof presentation and manipulation (e.g. compression, redirection)

Call For Papers

[.txt]

Program Committee

• Jasmin Christian Blanchette (co-chair), TU München, Germany
• Chad Brown, Saarland University, Germany
• David Delahaye, CEDRIC/CNAM, Paris, France
• Ewen Denney, SGT/NASA Ames, USA
• Peter Dybjer, Chalmers University, Sweden
• Pascal Fontaine, Loria, INRIA, University of Nancy, France
• John Harrison, Intel Corporation, USA
• Warren Hunt, University of Texas, USA
• Chantal Keller, Laboratoire d'Informatique de Polytechnique, France
• Konstantin Korovin, Manchester University, UK
• Magnus O. Myreen, University of Cambridge, UK
• Jens Otten, University of Potsdam, Germany
• Andrei Paskevich, Université Paris-Sud 11, IUT d'Orsay, France
• Lawrence C. Paulson, University of Cambridge, UK
• David Pichardie, INRIA Rennes - Bretagne Atlantique, France
• Florian Rabe, Jacobs University Bremen, Germany
• Stephan Schulz, TU München, Germany
• Aaron Stump, CS Department, University of Iowa, USA
• Geoff Sutcliffe, University of Miami, USA
• Laurent Théry, INRIA, France
• Josef Urban (co-chair), Radboud Universiteit Nijmegen, Netherlands
• Tjark Weber, Uppsala University, Sweden