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 SpeakersNikolaos Galatos, University of Denver
Alessio Guglielmi, INRIA Grand-Est & University of Bath
OrganizersKai 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
- 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.
|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.|
|11:00||Alessio Guglielmi: Beyond.|
|12:00||Marta Bílková: On uniform interpolation proofs in modal logic.|
|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.|
|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.|