TABLEAUX 2013 - The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods

This conference is the 22nd in a series international meetings on Automated Reasoning with Analytic Tableaux and Related Methods held 1992 in Lautenbach (Germany), 1993 in Marseille (France), 1994 in Abingdon (UK), 1995 in St. Goar (Germany), 1996 in Terrasini (Italy), 1997 in Pont-à-Mousson (France), 1998 in Oisterwijk (Netherlands), 1999 in Saratoga Springs (USA), 2000 in St Andrews (Scotland), 2002 in Copenhagen (Denmark), 2003 in Rome (Italy), 2005 in Koblenz (Germany), 2007 in Aix-en-Provence (France), 2009 in Oslo (Norway), and 2011 in Bern (Switzerland).
In 2001 TABLEAUX was part of IJCAR 2001 in Siena, in 2004 it was part of IJCAR 2004 in Cork (Ireland), in 2006 it was part of IJCAR 2006 in Seattle (United States of America), in 2008 it was part of IJCAR 2008 in Sydney (Australia), in 2010 it was part of IJCAR 2010 in Edinburgh (United Kingdom), and in 2012 it was part of IJCAR 2012 in Manchester (United Kingdom).
Proceedings of Tableaux 2013 will appear in the series Springer Lecture Notes in Artificial Intelligence (LNAI).
See the main TABLEAUX page for general details about this series of meetings.
RELEVANT TOPICS
Tableaux methods are a convenient formalism for automating deduction in various non-standard logics as well as in classical logic. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, and system diagnosis. The conference intends to bring together researchers interested in all aspects - theoretical foundations, implementation techniques, system developments and applications - of the mechanization of reasoning with tableaux and related methods.
Topics of interest include (but are not restricted to):
proof-theory in classical and non-classical logics (modal, temporal, description, intuitionistic, sub-structural, ...)
analytic tableaux for various logics (theory and applications)
related techniques and concepts, e.g., model checking and BDDs
related methods (model elimination, sequent calculi, resolution, connection method, ...)
new calculi and methods for theorem proving and verification in classical and non-classical logics
systems, tools, implementations and applications (provers, logical frameworks, model checkers, ...)
automated deduction and formal methods applied to logic, mathematics, software development, protocol verification, security, ...
TABLEAUX 2013 also welcomes applications of formal methods to real world examples. Papers describing applications of tableaux and related methods in areas such as, for example, hardware and software verification, knowledge engineering, semantic web, etc. are particularly invited.
One or more tutorials will be part of the Conference program.