This page is no longer updated.

Proof Theory Group at TU Dresden


Electric lamps were not invented by improving candles

Contents
  1. People
  2. Publications
  3. Submitted Papers
  4. International Events Organised by Our Group
  5. Events
  6. Funding
  7. 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.)

1People

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

2Publications

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 title A 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

3Submitted Papers

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

5Events

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 about System 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 about The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference, Charles and Robert about Purity Through Unravelling and Ozan about Implementing Deep Inference in TOM.

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

15-16.6Alessio visits Lutz Straßburger at the Programming Systems Lab (Saarbrücken) and talks about Classical 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 about Labeled Event Structure Semantics of Linear Logic Planning.

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

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

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

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

2004

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

29.11-3.12Charles and Robert visit INRIA's Calligramme group in Nancy; Charles talks about Designing Proof Theories: Handling Modalities and Labels and Robert talks about 3/4s Scott-Lemmon Theories.

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

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

27.10Phiniki successfully defends her MSc thesis The Design of Modal Proof Theories: The Case of S5 and 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:

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

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

9-20.8Ozan participates in the ESSLLI 2004 school (Nancy) and talks about Implementing 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:

In addition:

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

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

31.3-3.4Alessio participates in the Workshop on Constructive Classical Logic (Roma) and talks about The 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 about Linear Logic in the Calculus of Structures and On Proof Nets for Multiplicative Linear Logic with Units.

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

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

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

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

Past years list of events with funding details

6Funding

We are or have been financed by:

Exclusive grant:

7Resources

10.8.2005Alessio Guglielmiemail