This page is no longer updated, the new one is here.

**Contents of this page**

- Frequently Asked Questions
- Papers, Lectures and Theses
- Notes, Conjectures, Problems, Etc.
- Proof Theory Mailing List
- Politics
- Acknowledgements

**Related links**

- Group at TU Dresden (people, events, funding and resources)
- ProofTheory.ORG
- Summer School and Workshop on Proof Theory, Computation and Complexity (Dresden 2003)
- Workshop on Proof Theory and Computation (Dresden 2002)

The calculus of structures is a new proof theoretical formalism, introduced by myself in 1999 and mostly developed by members of our group in Dresden since 2000. It exploits a new *top-down symmetry* of derivations made possible by *deep inference*. We can present deductive systems in the calculus of structures and analyse their properties, as we do in the sequent calculus, natural deduction and proof nets. Typical properties of interest are *normalisation* and *cut elimination*.

The main purpose of our new formalism is to allow a *richer combinatorial analysis* of proofs than the other formalisms do. We adopted two main ideas: inferences are symmetric between premises and conclusions, and they are deeply applicable inside expressions (what we call `deep inference´). As a consequence, it is convenient to deduce over *structures*, which are expressions intermediate between formulae and sequents.

The proof theory of the calculus of structures *differs significantly* from what has been studied so far. Deep inference severely challenges the usual cut elimination methods, but this is mitigated by atomic cuts being much simpler objects than generic cuts.

We developed several new techniques to overcome the difficulties. Some of these methods allowed us to unveil totally new combinatorial properties of logical systems, like the *decomposition* theorems. In general, the new properties have a strong flavour of *modularity*. This, together with atomicity and locality, is important for applications in computer science, which we recently started to pursue.

So far, we presented *classical logic* and *linear logic* (in all its fragments) in the calculus of structures, in such a way that atomicity, locality and the various instances of modularity have been expressed. We are currently studying several *modal logics*, with equally pleasing results. In collaboration with external researchers, we are investigating *intuitionistic logics* and *non-commutative linear logics*, like *Yetter's cyclic linear logic* and *Abrusci-Ruet non-commutative logic*. The deductive systems in the calculus of structures are *simple* and *elegant*, and they pose no special challenge to those interested in using them.

This whole theory was born when trying to capture a hybrid commutative/non-commutative logic, which I call *system V*. Only the multiplicative fragment of V has been developed so far—again with all the good properties mentioned above. Despite its simplicity (only three inference rules), this system *cannot be presented* in the sequent calculus. This is rather surprising and allows us to claim our ability *to extend* the range of application of the sequent calculus, the most versatile formalism so far.

- General
- Isn't the calculus of structures just a trivial notational variation of the sequent calculus?
- Proof theory is famous for producing horrible proofs of its own theorems; are you doing any better?
- What is deep inference?
- What is a structure?
- Isn't the word `structure´ reserved for semantics?
- Can you do in the calculus of structures anything you can do in the sequent calculus?
- Does the calculus of structures automatically introduce a mix rule in any system?

- Cut Elimination
- You make a big deal of having the cut rule in atomic form; but can't you do the same in the sequent calculus?
- What's the point in proving again cut elimination for classical and linear logic?
- By the way, what's the point in dedicating an entire paper to such an easy statement as cut elimination for propositional classical logic in the calculus of structures?

- Term Rewriting
- Philosophy

The following material is broad in scope:

Mismatch

Alessio Guglielmi

PdfAugust 24, 2003

Brief note for the specialist, recently posted to the Foundations of Mathematics and Proof Theory lists. It introduces the calculus of structures by addressing the problem of a mismatch between object and meta level.

Deep Inference and Symmetry in Classical Proofs

Kai Brünnler

PdfJuly 15, 2003

PhD thesis, to be defended on 22.9.2003BibTeX entry

Linear Logic and Noncommutativity in the Calculus of Structures

Lutz Straßburger

PdfPdf in booklet formatJuly 25, 2003

PhD thesis, successfully defended on 24.7.2003BibTeX entry

Proof Theory With Deep Inference—Slide Presentation

Alessio Guglielmi

PdfJune 28, 2003

Course at Summer School and Workshop on Proof Theory, Computation and Complexity

Deep Inference—Slide Presentation

Alessio Guglielmi

PdfMarch 13, 2003

Talk

The Calculus of Structures—Project Report

Alessio Guglielmi

PdfSeptember 10, 2003

Always outdated but sometimes updated; this report assumes you are familiar with structural proof theory; it gives an overview of the activity in our group

Papers are divided into six sections according to their subject: classical logic, modal logics, linear Logic, commutative/non-commutative linear logic, cyclic linear logic and language design. Each paper presents an introduction to the calculus of structures. There is no general introduction to the calculus yet, because we started developing it from concrete examples, i.e., deductive systems. Inside each section, papers are listed in decreasing order of accessibility.

It is important to bear in mind a terminological distinction we make: a *(formal) system* is a set of inference rule schemes, a *calculus* is the formalism in which the formal systems are designed. For example, system LK is a formal system for classical logic in the sequent calculus.

So far, for classical logic in the calculus of structures it has been achieved:

- the cut rule trivially reduces to atomic form;
- one can show cut elimination for the propositional fragment by the simplest argument to date;
- the propositional fragment is fully local, including contraction;
- first order classical logic can be entirely made finitary;
- cut elimination and decomposition theorems are proved.

Atomic Cut Elimination for Classical Logic

Kai Brünnler

Pdf© Springer-VerlagApril 10, 2003

CSL 2003, LNCS 2803, pp. 86–97 (was Technical Report WV-02-11)BibTeX entry

Locality for Classical Logic

Kai Brünnler

PdfJanuary 22, 2003

Technical Report WV-03-04, submitted to Archive for Mathematical LogicBibTeX entry

A Finitary System for First Order Logic

Kai Brünnler and Alessio Guglielmi

PdfApril 30, 2003

Technical Report WV-03-09, accepted at First Order Logic 75BibTeX entry

A Local System for Classical Logic

Kai Brünnler and Alwen Fernanto Tiu

Pdf© Springer-VerlagOctober 2, 2001It was Technical Report WV-01-02, now replaced by Locality for Classical Logic

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

Two Restrictions on Contraction

Kai Brünnler

PdfAugust 3, 2003

Technical Report WV-02-04, to appear in Logic Journal of the Interest Group in Pure and Applied LogicsBibTeX entry

Consistency Without Cut Elimination

Kai Brünnler and Alessio Guglielmi

PdfSeptember 10, 2003It is contained in A Finitary System for First Order Logic

Technical Report WV-02-16BibTeX entry

Classical logic in the calculus of structures (abstracts)

So far, for linear logic in the calculus of structures it has been achieved:

- the cut rule trivially reduces to atomic form;
- the propositional fragment is fully local, including promotion and contraction;
- cut elimination and decomposition theorems are proved.

A Local System for Linear Logic

Lutz Straßburger

- Conference version pdf© Springer-VerlagAugust 9, 2002

LPAR 2002, LNAI 2514, pp. 388–402BibTeX entry- Work-in-progress technical report pdfJune 10, 2002

Technical Report WV-02-01BibTeX entry

MELL in the Calculus of Structures

Lutz Straßburger

PdfOctober 29, 2001This paper is contained in succinct form in Non-commutativity and MELL in the Calculus of Structures

Technical Report WV-01-03, to appear in Theoretical Computer ScienceBibTeX entry

Linear logic in the calculus of structures (abstracts)

Several normal propositional modal logics are systematically presented in the calculus of structures and cut elimination is proved.

A Systematic Proof Theory for Several Modal Logics

Charles Stewart and Phiniki Stouppa

PdfApril 16, 2003

Technical Report WV-03-08BibTeX entry

Modal logics in the calculus of structures (abstract)

We conservatively extend mixed multiplicative and multiplicative exponential linear logic with a self-dual non-commutative operator. The systems so obtained cannot be presented in the sequent calculus, but they enjoy the usual properties of locality, decomposition and cut elimination available in the calculus of structures.

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–68 (was Technical Report WV-01-04)BibTeX entry

A System of Interaction and Structure

Alessio Guglielmi

PdfSeptember 27, 2002

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

Properties of a Logical System in the Calculus of Structures

Alwen Fernanto Tiu

PdfSeptember 12, 2001

MSc thesis, successfully defended on 1.8.2001, Technical Report WV-01-06BibTeX entry

A Non-commutative Extension of Multiplicative Exponential Linear Logic

Alessio Guglielmi and Lutz Straßburger

- Conference version pdf© Springer-VerlagAugust 9, 2002

LPAR 2002, LNCS 2514, pp. 231–246BibTeX entry- Journal version pdfJuly 4, 2003

Technical Report WV-02-03, submitted to APALBibTeX entry

The Undecidability of System NEL

Lutz Straßburger

- Conference version pdfAugust 20, 2003

accepted at WoLLIC 2003 under the titleSystem NEL Is Undecidable, to appear in ENTCSBibTeX entry- Journal version pdfFebruary 12, 2003

Technical Report WV-03-05BibTeX entry

A1-Unification

Alwen Fernanto Tiu

Gzipped PostscriptFebruary 19, 2002

Technical Report WV-01-08BibTeX entry

Combining A1- and AC1-Unification Sharing Unit

Alwen Fernanto Tiu

Gzipped PostscriptFebruary 19, 2002

Technical Report WV-01-09BibTeX entry

Commutative/non-commutative linear logic in the calculus of structures (abstracts)

Yetter's cyclic linear logic is presented in the calculus of structures and cut elimination is proved. Interestingly, cyclicity is naturally subsumed by deep inference.

Structures in Cyclic Linear Logic

Pietro Di Gianantonio

Gzipped PostscriptFebruary 12, 2003

Technical Report, Università di UdineBibTeX entry

Cyclic linear logic in the calculus of structures (abstract)

Thanks to a self-dual non-commutative extension of linear logic one gets the first purely logical account of sequentiality in proof search.

A Purely Logical Account of Sequentiality in Proof Search

Paola Bruscoli

Pdf© Springer-VerlagAugust 12, 2002

ICLP 2002, LNCS 2401, pp. 302–316 (was Technical Report WV-02-06)BibTeX entry

Language design in the calculus of structures (abstract)

Freedom from Bureaucracy

F.F.The dream of flying above the miseries of syntax can be realised provided all ties with totalitarian ideologies are cut.February 15, 1963Goodness, Perfection and Miracles

A.G.I introduce three properties closely related to cut elimination and interpolation theorems. October 18, 2002Recipe

A.G.A family of tautologies that hold in most logics can be used, following a simple recipe, to produce deductive systems where all rules are local, including cut.October 27, 2002Finitary Cut

A.G.We all know that the traditional cut rule is considered infinitary. But if we reduce the cut rule to atomic form, as we always can do in the calculus of structures, is atomic cut still infinitary? Not really.October 23, 2002This note is now subsumed by A Finitary System for First Order LogicOn Lafont's Counterexample

A.G.Lafont's counterexample shows why cut elimination in the sequent calculus of classical logic is not confluent. I show here that the counterexample doesn't work in the calculus of structures.November 1, 2002Normalisation Without Cut Elimination

A.G.I propose a possible notion of equivalence for proofs in classical logic, sort of a normal form for case analysis.February 25, 2003Butterflies

A.G.It's not known whether MELL is decidable. I conjecture here that system NEL, i.e., MELL plus non-commutativity, is undecidable. I propose an encoding of Post's Correspondence Problem (PCP) into NEL that has the merit of making non–commutativity (in NEL) correspond to sequential composition (in PCP), which is intuitive.November 1, 2002Subatomic Logic

A.G.One can unify classical and linear logic by using only two simple, linear, `hyper´ inference rules; they generate nice systems for all the fragments, where all rules are local. The various logics are determined by the algebra of their units, for example boolean algebra determines classical logic. We can prove cut elimination easily and once and for all in the two-rule system, and the procedure scales down to all the derived fragments.November 21, 2002Minimal Logic in the Calculus of Structures

K.B.In this note I present preliminary ideas about a system for minimal logic.February 12, 2003

I help running a mailing list devoted to proof theory, where the calculus of structures is sometimes discussed: click here to subscribe or here to unsubscribe.

Since a few years I'm criticizing the current practice of publishing papers at conferences, in theoretical computer science. I decided not to send papers to, or participate in conferences, in any way, including reviewing. Of course this is an extremist position (and perhaps an irrelevant one), but I feel that everybody in life should choose a little radical campaign to fight. In order not to endanger too much the career of my colleagues, I accepted to co-author some conference papers with them.

The reasons for my choice are the following. There are too many conferences and it is too easy to publish papers. Since conference publication has some weight in assessing CVs, it is highly encouraged, and thanks to it people are able to put together massive CVs to slam on the face of their adversaries. Given the inflation of papers, the attention devoted to reviewing them is forcefully limited. Moreover, conference papers are usually written under time pressure and format constraints, which do not facilitate the task of communicating.

Conferences, like mobile phones and cars, are locally good but globally bad. While it might be nice and fruitful to participate in a conference occasionally, a system where an entire community is forced to jump from plane to plane, sleeplessly trying to write and review tons of paper, is dangerous to the healthy development of theoretical computer science. Breakthrough ideas require constant effort and continuous attention, they do not come out of brownian motion.

The development of the calculus of structures took me several years, the first five of which spent in recycling paper. I started at University of Pennsylvania (1994), then went on at Università di Pisa (1994-97) and INRIA Lorraine (1997-98), and then at TU Dresden.

The following persons profoundly influenced the building of the calculus of structures:

- Jean-Yves Girard: I took from him the conviction that there are deep geometrical phenomena at the basis of proof theory, and I found inspiration in linear logic.
- Giorgio Levi and Dale Miller: Giorgio made me read and work on Dale's papers, where I could find excellent design of logical systems.
- Christian Retoré: he made me interested in the strange properties of self-duality and non-commutativity and their challenge to proof theory, and he also pointed me to N-free orders, which is where everything started finally to work and make sense.

At TU Dresden I found three crazy, extraordinary students: Kai Brünnler, Lutz Straßburger and Alwen Tiu. They risked their future careers to come working on this project at a time when nobody sane could bet on its success.

Last, but not least, I'd like to acknowledge the excellent education I've got at the Scuola Normale Superiore, at a time when I didn't know that proof theory existed, nor did I know the value of education.

10.9.2003Alessio Guglielmiemail