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


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.



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: April 8, 2020 May 2, 2020
Paper submission deadline: April 15, 2020 May 9,2020
Author notification: June 15, 2020
Camera-ready paper versions due: June 25, 2020
Workshop: June 29-30, 2020
The workshop will be virtual. We are in discussion with IJCAR and other workshops to find the best solution so that the presentations will be optimally advertised and get the best possible feedback.


Registration is free. See the IJCAR registration page.


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

Previous Workshops

More information on the Practical Aspects of Automated Reasoning Workshop (PAAR) Series page.