TABLEAUX 2021

The main information:

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.

Submission Guidelines

Submissions are invited in two categories:

A. research papers, which describe original theoretical research or applications, with length up to 15 pages excluding references;
B. 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.

Important Dates

Abstract submission: 19 April 2021 (AoE)
Paper submission: 26 April 2021 (AoE)
Notification: 14 June 2021
TABLEAUX Conference: 6-9 September 2021

Conference Format and COVID-19

TABLEAUX 2021 and FroCoS 2021 are intended to be hybrid conferences welcoming both physical and virtual participation. The organisers are closely monitoring the pandemic situation and may choose to make the conference virtual-only if it seems unreasonable to host any sort of physical event. A final decision will be taken before the notification date 14 June (12 weeks before the conference) to leave ample time for potential travel plans to be made.

Publication

The conference proceedings will be published in the Springer series Lecture Notes in Artificial Intelligence (LNAI/LNCS).

For complete information see the site of Tableaux 2021.