PAAR-2014: Editor's Preface

This volume contains the papers presented at PAAR-2014: the 4th Workshop on Practical Aspects of Automated Reasoning. The workshop was held on July 22, 2014 in Vienna, in association with the 7th International Joint Conference on Automated Reasoning, IJCAR'14 as part of the Vienna Summer of Logic 2014.

This year we received 17 submissions. Each submission was reviewed by at least 2, and on the average 2.9, program committee members. After long and careful discussion, the committee decided to accept 11 papers. The program also included an invited talk Hierarchic Superposition Revisited by Uwe Waldmann. 

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.

The call for papers sulicited paper on topics that include all aspects of automated reasoning including 

  • 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 apsects, benchmarking approaches;
  • non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications;
  • implementation techniques, optimisation techniques, strategies and heuristics, fairness;
  • support tools for prover development;
  • system descriptions and demos.

We are very grateful to the VSL organizers for their support and for hosting the workshop, and are indebted to the EasyChair team for the availability of the EasyChair Conference and Proceedings Publishing Systems. We also thank the program committee members for their timely reviews and spritied discussion.


Leonardo De Moura
Boris Konev
Stephan Schulz
July 2014