The Coq mailing list

[Josef Urban <josef.urban AT gmail.com>]

TABLEAUX 2023 - PRELIMINARY CALL FOR PAPERS

The 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
Prague, Czech Republic, September 18-21, 2023

Website: http://tableaux2023.tableaux-ar.org
Submission deadlines: May 9 (abstract), May 14, 2023 (paper)

GENERAL INFORMATION
The 32nd 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 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 2023 will be co-located with the 14th 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.

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 (http://aitp-conference.org/2023/).

WORKSHOPS AND TUTORIALS
If you would like to organize a workshop or run a tutorial, please let us know before July 14, 2023.

INVITED SPEAKERS
To be announced.

SUBMISSION GUIDELINES 
Submissions are invited in the following two categories: 
(A) regular papers reporting original theoretical research or applications. Up to 15 pages excluding references;   
(B) short papers such as system descriptions, user experiences, case studies and domain models. Up to 9 pages excluding references.

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

Submissions must be unpublished and not submitted for archival publication elsewhere. If software or data is relevant to a paper, a link that provides access to the software/data must be provided to enable reproduction of the results. 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/my/conference?conf=tableaux2023

For all accepted papers, at least one author is required to register for 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
Submission of title and abstract: May 9, 2023
Paper submission deadline: May 14, 2023
Notification of acceptance: July 9, 2023
Final version: July 23, 2023
Conference date: September 18-21, 2023

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

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 from sponsorships and from the registration fees of all participants.

BEST PAPER AWARDS
The program committee will select
* the TABLEAUX 2023 Best Paper; and,
* the TABLEAUX 2023 Best Paper by a Junior Researcher.

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. The two awards will be presented at the conference.

TRAVEL GRANTS FOR STUDENTS
Some funding may be available to support students participating at TABLEAUX 2023. More details will be given on the conference website in due time.

PROGRAM COMMITTEE
To be announced.

PC CHAIRS 
Revantha Ramanayake (University of Groningen, The Netherlands)
Josef Urban (Czech Technical University in Prague, Czech Republic)

LOCAL ORGANIZERS
Karel Chvalovsky (Czech Technical University in Prague, Czech Republic)
Jan Jakubuv (Czech Technical University in Prague, Czech Republic)
Martin Suda (Czech Technical University in Prague, Czech Republic)
Josef Urban (Czech Technical University in Prague, Czech Republic)