This page is no longer updated.
Proof Theory Group at TU Dresden
Electric lamps were not invented by improving candles
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 StructuresProject 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.
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 GuglielmiAugust 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 StouppaSeptember 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 KahramanogullariApril 11, 2005
Accepted at WoLLIC 2005
2005
Towards Planning as Concurrency
Ozan KahramanogullariOctober 19, 2004
Artificial Intelligence and Applications 2005, ACTA Press, pp. 197202BibTeX
2004
System BV without the Equalities for Unit
Ozan Kahramanogullari© Springer-Verlag
August 4, 2004
ISCIS 2004, LNCS 3280, pp. 986995BibTeX
Deep Inference and Symmetry in Classical Proofs
Kai Brünnler© Logos Verlag
February 2004
PhD thesis, successfully defended on 22.9.2003, published by Logos VerlagBibTeX
You can buy this book here and hereA First Order System with Finite Choice of Premises
Kai Brünnler and Alessio GuglielmiDecember 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. 5974BibTeX
2003
A Tutorial on Proof Theoretic Foundations of Logic Programming
Paola Bruscoli and Alessio Guglielmi© Springer-Verlag
September 10, 2003
Invited tutorial at ICLP 2003, LNCS 2916, pp. 109127BibTeX
Two Restrictions on Contraction
Kai BrünnlerNovember 24, 2003
Logic Journal of the Interest Group in Pure and Applied Logics, Vol. 11 No. 5, pp. 525529BibTeX
MELL in the Calculus of Structures
Lutz StraßburgerNovember 24, 2003
Theoretical Computer Science, Vol. 309, pp. 213285BibTeX
On Structuring Proof Search for First Order Linear Logic
Paola Bruscoli and Alessio Guglielmi
Conference version pdf© Springer-Verlag
September 10, 2003
LPAR 2003, LNCS 2850, pp. 389406BibTeX
Atomic Cut Elimination for Classical Logic
Kai Brünnler© Springer-Verlag
April 10, 2003
CSL 2003, LNCS 2803, pp. 8697BibTeX
System NEL Is Undecidable
Lutz StraßburgerAugust 20, 2003
WoLLIC 2003, Electronic Notes in Theoretical Computer Science 84BibTeX
2002
A Local System for Linear Logic
Lutz Straßburger© Springer-Verlag
August 9, 2002
LPAR 2002, LNAI 2514, pp. 388402BibTeX
A Non-commutative Extension of Multiplicative Exponential Linear Logic
Alessio Guglielmi and Lutz Straßburger© Springer-Verlag
August 9, 2002
LPAR 2002, LNCS 2514, pp. 231246BibTeX
A Purely Logical Account of Sequentiality in Proof Search
Paola Bruscoli© Springer-Verlag
August 12, 2002
ICLP 2002, LNCS 2401, pp. 302316BibTeX
2001
A Local System for Classical Logic
Kai Brünnler and Alwen Fernanto Tiu© Springer-Verlag
October 2, 2001
LPAR 2001, LNAI 2250, pp. 347361BibTeX
Non-commutativity and MELL in the Calculus of Structures
Alessio Guglielmi and Lutz Straßburger© Springer-Verlag
June 28, 2001
CSL 2001, LNCS 2142, pp. 5468BibTeX
2005
Reducing the Nondeterminism in the Calculus of Structures
Ozan Kahramanogullari
PostscriptApril 11, 2005
SubmittedA Deep Inference System for the Modal Logic S5
Phiniki StouppaJune 13, 2005
Submitted
2004
A New Logical Notion of Partial Order Planning
Ozan KahramanogullariJune 13, 2004
Technical Report, submittedBibTeX
2003
A Non-commutative Extension of Multiplicative Exponential Linear Logic
Alessio Guglielmi and Lutz StraßburgerJanuary 21, 2004
Technical Report WV-02-03, submitted to Mathematical Structures in Computer ScienceBibTeX
Locality for Classical Logic
Kai BrünnlerJanuary 22, 2003
Technical Report WV-03-04, submittedBibTeX
4International Events Organised by Our Group
2005
1.9
Alessio and Paola move to the University of Bath.
9-12.8
Kai (Bern) visits us.
19-22.7
Ozan participates in the WoLLIC 2005 conference (Florianópolis - Brazil) and talks about System BV Is NP-Complete.
16-17.7
Charles 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.6
Alessio visits Thomas Streicher (TU Darmstadt) and talks about The How and Why of Deep Inference.
15-16.6
Alessio 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.5
Michel Parigot (PPS group, Paris) visits us.
20-21.4
Alessio visits Michel Parigot (PPS group) in Paris.
31.3-3.4
Ozan participates in the UNILOG 2005 conference (Montreux) and talks about Labeled Event Structure Semantics of Linear Logic Planning.
23.3
Robert 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.2
We organise the ICCL Workshop Proof Theory 2005; the following guests visit us:
- 22-24.2
Yves Guiraud (Marseille)
- 21-24.2
Lutz Straßburger (Saarbrücken)
- 21-24.2
Kai Brünnler (Bern)
- 21-23.2
Richard McKinley (Bath)
- 21-23.2
Alwen Tiu (LORIA, Nancy)
14-16.2
Ozan participates in the AIA 2005 conference (Innsbruck) and talks about Towards Planning as Concurrency.
7.2
Alessio visits the computer science department at University of Bath and gives a talk about Deep Inference.
2004
9-15.12
Alessio 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.12
Charles 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.12
Ozan visits INRIA's Calligramme and Protheo groups in Nancy and gives a talk about Implementing Deep Inference.
27-29.10
Ozan participates in the ISCIS 2004 conference (KemerAntalya) and talks about System BV without the Equalities for Unit.
27.10
Phiniki 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.9
We organise the ICCL Workshop Proof Theory 2004; the following guests visit us:
- 27.9-1.10
Roy Dyckhoff (St Andrews)
- 27.9-1.10
Nissim Francez (Technion Haifa)
- 27.9-1.10
Michel Parigot (CNRS, Paris)
- 27-29.9
Stéphane Lengrand (St Andrews and Paris VII)
- 27-29.9
Lutz Straßburger (LORIA, Nancy)
- 27-28.9
Kai Brünnler (Bern)
- 27-28.9
Ugo Dal Lago (Bologna)
- 27-28.9
Jeremy Dawson (NICTA, Canberra)
- 27-28.9
Birgit Elbl (Universität der Bundeswehr München)
- 27-28.9
José Espírito Santo (Universidade do Minho)
- 20.9-1.10
Elaine Pimentel (Belo Horizonte and Torino)
- 20-29.9
François Lamarche (Loria & INRIA, Nancy)
9-11.9
Charles and Phiniki participate in the AiML 2004 conference (Manchester) and talk about A Systematic Proof Theory for Several Modal Logics.
16-20.8
Alessio participates in the ESSLLI 2004 school (Nancy) and lectures on The Calculus of Structures.
9-20.8
Ozan participates in the ESSLLI 2004 school (Nancy) and talks about Implementing System BV of the Calculus of Structures in Maude.
14-25.6
We organise the ICCL Summer School 2004 - Proof Theory and Automated Theorem Proving; the following guests visit us and participate as indicated:
- 21-25.6
Roy Dyckhoff (St Andrews) gives an invited lecture on Sequent Calculi for Some Non-classical Logics.
- 21-25.6
Claude Kirchner (Loria & INRIA, Nancy) lectures on Deduction Modulo.
- 21-25.6
John Slaney (NICTA, Canberra and Australian National University) lectures on Automated Reasoning for Substructural Logics.
- 16-18,21-27.6
Michel Parigot (CNRS - Université Paris 7) lectures on Proofs as Programs.
- 14-25.6
François Lamarche (Loria & INRIA, Nancy) lectures on Logic Considered as a Branch of Geometry.
- 14-18.6
Andrei Voronkov (Manchester) lectures on Automated Theorem Proving for Classical Logics.
- 14-16.6
Luke Ong (Oxford) lectures on Game Semantics and Its Applications.
- 14-16.6
Simona Ronchi della Rocca (Torino) gives an invited lecture on A Logic for Intersection Types.
- 14.6
Wolfgang Bibel (TU Darmstadt and Un. British Columbia) gives an invited lecture on Transition Logic.
In addition:
- 14-17.6
Franz Baader (TU Dresden) lectures on Term Rewriting Systems.
- 14-17.6
Alessio lectures on Deep Inference and the Calculus of Structures.
3.6
Alessio visits the PPS group in Paris and gives a talk about Deep Inference and Self-dual Non-commutativity.
13.5
Lutz visits the SIGNES group in Bordeaux and gives a talk about The Calculus of Structures.
31.3-3.4
Alessio participates in the Workshop on Constructive Classical Logic (Roma) and talks about The Need for Deep Inference in Proof Theory.
22-23.3
Lutz 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.3
Lutz participates in the 9th Estonian Winter School in Computer Science (Palmse) and talks about The Calculus of Structures.
1-5.3
Prakash Panangaden (McGill and Oxford University) visits us and talks about Concurrent Common Knowledge : Agreement and Causal Consistency in Distributed Systems.
12.2
Lutz visits the PPS group in Paris and gives a talk about The Calculus of Structures.
26-27.1
Lutz 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
We are or have been financed by:
Exclusive grant:
10.8.2005Alessio Guglielmi
email