32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods

Important Dates
Paper Submission
Invited Speakers
Venue & Travel
Best Papers


Available online:


All Tableaux talks are in the Red Room.

Tuesday 19th September

08:40-09:00 Registration/Front desk
09:00-09:05 Conference welcome
09:05-09:25 Wolfgang Bibel
Invited Talk
Reasoning Research Viewed in Broad Terms
09:25-10:25 Roman Kuznets
Invited Talk
Always Look on Both Sides of Proof
(Chair: Jens Otten)
10:25-10:50 Ian Shillito, Iris van der Giessen, Rajeev Gore and Rosalie Iemhoff A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
10:50-11:20 Coffee break (Respirium)
Session: Sequent calculi (Chair: TBA)
11:20-11:45 Timo Lang Some Analytic Systems of Rules
11:45-12:10 Andrzej Indrzejczak and Nils Kürbis A cut-free, sound and complete Russellian theory of definite descriptions
12:10-12:35 Andrzej Indrzejczak Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators
12:35-14:00 Lunch (Respirium)
Session: Modal logics I (Chair: Andrzej Indrzejczak)
14:00-15:00 Rosalie Iemhoff
Invited Talk
Proof Systems and Termination
15:00-15:25 Iris van der Giessen, Raheleh Jalali and Roman Kuznets Extensions of K5: Proof Theory and Uniform Lyndon Interpolation
15:25-15:50 Anupam Das and Sonia Marin On intuitionistic diamonds (and lack thereof)
15:50-16:20 Coffee break (Respirium)
Session: Modal logics II (Chair: Roman Kuznets)
16:20-16:45 Tiziano Dalmonte and Andrea Mazzullo NP Complexity for Combinations of Non-Normal Modal Logics
16:45-17:10 Dirk Pattinson, Nicola Olivetti and Cláudia Nalon Resolution-based Calculi for Non-Normal Modal Logics
17:10-17:35 Tim Lyon and Eugenio Orlandelli Nested Sequents for Quantified Modal Logics
17:35-18:00 Matteo Acclavio, Davide Catta and Federico Olimpieri Canonicity of Proofs in Constructive Modal Logic

Wednesday 20th September

08:40-09:00 Registration/Front desk
09:00-10:00 Valentin Goranko
Invited Talk - Joint with FroCoS
Combining Semantic Tableaux
(Chair: Rosalie Iemhoff)
10:00-10:30 Coffee break (Respirium)
Session: Tableaux calculi (Chair: Nicolas Peltier)
10:30-10:55 Christoph Wernhard Range-Restricted and Horn Interpolation through Clausal Tableaux
10:55-11:10 Carlos Areces, Valentin Cassano, Raul Fervari and Guillaume Hoffmann DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics
(Short Paper)
11:10-11:35 Ineke Van Der Berg, Andrea De Domenico, Giuseppe Greco, Krishna Manoorkar, Alessandra Palmigiano and Mattia Panettiere Non-distributive description logic
Session: Separation Logics (Chair: Didier Galmiche)
11:35-12:00 Frank de Boer, Hans Dieter Hiep and Stijn de Gouw The Logic of Separation Logic: Models and Proofs
12:00-12:25 Nicolas Peltier Testing the Satisfiability of Formulas in Separation Logic with Permissions
12:25-14:00 Lunch (Respirium)
Excursion & Conference dinner
14:00-18:00 Transport and excursion to Karlštejn castle
18:00-22:00 Transport and conference dinner in Unětice

Thursday 21th September

Session: Linear logic and MV-algebras I (Chair: Revantha Ramanayake)
09:00-09:25 Alexander Gheorghiu, Tao Gu and David Pym Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic
09:25-10:25 Marta Bílková
Invited Talk - Joint with FroCoS
Epistemic Logics of Structured Intensional Groups: Agents - groups - names-types
10:25-10:55 Coffee break (Respirium)
Session: Linear Logic and MV-algebras II (Chair: Timo Lang)
10:55-11:20 Zuzana Haniková, Felip Manyà and Amanda Vidal The MaxSAT problem in the real-valued MV-algebra
Session: Non-wellfounded proofs (Chair: Sonia Marin)
11:20-11:45 Alexis Saurin A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points
11:45-12:10 Bahareh Afshari, Lide Grotenhuis, Graham Leigh and Lukas Zenger Ill-founded Proof Systems For Intuitionistic Linear-time Temporal Logic
12:10-12:35 Maurice Dekker, Johannes Kloibhofer, Johannes Marti and Yde Venema Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata
12:35-14:00 Lunch & best paper awards ceremony (Respirium)
14:00-15:00 Chad E. Brown
Invited Talk - Joint with FroCoS
First-Order Instantiation-Based Tableau
(Chair: Martin Suda)
15:00-15:30 Coffee break (Respirium)
Session: Theorem proving (Chair: Josef Urban)
15:30-15:55 Michael Rawson, Christoph Wernhard, Zsolt Zombori and Wolfgang Bibel Lemmas: Generation, Selection, Application
15:55-16:10 Bartosz Piotrowski, Ramon Fernández Mir and Edward Ayers Machine-Learned Premise Selection for Lean
(Short Paper)
16:10-16:25 Boris Shminke gym-saturation: Gymnasium environments for saturation provers (System description)
(Short Paper)
16:25-16:40 Clemens Eisenhofer, Ruba Alassaf, Michael Rawson and Laura Kovacs Non-Classical Logics in Satisfiability Modulo Theories
(Short Paper)
16:40-16:55 Asta Halkjær From and Jørgen Villadsen A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness
(Short Paper)
17:00-18:00 Business meeting