Edited by David Pichardie and Tjark Weber
Proceedings Copyright c 2012 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors. The goal of the PxTP workshop series is to bring together researchers working on proof production from automated theorem provers with potential consumers of proofs. Machine-checkable proofs have been proposed for applications like proof-carrying code and certi ed compilation, as well as for exchanging knowledge between di erent automated reasoning systems. For example, interactive theorem provers can import results from otherwise untrusted high-performance solvers, by means of proofs the solvers produce. In such situations, one automated reasoning tool can make use of the results of another, without having to trust that the second tool is sound. It is only necessary to be able to reconstruct a proof that the rst tool will accept, in order to import the result without increasing the size of the trusted computing base.
This simple idea of proof exchange for theorem proving becomes quite complicated under the real-world constraints of highly complex and heterogeneous proof producers and proof consumers. For example, even the issue of a standard proof format for a single class of solvers, like SMT solvers, is quite di cult to address, as di erent solvers use di erent inference systems. It may be quite challenging, from an engineering and possibly also theoretical point of view, to t these into a single standard format. Emerging work from several groups proposes standard meta-languages or parametrised formats to achieve exibility while retaining a universal proof language.
PxTP 2012, the Second International Workshop on Proof Exchange for Theorem Proving, was held as a satellite event of IJCAR on June 30, 2012, in Manchester, UK. The workshop featured invited talks by Robert L. Constable and Stephan Merz, a joint session with the Third Workshop on Practical Aspects of Automated Reasoning (PAAR 2012), and presentations of the ve accepted papers that are collected in this volume. We would like to thank the IJCAR organisers, the PxTP program committee, the authors and speakers, and everyone else who contributed to the workshop's success.
David Pichardie and Tjark Weber Co-chairs, PxTP 2012 Program Committee
The