Please note that this newsitem has been archived, and may contain outdated information or links.
6 - 9 September 2021, The 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021), Birmingham (UK) and Virtual
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.
TABLEAUX 2021 will be co-located with the 13th 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.
Submissions are invited in the following two categories: (A) research papers reporting original theoretical research or applications, with length up to 15 pages excluding references; (B) system descriptions, with length up to 9 pages excluding references.
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.);
* extensions of tableau procedures with conflict-driven learning;
* techniques for proof generation and compact (or humanly 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.
Please note that this newsitem has been archived, and may contain outdated information or links.