From Deep Inference to Proof Nets
Lutz Straßburger · 2005
Abstract. This paper shows how derivations in (a variation of) SKS can be translated into proof nets. Since an SKS derivation contains more information about a proof than the corresponding proof net, we observe a loss of information which can be understood as “eliminating bureaucracy”. Technically this is achieved by cut reduction on proof nets. As an intermediate step between the two extremes, SKS derivations and proof nets, we will see nets representing derivations in “Formalism A”. inria-00130501, version 1- 12 Feb 2007 1