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

Invited Lectures

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)


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

Research Papers

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

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