PAAR 2022

8th Workshop on Practical Aspects of Automated Reasoning

Important Dates
Paper Submission
Accepted Papers
Invited Speakers

Previous workshops


This year’s PAAR is colocated with the WG2 COST EuroProofNet kickoff meeting. Please checkout its site for more information about the meeting.

This is a draft program, and might still change slightly.

  Thursday, August 11 (Day 1)
Session 1  
09:00-10:00 Josef Urban (invited talk), title: Training ENIGMAs, CoPs, and other thinking creatures
10:00-10:30 QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Maximilian Heisinger, Martina Seidl and Armin Biere
  Coffee break
Session 2  
11:00 - 11:30 A Two-Watched Literal Scheme for First-Order Logic
Martin Bromberger, Tobias Gehl, Lorenz Leutgeb and Christoph Weidenbach
11:30 - 12:00 Lazy Paramodulation in Practice
Grzegorz Prusak and Cezary Kaliszyk
12:00 - 12:30 Empirical Properties of Term Orderings for Superposition
Stephan Schulz
  Lunch break
Session 3  
14:00 - 14:30 Exploring Partial Models with SCL
Martin Bromberger, Simon Schwarz and Christoph Weidenbach
14:30 - 15:00 On SGGS and Horn Clauses
Maria Paola Bonacina and Sarah Winkler
15:00 - 15:30 Exploring Representation of Horn clauses using GNNs
Chencheng Liang, Philipp Rümmer and Marc Brockschmidt
  Coffee break
Session 4  
16:00 - 16:30 Optimal Strategy Schedules for Everyone
Hans-Jörg Schurr
16:30 - 17:00 The Vampire Approach to Induction
Marton Hajdu, Laura Kovacs, Michael Rawson and Andrei Voronkov
17:00 - 17:30 Reuse of Introduced Symbols in Automatic Theorem Provers
Michael Rawson, Martin Suda, Petra Hozzová and Giles Reger

  Friday, August 12 (Day 2)
Session 1  
09:00-10:00 Geoff Sutcliffe (invited talk), title: The Logic Languages of the TPTP World
10:00-10:30 Automated Reasoning in Non-classical Logics in the TPTP World
Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe and Christoph Benzmüller
  Coffee break
Session 2  
11:00 - 11:30 Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Christoph Wernhard
11:30 - 12:00 An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
Alexander Steen
12:00 - 12:30 The Isabelle Community Benchmark
Fabian Huch and Vincent Bode
  Lunch break
Session 3  
14:00 - 14:05 short COST action EuroProofNet introduction
14:05 - 14:50 Guillaume Burel (ENSIIE): EuroProofNet presentation on proofs in Dedukti
14:50 - 15:35 Andres Notzli (U Stanford): EuroProofNet presentation on SMT and proofs
  Coffee break
Session 4  
16:00 - 16:45 Discussion on SMT proofs (joint with SMT workshop)
16:45 - 17:30 WG 2 business meeting and planning