12/02/2004
Lutz Strassburger (LORIA)
The Calculus of Structure

The calculus of structures is a proof theoretical formalism, like natural deduction and the sequent calculus, for specifying logical systems and studying their properties. In this talk I will present its basic principles and its main features. For example, due to a new up-down symmetry, the identity axiom and the cut rule become syntactically dual. This allows to reduce the cut to an atomic version without going through a cut elimination argument. Furthermore, in the calculus of structures one can present new types of inference rules that allow to design logical systems that are completely local. More precisely, the contraction rule can be reduced to an atomic version (in the same way as it is usually done for the identity), and the promotion rule of linear logic can be presented in a local form. I will also present decomposition theorems which provide new types of normal forms for proofs and which are independent from cut elimination.