Third Workshop on Practical Aspects of Automated Reasoning




  1. The Third Workshop on Practical Aspects of Automated Reasoning was held on June 30th amd July 1st, 2012 in Manchester, UK. PAAR was be associated with the 6th International Joint Conference on Automated Reasoning (IJCAR-2012), part of the Alan Turing Year 2012, and collocated with The Alan Turing Centenary Conference.

The Workshop Proceedings are now available.


  1. 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 will bring together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It will allow researchers to present their work in progress, and to discuss new implementation techniques and applications.

  2. Topics include but are not limited to:

  3. automated reasoning in propositional, first-order, higher-order and non-classical logics;

  4. implementation of provers (SAT, SMT, resolution, tableau, instantiation-based, rewriting, logical frameworks, etc);

  5. automated reasoning tools for all kinds of practical problems and applications;

  6. pragmatics of automated reasoning within proof assistants;

  7. practical experiences, usability aspects, feasibility studies;

  8. evaluation of implementation techniques and automated reasoning tools;

  9. performance aspects, benchmarking approaches;

  10. non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications;

  11. implementation techniques, optimization techniques, strategies and heuristics, fairness;

  12. support tools for prover development;

  13. system descriptions and demos.

If you do not submit to PAAR, Stan the T. Rex at the Manchester Museum will eat you!

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


  1. Researchers interested in participating are invited to submit a short abstract of up to 10 pages via EasyChair. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions.

  2. Submissions should be in standard-conforming PDF. To submit a paper, go to the EasyChair PAAR page  and follow the instructions there. Final versions should be prepared in LaTeX using the easychair.cls class file. Proceedings will be published as CEUR Workshop Proceedings and will be available  in print at the event.

  3. If quality and quantity of the submissions warrants this, we plan to produce a special issue of a recognized journal on the topic of the workshop.


  1. Submission of papers/abstracts:

  2. Notification of acceptance:

  3. Camera ready versions due:

  4. Workshop:

  1. May 3rd, 2012

  2. May 24th, 2012

  3. May 31st, 2012

  4. June 30th-July 1st, 2012


  1. Practical Aspects of SAT Solving

    Armin Biere, Johannes-Kepler-Universiät Linz

  1. SAT solving techniques are used in many automated reasoning engines. This talk gives an overview on recent developments in practical aspects of SAT solver development. Beside improvements of the basic conflict driven clause learning (CDCL) algorithm, we also discuss improving and integrating advanced preprocessing techniques as inprocessing during search. The talk concludes with a brief overview on current trends in parallelizing SAT.


  1. Building an Efficient OWL 2 DL Reasoner

    Boris Motik, University of Oxford

  1. The Ontology Web Language (OWL) has received considerable traction recently and is used in a number of industrial and practical applications. While decidable, all basic reasoning tasks for OWL are intractable (most of them are N2ExpTime-complete). Thus, in order to obtain a system capable of solving practically-relevant nontrivial problems, a number of theoretical and practical issues need to be resolved. In my talk I will present an overview of the techniques employed in HermiT -- a state-of-the-art OWL reasoner developed at Oxford University. I will present the main ideas behind the hypertableau calculus and contrast them with the tableau calculi used in similar systems. Furthermore, I will discuss optimization techniques used in HermiT such as the blocking cache, individual reuse, and core blocking. Finally, I will discuss certain higher-level optimizations implemented on top of the basic calculus, such as the recently-developed optimized classification algorithm.


  1. Saturday, 30 June 2012

  2. ======================

  3. 9:00-10:00 Invited Talk: Boris Motik

  4.             Building an Efficient OWL 2 DL Reasoner

  5. 10:00-10:30 Coffee break

  6. 10:30-12:00 (Proofs/HOL - Joint session with PxTP-2012)

  7.             Daniel Kuehlwein and Josef Urban

  8.             Learning from Multiple Proofs: First Experiments

  9.             Jesse Alama

  10.             Escape to Mizar from ATPs

  11.             Cezary Kaliszyk and Josef Urban

  12.             Initial Experiments with External Provers and Premise Selection

  13.             on HOL Light Corpora

  14. 12:00-13:30 Lunch break

  15. 13:30-15:00 (Tableaux/ML)

  16.             Dmitry Tishkovsky, Renate A. Schmidt and Mohammad Khodadadi

  17.             MetTeL2: Towards a Tableau Prover Generation Platform

  18.             Stefan Minica, Mohammad Khodadadi, Renate A. Schmidt and Dmitry Tishkovsky

  19.             Synthesising and Implementing Tableau Calculi for Interrogative

  20.             Epistemic Logics

  21.             Christoph Benzmueller, Jens Otten and Thomas Raths

  22.             Implementing Different Proof Calculi for First-order Modal Logics

  23. 15:00-15:30 Coffee break

  24. 15:30-17:00 (Resolution/EPR)

  25.             Alexander Leitsch and Tomer Libal

  26.             A Resolution Calculus for Second-order Logic with Eager Unification

  27.             Martina Seidl, Florian Lonsing and Armin Biere

  28.             qbf2epr: A Tool for Generating EPR Formulas from QBF

  29.             Christoph Weidenbach and Patrick Wischnewski

  30.             Satisfiability Checking and Query Answering for large Ontologies

  31. Sunday, 1 July 2012

  32. ===================

  33. 9:00-10:00 Invited Talk (Joint session with SMT-2012): Armin Biere

  34.             Practical Aspects of SAT Solving

  35. 10:00-10:30 Coffee break

  36. 10:30-12:00 (SMT/SAT/ME)

  37.             Diego Caminha Barbosa de Oliveira and David Monniaux

  38.             Experiments on the feasibility of using a floating-point simplex

  39.             in an SMT solver

  40.             Tianyi Liang and Cesare Tinelli

  41.             Exploiting parallelism in the Model Evolution calculus

  42.            Anthony Monnet and Roger Villemaire

  43.             CDCL with Less Destructive Backtracking through Partial Ordering

  44. 12:00-13:30 Lunch break

  45. 13:30-15:00 (AREIS/TL)

  46.             Rajeev Gore and Jimmy Thomson

  47.             BDD-based automated reasoning in propositional non-classical logics:

  48.             progress report

  49.             Md Zahidul Islam and Wendy MacCaull

  50.             A One-Pass Tableau-Based Workflow Verification Framework

  51.             Jason Crampton, Michael Huth and Jim Huan-Pu Kuo

  52.             Authorization Enforcement in Workflows: Maintaining Realizability

  53.             Via Automated Reasoning

  54. 15:00-15:30 Coffee break

  55. 15:30       End


  1. INRIA and University of Nancy

  2. University of Manchester

  3. Technische Universität München

  4. New York University

  5. NICTA

  6. Freie Universität Berlin

  7. Technische Universität München

  8. Universität des Saarlandes

  9. Chalmers University

  10. University of Oslo

  11. Fondazione Bruno Kessler

  12. Intel

  13. Universität Ulm

  14. University of Manchester

  15. Université d'Artois

  16. Uniwersytet Wrocławski

  17. Universitat Politècnica de Catalunya

  18. Université Paul Cézanne

  19. Universität Potsdam

  20. University of Aberdeen

  21. University of Cambridge

  22. Articulate Software

  23. CNRS

  24. Max-Planck-Institute for Software Systems

  25. Vrije Universiteit Amsterdam

  26. University of Miami

  27. INRIA Sophia-Antipolis

  28. University of Manchester

  29. Max-Planck-Institut für Informatik

  30. Australian National University

  31. Microsoft Research


  1. IJCAR’08 Workshop on Practical Aspects of Automated Reasoning (Sydney, Australia, 2008)

  2. Second Workshop on Practical Aspects of Automated Reasoning (Edinburgh, UK, 2010)