PAAR 2022
Practical Aspects of Automated Reasoning 2022

Table of Contents

• Preface
  Summary: There were 15 papers submitted for peer-review to this workshop. Out of these, 14 papers were accepted for this volume, 11 as regular papers, and 3 as short papers.

Session 1:

• Josef Urban (invited talk)
  Training ENIGMAs, CoPs, and other thinking creatures ,
• QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
  Maximilian Heisinger , Martina Seidl , Armin Biere

Session 2:

• A Two-Watched Literal Scheme for First-Order Logic
  Martin Bromberger , Tobias Gehl , Lorenz Leutgeb , Christoph Weidenbach
• Lazy Paramodulation in Practice
  Grzegorz Prusak , Cezary Kaliszyk
• Empirical Properties of Term Orderings for Superposition
  Stephan Schulz

Session 3:

• Exploring Partial Models with SCL
  Martin Bromberger , Simon Schwarz , Christoph Weidenbach
• On SGGS and Horn Clauses
  Maria Paola Bonacina , Sarah Winkler
• Exploring Representation of Horn clauses using GNNs
  Chencheng Liang , Philipp Rümmer , Marc Brockschmidt

Session 4:

• Optimal Strategy Schedules for Everyone
  Hans-Jörg Schurr
• The Vampire Approach to Induction (short paper)
  Marton Hajdu , Laura Kovacs , Michael Rawson , Andrei Voronkov
• Reuse of Introduced Symbols in Automatic Theorem Provers (short paper)
  Michael Rawson , Martin Suda , Petra Hozzová , Giles Reger

Session 5:

• The Logic Languages of the TPTP World and Proofs and Models in the TPTP World (invited talk)
  Geoff Sutcliffe
• Automated Reasoning in Non-classical Logics in the TPTP World
  Alexander Steen , David Fuenmayor , Tobias Gleißner , Geoff Sutcliffe , Christoph Benzmüller

Session 6:

• Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
  Christoph Wernhard
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning (short paper)
  Alexander Steen
• The Isabelle Community Benchmark
  Fabian Huch , Vincent Bode