# From Deep Inference to Proof Nets

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''.
Document type :
Conference papers
Domain :

Cited literature [25 references]

https://hal.inria.fr/inria-00130501
Contributor : Lutz Straßburger <>
Submitted on : Monday, February 12, 2007 - 3:49:14 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 9:07:04 PM

### File

deepnet.pdf
Files produced by the author(s)

### Identifiers

• HAL Id : inria-00130501, version 1

### Citation

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

Record views