TABLEAUX 2021

General Information

The 30^th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021) will be hosted by the University of Birmingham, UK, 6-9 September 2021. It will primarily be a virtual conference, due to ongoing conerns about COVID-19. However it will be possible to attend the conference physically for those who are able to travel to Birmingham and take advantage of a hybrid format. More information can be found here.

TABLEAUX is the main international conference at which research on all aspects -- theoretical foundations, implementation techniques, systems development and applications -- of tableaux-based reasoning and related methods is presented. The first TABLEAUX conference was held in Lautenbach near Karlsruhe, Germany, in 1992. Since then it has been organised on an annual basis (sometimes as a part of IJCAR).

TABLEAUX 2021 will be co-located with the 13^th International Symposium on Frontiers of Combining Systems (FroCoS 2021). The conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions.

Scope of conference

Tableaux and other proof based methods offer convenient and flexible tools for automated reasoning for both classical and non-classical logics. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis.

Topics of interest include but are not limited to:

• tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, linear, substructural, relevance, non-monotonic logics) and their proof-theoretic foundations;
• related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches);
• sequent, natural deduction, labelled, nested and deep calculi for classical and non-classical logics, as tools for proof search and proof representation;
• flexible, easily extendable, light weight methods for theorem proving;
• novel types of calculi for theorem proving and verification in classical and non-classical logics;
• systems, tools, implementations, empirical evaluations and applications (provers, logical frameworks, model checkers, ...);
• implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, ...);
• extensions of tableau procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs;
• decision procedures, theoretically optimal procedures;
• applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching.

We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the TABLEAUX community and should focus on the role of reasoning, and logical aspects of the solution.

Invited Speakers

TABLEAUX 2021 is pleased to confirm the following invited speakers:

Michael Benedikt (University of Oxford, UK). Joint with FroCoS.
Orna Kupferman (Hebrew University, Israel).
Revantha Ramanayake (University of Gröningen, The Netherlands).
Greg Restall (University of Melbourne, Australia / University of St Andrews, UK).
Renate Schmidt (University of Manchester, UK). Joint with FroCoS.

Submission Guidelines

The submission deadline has now passed.

Submissions are invited in two categories:

• research papers, which describe original theoretical research or applications, with length up to 15 pages excluding references;
• system descriptions, with length up to 9 pages excluding references.

There will also be a later call inviting position papers and brief reports on work-in-progress. Details will be kept up to date on the website.

Submissions will be reviewed by the PC, possibly with the help of external reviewers, taking into account readability, relevance and originality. Any additional material (going beyond the page limit) can be included in a clearly marked appendix, which will be read at the discretion of the committee and must be removed for the camera-ready version.

For category (A) submissions, the reported results must be original and not submitted for publication elsewhere. For category (B) submissions, a working implementation must be accessible via the internet. Authors are encouraged to publish the implementation under an open source license. The aim of a system description is to make the system available in such a way that people can use it, understand it, and build on it. Accepted papers in categories (A) and (B) will be published in the conference proceedings.

Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via the EasyChair system:
https://easychair.org/conferences/?conf=tableaux21.

For all accepted papers at least one author is required to register to the conference and present the paper. A title and a short abstract of about 100 words must be submitted before the paper submission deadline. Formatting instructions and the LNCS style files can be obtained at:
http://www.springer.com/br/computer-science/lncs/conference-proceedings-guidelines.

Accepted Papers

We are pleased to announce that the following papers have been selected for presentation at TABLEAUX 2021 and publication in the conference proceedings.

• AC simplifications and closure redundancies in the superposition calculus. André Duarte and Konstantin Korovin.
• Tableaux for Free Logics with Descriptions. Andrzej Indrzejczak and Michal Zawidzki.
• Basing Sequent Systems on Exclusive Or. Arnon Avron.
  
• Uniform interpolation from cyclic proofs: the case of modal mu-calculus. Bahareh Afshari, Graham Leigh and Guillermo Menéndez Turata.
• From Input/Output Logics to Conditional Logics via Sequents - With Provers. Bjoern Lellmann.
  
• A formally verified cut-elimination procedure for linear nested sequents for tense logic. Caitlin D'Abrera, Jeremy Dawson and Rajeev Goré.
• Cyclic hypersequent calculi for some modal logics with the master modality. Jan Rooduijn.
• The nanoCoP 2.0 Provers for Classical, Intuitionistic and Modal Logics. Jens Otten.
• A Focus System for the Alternation-Free Mu-Calculus. Johannes Marti and Yde Venema.
• Learning Theorem Proving Components. Karel Chvalovský, Jan Jakubuv, Miroslav Olšák and Josef Urban.
• Analytic Tableaux for Non-Deterministic Semantics. Lukas Grätz.
• Constraint tableaux for two-dimensional fuzzy logics. Marta Bilkova, Sabine Frittella and Daniil Kozhemiachenko.
• Game Semantics for Constructive Modal Logic. Matteo Acclavio, Davide Catta and Lutz Straßburger.
• The Došen Square under construction: A tale of four modalities. Michael Mendler, Stephan Scheele and Luke Burke.
• Eliminating Models during Model Elimination. Michael Rawson and Giles Reger.
• lazyCoP: Lazy Paramodulation meets Neurally Guided Search. Michael Rawson and Giles Reger.
• Proof-Theory and Semantics for a Theory of Definite Descriptions. Nils Kurbis.
• CEGAR-Tableaux: improved modal satisfiability via modal clause-learning and SAT. Rajeev Goré and Cormac Kikkert.
• Cut-elimination for provability logic by terminating proof search: formalised and deconstructed using Coq. Rajeev Goré, Revantha Ramanayake and Ian Shillito.
• Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs. Stepan Kuznetsov.
• Tableaux and Restricted Quantification for Systems Related to Weak Kleene Logic. Thomas Ferguson.
• Nested Sequents for Intuitionistic Modal Logics via Structural Refinement. Tim Lyon.
• Terminating Calculi and Countermodels for Constructive Modal Logics. Tiziano Dalmonte, Charles Grellois and Nicola Olivetti.
• Proof Search on Bilateralist Judgments over Non-deterministic Semantics. Vitor Greati, Sérgio Marcelino and João Marcos.
• Towards Finding Longer Proofs. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk and Josef Urban.
• The Role of Entropy in Guiding a Connection Prover. Zsolt Zombori, Josef Urban and Miroslav Olsak.