Proof nets and deep inference for linear logic

Lutz Straßburger, INRIA Futurs

LIX, Ecole Polytechnique, Palaiseau

Superficially, proof nets and deep inference seem to be to opposite approaches towards the problem of the identity of proofs (When are two proofs the same?): Proof nets are graph-like presentations of proofs that quotient away trivial rule permutations in the sequent calculus, and by this make more proof identification than the sequent calculus. On the other hand, in a deep inference system rules have a much finer granularity which allows even more permutations than the sequent calculus, and therfore there are less proof identification than the sequent calculus.

However, the finer granularity of inference rules allows a finer analysis of the inner structure of proofs which then can lead to new notions of proof nets which are independent from the sequent calculus. This mean that we now can avoid constructs like boxes in proof nets which are there because the sequent calculus makes use of some global information. This is particularly visible in multiplicative exponential linear logic (MELL), where the promotion rule is global in the sequent calculus and local in the deep inference system.

The problem for this internship is to exploit this locality and design proof nets without boxes for MELL.

Basic knowledge in logic and proof theory. Knowledge in proof nets and deep inference is not needed but would be of advantage.

The following bibliography is indicative of the kind of papers that will be part of this research effort.

1. Lutz Straßburger. A local system for linear logic. LPAR 2002, LNAI 2514, pp. 388-402, 2002.
2. Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the Calculus of Structures. CSL 2001, LNCS 2142, pp. 54-68, 2001.
3. Lutz Straßburger. Linear Logic and Noncommutativity in the Calculus of Structures. Phd Thesis, TU Dresden, 2003.
4. François Lamarche and Lutz Straßburger. From Proof Nets to the Free *-Autonomous Category. Logical Methods in Computer Science, Vol 2 (4:3), pp. 1-44, 2006.
5. Dominic Hughes and Rob van Glabbeek. Proof Nets for unit-free Multiplicative-Additive Linear Logic. LICS 2003.

Lutz Straßburger's list of problems
Parsifal's web page
Alessio Guglielmi's web page on deep inference