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

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

Collections

Citation

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

Share

Metrics

Record views

387

Files downloads

145