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.