Topics

Tableau 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 brings together researchers interested in all aspects --- theoretical foundations, implementation techniques, systemsdevelopment and applications --- of the mechanization of reasoning with tableaux and related methods.

Topics of interest include (but are not restricted to):

• analytic tableaux for various logics (theory and applications)
• related techniques and concepts, e.g., model checking and BDDs
• related methods (model elimination, sequent calculi, connection method, ...)
• new calculi and methods for theorem proving in classical and non-classical logics (modal, description, intuitionistic, linear, temporal, ...)
• systems, tools, implementations and applications (e.g. verification)

One or more TUTORIALS will be part of the conference programme.

The Tableaux 2000 conference will feature a COMPARISON of theorem provers, TANCS (TABLEAUX Comparison for Non-Classical Systems), organized by Fabio Massacci of Universitå di Siena.