HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

From Deep Inference to Proof Nets

Lutz Straßburger 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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''.
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download

Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Monday, February 12, 2007 - 3:49:14 PM
Last modification on : Thursday, January 20, 2022 - 5:30:48 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 9:07:04 PM


Files produced by the author(s)


  • HAL Id : inria-00130501, version 1



Lutz Straßburger. From Deep Inference to Proof Nets. Structures and Deduction 2005 (ICALP Workshop), Jul 2005, Lisbon, Portugal. ⟨inria-00130501⟩



Record views


Files downloads