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

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