This page is no longer updated.

**Proof Theory Group at TU Dresden**

Electric lamps were not invented by improving candles

- People
- Publications
- Submitted Papers
- International Events Organised by Our Group
- Events
- Funding
- Resources

Most of our research concerns the *calculus of structures*, which is a computation-motivated proof-theoretical formalism we developed. Its most direct analog is Gentzen's *sequent calculus*.

We know that systems in the sequent calculus can be interpreted computationally, in the proof-normalisation-as-computation and proof-search-as-computation paradigms. Many aspects of computation are not managed satisfactorily by the sequent calculus, especially some important for distributed computation, like *locality*, *atomicity* and several kinds of *modularity*. This holds for all logics expressed in the sequent calculus, including, e.g., linear logic.

The calculus of structures addresses these problems in a radically new, purely proof-theoretical foundation, based on the principles of *deep inference* and *top-down symmetry*. We expressed *classical logic*, *linear logic*, *modal logics*, and several variants thereof, and their deductive systems are as simple as those in the sequent calculus, but possess the desired computational properties. This new proof theory is richer than the old one, e.g., there are new interesting notions of *normalisation*.

Besides the theoretical foundations, we are pursuing applications in the *design of languages* for *concurrency* and *planning*, since the new formalism possesses unifying features that allow a common specification of these otherwise distinct application areas.

Other topics of interest to our group are proof search, uniform provability and proof nets.

The Calculus of Structures—Project Report

Alessio Guglielmi's web page on deep inference and the calculus of structures (FAQ, papers, notes, etc.)

The following persons are or have been members of our group.

- Kai Brünnler, former PhD student here, now a researcher in Gerhard Jäger's group in Bern
- Paola Bruscoli, researcher
- Alessio Guglielmi, researcher
- Robert Hein, former MSc student here
- Steffen Hölldobler, professor
- Ozan Kahramanogullari, PhD student
- Charles Stewart, researcher
- Phiniki Stouppa, former MSc student here, now a PhD student in Gerhard Jäger's group in Bern
- Lutz Straßburger, former PhD student here, former researcher in INRIA's Calligramme group, now a researcher in the Programming Systems Lab at Universität des Saarlandes
- Alwen Tiu, former MSc student here, then a PhD student with Dale Miller, now a researcher at INRIA

I list here accepted, peer-reviewed, proof-theoretical papers written by members of our group while in Dresden; other papers, PhD theses, technical reports and notes are available from the calculus of structures web page and the personal pages of group members.

**To Appear**

On Structuring Proof Search for First Order Linear Logic

Paola Bruscoli and Alessio Guglielmi

Journal version pdfJuly 6, 2004

Technical Report WV-03-10, accepted pending minor revisions by Theoretical Computer ScienceBibTeX

A System of Interaction and Structure

Alessio Guglielmi

PdfAugust 30, 2004

Technical Report WV-02-10, to appear on ACM Transactions on Computational LogicBibTeX

A Systematic Proof Theory for Several Modal Logics

Charles Stewart and Phiniki Stouppa

PdfSeptember 2, 2004

Technical Report WV-03-08, accepted at Advances in Modal Logic 2004, to appear in proceedings published by King's College PublicationsBibTeX

System BV Is NP-Complete

Ozan Kahramanogullari

PdfApril 11, 2005

Accepted at WoLLIC 2005

**2005**

Towards Planning as Concurrency

Ozan Kahramanogullari

PdfOctober 19, 2004

Artificial Intelligence and Applications 2005, ACTA Press, pp. 197–202BibTeX

**2004**

System BV without the Equalities for Unit

Ozan Kahramanogullari

Pdf© Springer-VerlagAugust 4, 2004

ISCIS 2004, LNCS 3280, pp. 986–995BibTeX

Deep Inference and Symmetry in Classical Proofs

Kai Brünnler

Pdf© Logos VerlagFebruary 2004

PhD thesis, successfully defended on 22.9.2003, published by Logos VerlagBibTeX

You can buy this book here and here

A First Order System with Finite Choice of Premises

Kai Brünnler and Alessio Guglielmi

PdfDecember 1, 2003

Presented at First Order Logic 75 under the titleA Finitary System for First Order Logic; appeared in Hendricks et al., editor, First-Order Logic Revisited, Logos Verlag, Berlin, 2004, pp. 59–74BibTeX

**2003**

A Tutorial on Proof Theoretic Foundations of Logic Programming

Paola Bruscoli and Alessio Guglielmi

Pdf© Springer-VerlagSeptember 10, 2003

Invited tutorial at ICLP 2003, LNCS 2916, pp. 109–127BibTeX

Two Restrictions on Contraction

Kai Brünnler

PdfNovember 24, 2003

Logic Journal of the Interest Group in Pure and Applied Logics, Vol. 11 No. 5, pp. 525–529BibTeX

MELL in the Calculus of Structures

Lutz Straßburger

PdfNovember 24, 2003

Theoretical Computer Science, Vol. 309, pp. 213–285BibTeX

On Structuring Proof Search for First Order Linear Logic

Paola Bruscoli and Alessio Guglielmi

Conference version pdf© Springer-VerlagSeptember 10, 2003

LPAR 2003, LNCS 2850, pp. 389–406BibTeX

Atomic Cut Elimination for Classical Logic

Kai Brünnler

Pdf© Springer-VerlagApril 10, 2003

CSL 2003, LNCS 2803, pp. 86–97BibTeX

System NEL Is Undecidable

Lutz Straßburger

PdfAugust 20, 2003

WoLLIC 2003, Electronic Notes in Theoretical Computer Science 84BibTeX

**2002**

A Local System for Linear Logic

Lutz Straßburger

Pdf© Springer-VerlagAugust 9, 2002

LPAR 2002, LNAI 2514, pp. 388–402BibTeX

A Non-commutative Extension of Multiplicative Exponential Linear Logic

Alessio Guglielmi and Lutz Straßburger

Pdf© Springer-VerlagAugust 9, 2002

LPAR 2002, LNCS 2514, pp. 231–246BibTeX

A Purely Logical Account of Sequentiality in Proof Search

Paola Bruscoli

Pdf© Springer-VerlagAugust 12, 2002

ICLP 2002, LNCS 2401, pp. 302–316BibTeX

**2001**

A Local System for Classical Logic

Kai Brünnler and Alwen Fernanto Tiu

Pdf© Springer-VerlagOctober 2, 2001

LPAR 2001, LNAI 2250, pp. 347–361BibTeX

Non-commutativity and MELL in the Calculus of Structures

Alessio Guglielmi and Lutz Straßburger

Pdf© Springer-VerlagJune 28, 2001

CSL 2001, LNCS 2142, pp. 54–68BibTeX

**2005**

Reducing the Nondeterminism in the Calculus of Structures

Ozan Kahramanogullari

PostscriptApril 11, 2005

Submitted

A Deep Inference System for the Modal Logic S5

Phiniki Stouppa

PdfJune 13, 2005

Submitted

**2004**

A New Logical Notion of Partial Order Planning

Ozan Kahramanogullari

PdfJune 13, 2004

Technical Report, submittedBibTeX

**2003**

A Non-commutative Extension of Multiplicative Exponential Linear Logic

Alessio Guglielmi and Lutz Straßburger

PdfJanuary 21, 2004

Technical Report WV-02-03, submitted to Mathematical Structures in Computer ScienceBibTeX

Locality for Classical Logic

Kai Brünnler

PdfJanuary 22, 2003

Technical Report WV-03-04, submittedBibTeX

**4International Events Organised by Our Group**

- Structures and Deduction workshop at ICALP 2005 in Lisbon (16-17.7.2005)
- ICCL Workshop Proof Theory 2005 (21-23.2.2005)
- ICCL Workshop Proof Theory 2004 (27-28.9.2004)
- ICCL Summer School 2004 - Proof Theory and Automated Theorem Proving (14-25.6.2004)
- Workshop on Structural Proof Theory (19-21.11.2003)
- Summer School and Workshop on Proof Theory, Computation and Complexity (23.6-4.7.2003)
- Workshop on Proof Theory and Computation (3-14.6.2002)
- Workshop in Proof Theory (8.12.2000)

**2005**

1.9Alessio and Paola move to the University of Bath.

9-12.8Kai (Bern) visits us.

19-22.7Ozan participates in the WoLLIC 2005 conference (Florianópolis - Brazil) and talks aboutSystem BV Is NP-Complete.

16-17.7Charles and Paola co-organise the workshop Structures and Deduction at next ICALP 2005 in Lisbon; at the workshop, Alessio talks aboutThe Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference, Charles and Robert aboutPurity Through Unravellingand Ozan aboutImplementing Deep Inference in TOM.

17.6Alessio visits Thomas Streicher (TU Darmstadt) and talks aboutThe How and Why of Deep Inference.

15-16.6Alessio visits Lutz Straßburger at the Programming Systems Lab (Saarbrücken) and talks aboutClassical Logic in Deep Inference and Some Ideas on Proof Search.

2-7.5Michel Parigot (PPS group, Paris) visits us.

20-21.4Alessio visits Michel Parigot (PPS group) in Paris.

31.3-3.4Ozan participates in the UNILOG 2005 conference (Montreux) and talks aboutLabeled Event Structure Semantics of Linear Logic Planning.

23.3Robert successfully defends his MSc thesisGeometric Theories and Modal Logic in the Calculus of Structuresand he gets the grade 1.0 (the highest possible).

21-24.2We organise the ICCL Workshop Proof Theory 2005; the following guests visit us:

22-24.2Yves Guiraud (Marseille)21-24.2Lutz Straßburger (Saarbrücken)21-24.2Kai Brünnler (Bern)21-23.2Richard McKinley (Bath)21-23.2Alwen Tiu (LORIA, Nancy)

14-16.2Ozan participates in the AIA 2005 conference (Innsbruck) and talks aboutTowards Planning as Concurrency.

7.2Alessio visits the computer science department at University of Bath and gives a talk aboutDeep Inference.

**2004**

9-15.12Alessio visits the PPS group in Paris, participates in the Paris-Vienna Workshop 2004 on Proofs and talks aboutReasons and Methods of Deep Inference.

29.11-3.12Charles and Robert visit INRIA's Calligramme group in Nancy; Charles talks aboutDesigning Proof Theories: Handling Modalities and Labelsand Robert talks about3/4s Scott-Lemmon Theories.

22.11-17.12Ozan visits INRIA's Calligramme and Protheo groups in Nancy and gives a talk aboutImplementing Deep Inference.

27-29.10Ozan participates in the ISCIS 2004 conference (Kemer–Antalya) and talks aboutSystem BV without the Equalities for Unit.

27.10Phiniki successfully defends her MSc thesisThe Design of Modal Proof Theories: The Case of S5and she gets the grade 1.0 (the highest possible); she joins as a graduate student Gerhard Jäger's group in Bern.

27-28.9We organise the ICCL Workshop Proof Theory 2004; the following guests visit us:

27.9-1.10Roy Dyckhoff (St Andrews)27.9-1.10Nissim Francez (Technion Haifa)27.9-1.10Michel Parigot (CNRS, Paris)27-29.9Stéphane Lengrand (St Andrews and Paris VII)27-29.9Lutz Straßburger (LORIA, Nancy)27-28.9Kai Brünnler (Bern)27-28.9Ugo Dal Lago (Bologna)27-28.9Jeremy Dawson (NICTA, Canberra)27-28.9Birgit Elbl (Universität der Bundeswehr München)27-28.9José Espírito Santo (Universidade do Minho)20.9-1.10Elaine Pimentel (Belo Horizonte and Torino)20-29.9François Lamarche (Loria & INRIA, Nancy)

9-11.9Charles and Phiniki participate in the AiML 2004 conference (Manchester) and talk aboutA Systematic Proof Theory for Several Modal Logics.

16-20.8Alessio participates in the ESSLLI 2004 school (Nancy) and lectures onThe Calculus of Structures.

9-20.8Ozan participates in the ESSLLI 2004 school (Nancy) and talks aboutImplementing System BV of the Calculus of Structures in Maude.

14-25.6We organise the ICCL Summer School 2004 - Proof Theory and Automated Theorem Proving; the following guests visit us and participate as indicated:

21-25.6Roy Dyckhoff (St Andrews) gives an invited lecture onSequent Calculi for Some Non-classical Logics.21-25.6Claude Kirchner (Loria & INRIA, Nancy) lectures onDeduction Modulo.21-25.6John Slaney (NICTA, Canberra and Australian National University) lectures onAutomated Reasoning for Substructural Logics.16-18,21-27.6Michel Parigot (CNRS - Université Paris 7) lectures onProofs as Programs.14-25.6François Lamarche (Loria & INRIA, Nancy) lectures onLogic Considered as a Branch of Geometry.14-18.6Andrei Voronkov (Manchester) lectures onAutomated Theorem Proving for Classical Logics.14-16.6Luke Ong (Oxford) lectures onGame Semantics and Its Applications.14-16.6Simona Ronchi della Rocca (Torino) gives an invited lecture onA Logic for Intersection Types.14.6Wolfgang Bibel (TU Darmstadt and Un. British Columbia) gives an invited lecture onTransition Logic.In addition:

14-17.6Franz Baader (TU Dresden) lectures onTerm Rewriting Systems.14-17.6Alessio lectures onDeep Inference and the Calculus of Structures.

3.6Alessio visits the PPS group in Paris and gives a talk aboutDeep Inference and Self-dual Non-commutativity.

13.5Lutz visits the SIGNES group in Bordeaux and gives a talk aboutThe Calculus of Structures.

31.3-3.4Alessio participates in the Workshop on Constructive Classical Logic (Roma) and talks aboutThe Need for Deep Inference in Proof Theory.

22-23.3Lutz visits the Laboratoire de Géométrie, Topologie et Algèbre in Montpellier and gives two talks aboutLinear Logic in the Calculus of StructuresandOn Proof Nets for Multiplicative Linear Logic with Units.

1-5.3Lutz participates in the 9th Estonian Winter School in Computer Science (Palmse) and talks aboutThe Calculus of Structures.

1-5.3Prakash Panangaden (McGill and Oxford University) visits us and talks aboutConcurrent Common Knowledge : Agreement and Causal Consistency in Distributed Systems.

12.2Lutz visits the PPS group in Paris and gives a talk aboutThe Calculus of Structures.

26-27.1Lutz participates in the Géométrie du Calcul meeting (Marseille) and talks aboutThe Calculus of Structures.

Past years list of events with funding details

We are or have been financed by:

- CoLogNet
- Consolato Generale d'Italia - Lipsia/Italienisches Generalkonsulat in Leipzig
- Deutscher Akademischer Austausch Dienst
- Graduiertenkolleg 334 Spezifikation Diskreter Prozesse und Prozesssysteme Durch Operationelle Modelle und Logiken
- International Masters Programme in Computational Logic
- International Quality Network Rational Mobile Agents and Systems of Agents
- Sächsische Ministerium für Wissenschaft und Kunst
*Programme HWP*

Exclusive grant:

- DAAD grant Procope
*Structures and Deductions*, for scientific exchanges with INRIA's group Calligramme, in 2003 and 2004 (total amount for our group 7400 EUR, Calligramme has separate funding)

- Rules for the names of systems and notation
- Example files, macros, fonts, etc.
- Groucho's repository of papers (access is restricted to colleagues for copyright reasons)

10.8.2005Alessio Guglielmiemail