What is this Workshop about?

This is a workshop on Gentzen-style proof systems and generalisations or extensions of them. 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 in particular to explore and compare the motivations for and relative merits of these different approaches. Potential topics include:

  • Cut-elimination and its applications, e.g. decidability, interpolation, amalgamation, completeness proofs, computational interpretations, etc.
  • 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.

Time and Location

The workshop is co-located with Tableaux 2009, and will take place on the 6th of July in Oslo.

Invited Speakers

Nikolaos Galatos, University of Denver
Alessio Guglielmi, INRIA Grand-Est & University of Bath

Organizers

Kai Brünnler, University of Bern
George Metcalfe, Vanderbilt University

Preliminary List of Talks

Arnon Avron
A simple semantic proof of completeness and cut-admissibility for an hypersequential calculus for propositional Gödel logic.
Marta Bílková
On uniform interpolation proofs in modal logic.
Nikolaos Galatos
Sequents, hypersequents and beyond.
Rajeev Goré
Towards automatic cut elimination.
Alessio Guglielmi
Beyond.
Dirk Pattinson
The coalgebraic mu-calculus.
Robert Rothenberg
On the correspondence between hypersequent and labelled calculi for intermediate logics.
Mehrnoosh Sadrzadeh
Cut-free nested sequent calculi for logics with adjoint pairs of modalities.
Lutz Straßburger
Expanding the realm of systematic proof theory.

Preliminary List of Abstracts

Here is a preliminary booklet of abstracts.

Preliminary Program

9:00 Nikolaos Galatos: Sequents, hypersequents and beyond.
10:00 Arnon Avron: A simple semantic proof of completeness and cut-admissibility for an hypersequential calculus for propositional Gödel logic.
10:30 Coffee break
11:00 Alessio Guglielmi: Beyond.
12:00 Marta Bílková: On uniform interpolation proofs in modal logic.
12:30 Lunch break
14:00 Rajeev Goré: Towards automatic cut elimination.
14:30 Mehrnoosh Sadrzadeh: Cut-free nested sequent calculi for logics with adjoint pairs of modalities.
15:00 Dirk Pattinson: The coalgebraic mu-calculus.
15:30 Coffee break
16:00 Robert Rothenberg: On the correspondence between hypersequent and labelled calculi for intermediate logics.
16:30 Lutz Straßburger: Expanding the realm of systematic proof theory.