TABLEAUX 2023 Conference

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

Online Proceedings

http://link.springer.com/openurl.asp?genre=issue&issn=0302-9743&volume=14278

General Information

The 32^nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023) will be hosted by the Czech Technical University in Prague, Czech Republic, September 18-21, 2023.

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 are 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 2023 will be co-located with the 14^th International Symposium on Frontiers of Combining Systems (FroCoS 2023). The conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions.

TABLEAUX 2023 and FroCoS 2023 are planned as in-person conferences. However, virtual participation might be a possibility in exceptional situations.

Scope of Conference

Tableaux and related proof 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, fuzzy, relevance and non-monotonic logics) and their proof-theoretic foundations;
sequent, natural deduction, labelled, nested and deep calculi for classical and non-classical logics, as tools for proof search and proof representation;
related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches);
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, proof assistants, logical frameworks, model checkers, etc.);
implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, etc.);
combinations with machine learning and other AI methods;
techniques for proof generation and compact (or human-readable) proof representation;
theoretical and practical aspects of decision 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 on logical aspects of the solution.

AITP-TABLEAUX Special Track

Besides the main track, TABLEAUX 2023 will host a special track on Artificial Intelligence and Theorem Proving (AITP). The special track invites papers combining machine learning and related AI methods with standard TABLEAUX topics (see above). We welcome full versions of the extended abstracts presented at the AITP conference.

Workshops and Tutorials

Workshop/Tutorial proposals can be made any time up to July 7, 2023. Notification will be provided within one week after submission.

Proposals for workshops/tutorials should contain at least the following pieces of information:

name and contact details of the main organiser(s)
(if applicable:) names of additional organisers
title and organisational style of event (tutorial, public workshop, project workshop, etc.)
preferred length of workshop (between half day and two days)
estimated number of attendees
short (up to one page) description of topic
(if applicable:) pointers to previous editions of the workshop, or to similar events

Publication

The conference proceedings will be published in the Springer series Lecture Notes in Artificial Intelligence (LNAI/LNCS) as Gold Open Access under a CC-BY-4.0-license. The open access costs will be covered by (at most) 100 EUR of the registration fee, and from sponsorships.

See also Paper Submission and Important Dates.

Best Paper Awards

The program committee will select

the TABLEAUX 2023 Best Paper; and,
the TABLEAUX 2023 Best Junior Researcher Paper.

Researchers will be considered “junior” if either they are students or their PhD degree date is less than two years from the first day of the meeting. For a submission to be eligible for the Best Junior Researcher Paper award, more than 50% of the contribution must be made by the junior researcher(s). The two awards will be presented at the conference.