TABLEAUX 2027

36th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
Marseille, France
September 27th — September 29th


Website under construction

Aims

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 2027 will be co-located with the 17th International Symposium on Frontiers of Combining Systems (FroCoS 2027).

Scope

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

Topics of interest include but are not limited to:

  • tableaux 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.