Program

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