PxTP 2013: Editor's Preface

The Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013) was held as a satellite event of the 24th International Conference on Automated Deduction (CADE-24) on June 9 and 10, 2013 in Lake Placid, New York.

The workshop featured an invited talk by Thomas C. Hales, presentations of the eleven accepted papers that are collected in this volume, and additional presentations by Pascal Fontaine (on behalf of Bruno Woltzenlogel Paleo), Cezary Kaliszyk (joint work with Alexander Krauss), Geoff Sutcliffe, and Josef Urban.

The focus of the workshop were various aspects of communication, integration, and cooperation between reasoning systems and formalisms. It is becoming clear that the success of deduction tools does not only depend on their power to solve large and difficult problems in an isolated manner, but also depends on their ability to cooperate.

The workshop's mission was thus 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. The final number of accepted submissions clearly shows that cooperation of reasoning systems is a thriving topic drawing the attention of researchers in automatic and interactive theorem proving.

We would like to thank the CADE organizers, the PxTP program committee, the authors and speakers, Andrei Voronkov of EasyChair, and everyone else who contributed to the workshop's success.