PAAR-2012: Editor's Preface

This volume contains the papers presented at the Third Workshop on Practical Aspects of Automated Reasoning (PAAR-2012). The workshop was held on June 30 and July 1, 2012, in Manchester, UK, in association with the Sixth International Joint Conference on Automated Reasoning (IJCAR-2012), as part of the Alan Turing Year 2012, held just after The Alan Turing Centenary Conference.

PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brought together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It allowed researchers to present their work in progress, and to discuss new implementation techniques and applications. Papers were solicited on topics that include all practical aspects of automated reasoning. More specifically, some suggested topics were:

• automated reasoning in propositional, first-order, higher-order and non-classical logics;
• implementation of provers (SAT, SMT, resolution, tableau, instantiation-based, rewriting, logical frameworks, etc);
• automated reasoning tools for all kinds of practical problems and applications;
• pragmatics of automated reasoning within proof assistants;
• practical experiences, usability aspects, feasibility studies;
• evaluation of implementation techniques and automated reasoning tools;
• performance aspects, benchmarking approaches;
• non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications;
• implementation techniques, optimization techniques, strategies and heuristics, fairness;
• support tools for prover development;
• system descriptions and demos.

We were particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems in practice, and how to apply existing systems to real problems.

The workshop this year was particularly successful. We received seventeen submissions, for a workshop whose duration was initially one day. Each submission was reviewed by three program committee members. Due to the quality of the submissions, and to prevent the workshop to be intolerably selective, we decided to extend the duration of the event to two days. Also, the AREIS Workshop on Automated Reasoning for Enterprise Information Systems joined PAAR as a special session. In the end and altogether, nineteen papers were submitted, fifteen of which were accepted for presentation. The program included two invited talks:

• Practical Aspects of SAT Solving, by Armin Biere,
• Building an Efficient OWL 2 DL Reasoner, by Boris Motik.

Besides a session on the topic of AREIS, PAAR shared a session with the PxTP Workshop on Proof eXchange for Theorem Proving, and included a joint invited talk with the SMT Workshop on Satisfiability Modulo Theories.

The workshop organizers would like to thank the following people for helping to make PAAR a success.

• the authors and participants of the workshop;
• the invited speakers;
• the program committee and the reviewers for their effort;
• Peter Baumgartner and Silvio Ranise, the organizers of the AREIS Workshop, for proposing to group PAAR and AREIS;
• the organizers of the PxTP Workshop, for including the PAAR session on proofs in the PxTP program and making it a joint PAAR-PxTP session;
• the organizers of the SMT workshop, for the organization of the joint SMT-PAAR invited talk.

We are very grateful to the IJCAR organizers for their support and for hosting the workshop, and are indebted to the EasyChair team for the availability of the EasyChair Conference System.