Third Workshop on Practical Aspects of Automated Reasoning

(PAAR-2012)

 

GENERAL INFORMATION


  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.


SCOPE


  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.


  3. Topics include but are not limited to:


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

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

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

  8. ‣pragmatics of automated reasoning within proof assistants;

  9. ‣practical experiences, usability aspects, feasibility studies;

  10. ‣evaluation of implementation techniques and automated reasoning tools;

  11. ‣performance aspects, benchmarking approaches;

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

  13. ‣implementation techniques, optimization techniques, strategies and heuristics, fairness;

  14. ‣support tools for prover development;

  15. ‣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.


SUBMISSIONS


  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.


  3. 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.


  5. 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.


IMPORTANT DATES


  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



INVITED TALKS


  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.



PROGRAM


  1. Saturday, 30 June 2012

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


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

  5.             Building an Efficient OWL 2 DL Reasoner


  7. 10:00-10:30 Coffee break


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


  11.             Daniel Kuehlwein and Josef Urban

  12.             Learning from Multiple Proofs: First Experiments


  14.             Jesse Alama

  15.             Escape to Mizar from ATPs


  17.             Cezary Kaliszyk and Josef Urban

  18.             Initial Experiments with External Provers and Premise Selection

  19.             on HOL Light Corpora


  21. 12:00-13:30 Lunch break


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


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

  26.             MetTeL2: Towards a Tableau Prover Generation Platform


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

  29.             Synthesising and Implementing Tableau Calculi for Interrogative

  30.             Epistemic Logics


  32.             Christoph Benzmueller, Jens Otten and Thomas Raths

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


  35. 15:00-15:30 Coffee break


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


  39.             Alexander Leitsch and Tomer Libal

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


  42.             Martina Seidl, Florian Lonsing and Armin Biere

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


  45.             Christoph Weidenbach and Patrick Wischnewski

  46.             Satisfiability Checking and Query Answering for large Ontologies


  48. Sunday, 1 July 2012

  49. ===================


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

  52.             Practical Aspects of SAT Solving


  54. 10:00-10:30 Coffee break


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


  58.             Diego Caminha Barbosa de Oliveira and David Monniaux

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

  60.             in an SMT solver


  62.             Tianyi Liang and Cesare Tinelli

  63.             Exploiting parallelism in the Model Evolution calculus


  65.            Anthony Monnet and Roger Villemaire

  66.             CDCL with Less Destructive Backtracking through Partial Ordering


  68. 12:00-13:30 Lunch break


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


  72.             Rajeev Gore and Jimmy Thomson

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

  74.             progress report


  76.             Md Zahidul Islam and Wendy MacCaull

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


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

  80.             Authorization Enforcement in Workflows: Maintaining Realizability

  81.             Via Automated Reasoning


  83. 15:00-15:30 Coffee break


  85. 15:30       End



PROGRAM COMMITTEE


  1. Pascal Fontaine (Co-chair)

  2. Renate Schmidt (Co-chair)

  3. Stephan Schulz (Co-Chair)


  5. Clark Barrett

  6. Peter Baumgartner

  7. Christoph Benzmüller

  8. Jasmin Christian Blanchette

  9. Chad Brown

  10. Koen Claessen

  11. Martin Giese

  12. Alberto Griggio

  13. John Harrison

  14. Yevgeny Kazakov

  15. Konstantin Korovin

  16. Daniel Le Berre

  17. Hans de Nivelle

  18. Albert Oliveras

  19. Nicola Ollivetti

  20. Jens Otten

  21. Jeff Pan

  22. Lawrence Paulson

  23. Adam Pease

  24. Nicolas Peltier

  25. Ruzica Piskac

  26. Stefan Schlobach

  27. Geoff Sutcliffe

  28. Laurent Théry

  29. Dmitry Tishkovsky

  30. Christoph Weidenbach

  31. Florian Widmann

  32. Christoph M. Wintersteiger

  1. INRIA and University of Nancy

  2. University of Manchester

  3. Technische Universität München


  5. New York University

  6. NICTA

  7. Freie Universität Berlin

  8. Technische Universität München

  9. Universität des Saarlandes

  10. Chalmers University

  11. University of Oslo

  12. Fondazione Bruno Kessler

  13. Intel

  14. Universität Ulm

  15. University of Manchester

  16. Université d'Artois

  17. Uniwersytet Wrocławski

  18. Universitat Politècnica de Catalunya

  19. Université Paul Cézanne

  20. Universität Potsdam

  21. University of Aberdeen

  22. University of Cambridge

  23. Articulate Software

  24. CNRS

  25. Max-Planck-Institute for Software Systems

  26. Vrije Universiteit Amsterdam

  27. University of Miami

  28. INRIA Sophia-Antipolis

  29. University of Manchester

  30. Max-Planck-Institut für Informatik

  31. Australian National University

  32. Microsoft Research




PREVIOUS WORKSHOPS


  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)