Tableau algorithms for description logics	Franz Baader (with Ulrike Sattler)
Modality and databases	Melvin Fitting
Local symmetries in propositional logic	Alasdair Urquhart (with Noriko H. Arai)

International Conference
TABLEAUX 2000
Automated Reasoning with
Analytic Tableaux and Related Method
University of St Andrews, Scotland
4-7 July, 2000

Design and results of TANCS-2000 non-classical (modal) systems comparison	Fabio Massacci and Francesco M. Donini
Consistency testing: the RACE experience	Volker Haarslev and Ralf Möller
Benchmark analysis with FaCT	Ian Horrocks
MSPASS Modal reasoning by translation and first-order resolution	Ullrich Hustadt and Renate Schmidt
TANCS-2000 results for DLP	Peter F. Patel-Schneider
Evaluating *SAT on TANCS 2000 benchmarks	Armando Tacchella

A labelled tableau calculus for nonmonotonic (cumulative) consequence relations	Alberto Artosi, Guido Governatori and Antonino Rotolo
A tableau system for Gödel-Dummett logic based on a hypersequent calculus	Arnon Avron
An analytic calculus for quantified propositional Gödel logic	Matthias Baaz, Christian Fermüller and Helmut Veith
A tableau method for inconsistency-adaptive logics	Diderik Batens and Joke Meheus
A tableau calculus for integrating first-order reasoning with elementary set theory reasoning	Domenico Cantone and Calogero G. Zarba
Hypertableau and path-hypertableau calculi for some families of intermediate logics	Agata Ciabattoni and Mauro Ferrari
Variants of first-order modal logics	Marta Cialdea Mayer and Serenella Cerrito
Complexity of simple dependent bimodal logics	Stéphane Demri
Properties of Embeddings from Int to S4	Uwe Egly
Term-modal logics	Melvin Fitting, Lars Thalmann and Andrei Voronkov
A subset-matching size-bounded cache for satisfiability in modal logics	Enrico Giunchiglia and Armando Tacchella
Dual intuitionistic logic revisited	Rajeev Goré
Model sets in a nonconstructive logic of partial terms with definite descriptions	Ray Gumb
Search space compression in connection tableau calculi using disjunctive constraints	Ortrun Ibens
Matrix-based inductive theorem proving	Christoph Kreitz and Brigitte Pientka
Monotonic preorders for free variable tableaux	Pedro J. Martín and Antonio Gavilanes
The mosaic method for temporal logics	Maarten Marx, Szabolcs Mikulás and Mark Reynolds
Sequent-like tableau systems with the analytic superformula property for the modal logics KB, KDB, K5, KD5	Linh Anh Nguyen
A tableau calculus for equilibrium entailment	David Pearce, Inmaculada P. de Guzmán and Agustín Valverde
Towards tableau-based decision procedures for non-well-founded fragments of set theory	Carla Piazza and Alberto Policriti
Tableau calculus for only knowing and knowing at most	Riccardo Rosati
A tableau-like representation framework for efficient proof reconstruction	Stephan Schmitt
The semantic tableaux version of the second incompleteness theorem extends almost to Robinson's arithmetic Q	Dan Willard

Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO	Joachim Draeger
E-SETHEO: An automated³ theorem prover	Gernot Stenz and Andreas Wolf

International Conference TABLEAUX 2000 Automated Reasoning with Analytic Tableaux and Related Method University of St Andrews, Scotland 4-7 July, 2000

Invited Lectures

Comparison

Research Papers

System Descriptions Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO Joachim Draeger E-SETHEO: An automated3 theorem prover Gernot Stenz and Andreas Wolf

International Conference
TABLEAUX 2000
Automated Reasoning with
Analytic Tableaux and Related Method
University of St Andrews, Scotland
4-7 July, 2000

System Descriptions

Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO Joachim Draeger

E-SETHEO: An automated³ theorem prover Gernot Stenz and Andreas Wolf