Regular papers

Matthias Baaz and Agata Ciabattoni, Vienna U of Techn., Austria
A Schütte-Tait style cut-elimination proof for first-order Gödel logic

Patrick Blackburn, LORIA Nancy, France and Maarten Marx, U Amsterdam, The Netherlands
Tableaux for quantified hybrid logic

Nathalie Chetcuti-Sperandio, IRIT Toulouse, France
Tableau-based automated deduction for duration calculus

Anatoli Degtyarev, Michael Fisher, and Boris Konev; U Liverpool, UK
A simplified clausal resolution procedure for propositional linear-time temporal logic

Thomas Eiter, Volker Klotz, Hans Tompits, and Stefan Woltran; Vienna U of Techn., Austria
Modal nonmonotonic logics revisited: Efficient encodings for the basic reasoning tasks

Mauro Ferrari, U Milan, Italy; Camillo Fiorentini, U Milan, Italy; and Guido Fiorino, Varese U, Italy
Tableau calculi for the logics of finite k-ary trees

Martin Giese, Karlsruhe U, Germany
A model generation style completeness proof for constraint tableaux with superposition

Jan Hladik, Dresden U of Techn., Germany
Implementation and optimization of a tableau algorithm for the guarded fragment

Reinhold Letz, Techn. U of Munich, Germany
Lemma and model caching in decision procedures for quantified boolean formulas

Reinhold Letz and Gernot Stenz, Techn. U of Munich, Germany
Integration of equality reasoning into the disconnection calculus

Marta Cialdea Mayer and Carla Limongelli, U Rome III, Italy
Linear time logic, conditioned models and planning with incomplete knowledge

George Metcalfe, King's College London, UK; Nicola Olivetti, U Turin, Italy; and Dov Gabbay, King's College London, UK
Analytic sequent calculi for abelian and Lukasiewicz logics

Linh Anh Nguyen, Warsaw U, Poland
Analytic tableau systems for propositional bimodal logics of knowledge and belief

Uwe Petermann, Leipzig U of Applied Sciences, Germany
A confluent theory connection calculus

Viorica Sofronie-Stokkermans, MPI Saarbrücken, Germany
Deciding uniform word problems involving bridging operators on bounded distributive lattices

Balder ten Cate, U Amsterdam, The Netherlands and Chung-chieh Shan, Harvard U, USA
Question answering: from partitions to prolog

Virginie Thion, U Paris XI (Paris-Sud), France; Serenella Cerrito, U Paris XI (Paris-Sud), France; and Marta Cialdea Mayer, U Rome III, Italy
A general theorem prover for quantified modal logics

Dan E. Willard, State U of New York-Albany, USA
Some new exceptions for the semantic tableaux version of the second incompletness theorem

Claus-Peter Wirth, Saarland U, Germany
A new indefinite semantics for Hilbert's epsilon

Calogero G. Zarba, Stanford U, USA
A tableau calculus for combining non-disjoint theories

Position papers

Frank M. Brown, U Kansas, USA
A tableaux based system for propositional nonmonotonic logics

Guido Fiorino, Varese U, Italy
Improving the treatment of negation in propositional Dummett logic

Reiner Hähnle, Chalmers U of Techn., Sweden; Neil V. Murray, State U of New York-Albany, USA; and Erik Rosenthal, U New Haven, USA
Unit preference for ordered resolution and for connection graph resolution

Jens Happe, Simon Fraser U, Canada
Free-variable tableaux for efficient deduction in K

James Harland, RMIT U, Australia
Search calculi for classical and intuitionistic logic

Georg Moser, Vienna U of Techn., Austria
Epsilon, delta, and speed-ups

Breanndán Ó Nualláin, U Amsterdam, The Netherlands
Constraint tableaux

Regimantas Pliuskevicius, Inst. of Mathematics and Informatics, Vilnius, Lithuania
A parametrical similarity saturation based decision procedure for a fragment of FTL

Norbert Preining, Vienna U of Techn., Austria
Proof theory and proof systems for projective and affine geometry

System descriptions

Luc Habert, Jean-Marc Notin, and Didier Galmiche; LORIA Nancy, France
LINK: a proof environment based on proof nets

Gernot Stenz, Techn. U of Munich, Germany
DCTP 1.2