Normal forms for classical logic proofs in deep inference

Lutz Straßburger, INRIA Futurs

LIX, Ecole Polytechnique, Palaiseau

Deep inference is a recently developped paradigm for presenting deductive systems. It has successfully be applied for varios logics, like classical logic, linaer logic, intuitionistic logic and modal logics. The novelty is that inference rules are allowed to be applied like rewrite rules deep inside formulas. This is not possible with shallow inference systems like sequent calculus or natural deduction.

The new freedom in the design of inference rules has a drawback: The usual techniques for obtaining important properties, like cut elimination, break down. For this reason new techniques, like splitting and decomposition have been developped.

The task for this internship is to apply these new methods to the deep inference system SKS for classical logic, and relate the cut elimination proof obtained in this way to cut elimination in the sequent calculus and in proof nets.

Basic knowledge in logic and proof theory. Knowledge in proof normalization 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. Kai Brünnler. Deep Inference and Symmetry for Classical Proofs. Phd Thesis, TU Dresden, 2003.
2. Kai Brünnler. Cut Elimination inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82:51-71, 2006.
3. Lutz Straßburger. Linear Logic and Noncommutativity in the Calculus of Structures. Phd Thesis, TU Dresden, 2003.
4. Lutz Straßburger. A Characterisation of Medial as Rewriting Rule. Term Rewriting and Applications, RTA'07, LNCS 4533, pp. 344-358, 2007.
5. François Lamarche and Lutz Straßburger. Naming Proofs in Classical Propositional Logic. TLCA'05, LNCS 3461, pp. 246-261, 2005.

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