## 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 DenverAlessio Guglielmi, INRIA Grand-Est & University of Bath

## Organizers

Kai Brünnler, University of BernGeorge 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. |