Workshop Description
General Information
The Seventh Workshop on Practical Aspects of Automated Reasoning will take place on June 29-30, 2020 in Paris, France (virtual). PAAR is associated with the 10th International Joint Conference on Automated Reasoning (IJCAR-2020).
Scope
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 brings together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It allows researchers to present their work in progress, and to discuss new implementation techniques and applications.
Topics include but are not limited to:
- 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, optimisation techniques, machine learning, strategies and heuristics, fairness;
- support tools for prover development;
- system descriptions and demos.
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.
Proceedings
- The proceedings are available here as a CEUR Volume.
Submission
Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages) via EasyChair. Those limits are references excluded. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome.
Submissions should be in PDF. Final versions should be prepared in LaTeX using the "easychair.cls" class file. Paper should be submitted through the EasyChair page. PAAR proceedings will be published electronically in the CEUR workshop proceedings.
Important Dates
Due to the 2019-nCoV crisis, the dates are adapted as follow| Abstract submission deadline: | |
| Paper submission deadline: | |
| Author notification: | June 15, 2020 |
| Camera-ready paper versions due: | June 25, 2020 |
| Workshop: | June 29-30, 2020 |
Registration
Registration is free. See the IJCAR registration page.
Program
Note: in order to better accommodate the time constraints of authors and audience, the topic of the papers was not the main criteria to organize sessions.
All sessions will be using Zoom meeting. You have to be registered to PAAR to participate, but registration is free. Mute your microphone during the talks, you can share your camera (or not). By default, we do not interrupt talks for questions (this might be very uncomfortable in videoconference). You can ask questions through the chat during the talk, but the session chair will keep them for the end of the talk.
Talks should be 20 minutes long, 10 minutes are allocated for questions and switching between talks. The session starting time thus precisely defines the theoretical start of each talk. No talk will start earlier.
Discussion topics for coffee breaks can be sent to chairs until the morning of the day of the workshop!
Times are given w.r.t. Paris, France time zone
June 29
| 13:45 - 14:00 |
A word about organization of the workshop. Welcome to PAAR 2020! |
| 14:00 - 15:30
Session 1 Chair: Cláudia Nalon |
Pedro Barroso, António Ravara and Mário Pereira Animated Logic: Correct Functional Conversion to Conjunctive Normal Form Hans de Nivelle Deciding Logical Relations between Inductive Types using Monadic Horn Clauses (presentation only) Constantin Ruhdorfer and Stephan Schulz Efficient Implementation of Large-Scale Watchlists |
| 15:30 - 16:00 | coffee break |
| 16:00 - 17:30
Session 2 Chair: Martin Suda |
Jørgen Villadsen A Micro Prover for Teaching Automated Reasoning (presentation only) Sen Zheng and Renate A. Schmidt Querying the Guarded Fragment via Resolution Nahku Saidy, Hanna Siegfried, Stephan Schulz and Geoff Sutcliffe Cutting down the TPTP language (and others) |
June 30
| 13:30 - 15:30
Session 3 Chair: Geoff Sutcliffe |
Petar Vukmirović and Visa Nummelin Boolean Reasoning in a Higher-Order Superposition Prover Filip Bártek and Martin Suda Learning Precedences from Simple Symbol Features Ahmed Bhayat, Michael Rawson and Giles Reger Reinforcement-Learned External Guidance for Theorem Provers (presentation only) Seulkee Baek The TESC Proof Format for First-Order ATPs |
| 15:30 - 16:00 | coffee break
Giles Reger's announcement: Looking to play with fire? We’re looking for some expert postdocs in model checking/dynamic analysis/theorem proving to work on our new SCorCH project developing formal analysis tools to find security issues in code running on a new generation of security-aware hardware chips. You’ll be able to work with experts in the field and develop close links with our project partners at ARM and Amazon AWS. Meet Giles and get more details during the coffee break! |
| 16:00 - 17:30
Session 4 Chair: Stephan Schulz |
Michael Rawson and Giles Reger Directed Graph Networks for Logical Reasoning Qinghua Liu, Zishi Wu, Zihao Wang and Geoff Sutcliffe Evaluation of Axiom Selection Techniques Bernhard Gleiss and Martin Suda Layered Clause Selection for Saturation-based Theorem Proving |
| 17:30 - 18:00 | coffee break |
| 18:00 - 19:30
Session 5 Chair: Ondřej Lengál |
Benjamin Oliver and Jens Otten Equality Preprocessing in Connection Calculi Robert Lewis and Paul-Nicolas Madelaine Simplifying Casts and Coercions Thomas Prokosch and François Bry Give Reasoning a Trie |
Call For Papers
The Call for Papers is available in plain (UTF-8) text format.
Program Committee
- Simon Cruanes, Aesthetic Integration, Texas, USA
- Hans de Nivelle, Nazarbayev University, Kazakhstan
- Bruno Dutertre, SRI international, California, USA
- Gabriel Ebner, VU Amsterdam, Netherlands
- Pascal Fontaine (co-chair), Liège University, Belgium
- Antti Hyvärinen, University of Lugano, Switzerland
- Ahmed Irfan, Stanford University, California, USA
- Cezary Kaliszyk, University of Innsbruck, Austria
- Daniel Le Berre, CNRS - University of Artois, France
- Ondrej Lengal, Brno University of Technology, Czech Republic
- Tomer Libal, American University of Paris, France
- Cláudia Nalon, University of Brasília, Brasil
- Jens Otten, University of Oslo, Norway
- Philipp Ruemmer (co-chair), Uppsala University, Sweden
- Renate A. Schmidt, The University of Manchester, UK
- Stephan Schulz, DHBW Stuttgart, Germany
- Martina Seidl, Johannes Kepler University Linz, Austria
- Mihaela Sighireanu, IRIF, University Paris Diderot and CNRS, France
- Alexander Steen, University of Luxembourg, Luxembourg
- Martin Suda, Czech Technical University, Czech Republic
- Geoff Sutcliffe, University of Miami, Florida, USA
- Sophie Tourret (co-chair), Max-Planck Institute for Informatics, Germany
- Sarah Winkler, University of Verona, Italy
- Aleksandar Zeljić, Stanford University, California, USA
Previous Workshops
- IJCAR’08 Workshop on Practical Aspects of Automated Reasoning (Sydney, Australia, 2008)
- Second Workshop on Practical Aspects of Automated Reasoning (Edinburgh, UK, 2010)
- Third Workshop on Practical Aspects of Automated Reasoning (Manchester, UK, 2012)
- Fourth Workshop on Practical Aspects of Automated Reasoning (Vienna, Austria, 2014)
- Fifth Workshop on Practical Aspects of Automated Reasoning (Coimbra, Portugal, 2016)
- Sixth Workshop on Practical Aspects of Automated Reasoning (Oxford, UK, 2018)