There will be 3 workshops in connection with Tableaux 2009.

FTP 2009 - the workshop on First-Order Theorem Proving

This is a workshop with a long tradition and a high standard. FTP 2009 will take place in the University Library Building on Monday 6 July and Tuesday 7 July.

Nicloas Peltier (LIG, Grenoble, France) and Viorica Sofronie-Stokkermans (MPI, Saarbrücken, Germany) are PC chairs of this workshop.

See the FTP 2009 Web Page for details.

Tableaux versus automata as logical decision methods

This workshop is organized by Valentin Goranko (Technical University of Denmark). It will take place on Monday 6 July, before the main programme of Tableaux.

See the detailed programme.


Terminating semantic tableaux have served for a long time as one of the practically most efficient types of decision procedures for a wide range of logical systems. On the other hand, over the past two decades automata-based methods for testing satisfiability and model checking for various modal and temporal logics of computations have gained very wide recognition and popularity, because they provide uniform, elegant, and often optimal decision procedures.
Furthermore, a number of increasingly efficient automata-based tools have been implemented, and there seems to be a growing perception amongst the formal verification community that these tools are superior and preferable to the tableau-based tools. That perception, however, is not based on systematic comparative analysis, and some practical experience with well-designed tableau-based tools suggest that such perception can be misleading.
Moreover, various optimization techniques, such as on-the-fly methods, draw automata-based algorithms very close to tableau-like procedures, thus strongly suggesting that tableaux and automata are closely related formalisms for deciding logical satisfiability. Yet, few formal technical results to that effect are known, and the scientific discussion on the pros and cons, similarities and differences, between tableaux and automata has so far been rather sporadic.
The purpose of this workshop is to provide an expert forum for such discussion, to provoke and foster discussion between the automata and tableaux communities, and to stimulate further research on the topic.

See the workshop web page and in particular the Call for Papers for details.

Gentzen Systems and Beyond

This workshop is organized by Kai Brünnler (Univ. of Bern, Switzerland) and George Metcalfe (Vanderbilt Univ., Nashville, USA). It will take place on Monday 6 July, before the main programme of Tableaux.

See the detailed programme.


This is a workshop on Gentzen-style proof systems, their generalizations, and extensions. Since the introduction of the Sequent Calculus and Natural Deduction by Gerhard Gentzen in the 1930s, a wide spectrum of formalisms have been used to construct proof systems for logics, including Hypersequents, Display Calculi, Labelled Deductive Systems, Tableaux, Deep Inference, and Proof Nets, to name just a few. The aim of this workshop is to explore and compare the motivations for and relative merits of these different approaches.
Potential topics for talks include: (1) cut-elimination and its applications, such as decidability, interpolation, amalgamation, completeness proofs, computational interpretations, etc. (2) the scope, limitations, interrelationships, and philosophical aspects of various formalisms.
A broader aim of this workshop is to build a bridge between researchers into theoretical aspects of structural proof theory and the more application-oriented goals of the Tableaux community, particularly in cases where the methods, such as constructing analytic systems, are shared.

See the workshop web page for details.

Proofs and Refutations in Non-Classical Logics

This workshop has unfortunately had to be cancelled!

Page last modified on June 18, 2009, at 06:55 PM