From deduction graphs to proof nets: boxes and sharing in the graphical presentation of deductions

J.H. Geuvers, I. Loeb

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    3 Citaten (Scopus)

    Samenvatting

    Deduction graphs [3] provide a formalism for natural deduction, where the deductions have the structure of acyclic directed graphs with boxes. The boxes are used to restrict the scope of local assumptions. Proof nets for multiplicative exponential linear logic (MELL) are also graphs with boxes, but in MELL the boxes have the purpose of controlling the modal operator !. In this paper we study the apparent correspondences between deduction graphs and proof nets, both by looking at the structure of the proofs themselves and at the process of cut-elimination defined on them. We give two translations from deduction graphs for minimal proposition logic to proof nets: a direct one, and a mapping via so-called context nets. Context nets are closer to natural deduction than proof nets, as they have both premises (on top of the net) and conclusions (at the bottom). Although the two translations give basically the same results, the translation via context nets provides a more abstract view and has the advantage that it follows the same inductive construction as the deduction graphs. The translations behave nicely with respect to cut-elimination.
    Originele taal-2Engels
    TitelMathematical Foundations of Computer Science (Proceedings 31st International Symposium, MFCS 2006, Stará Lesná, Slovakia, August 28-September 1, 2006)
    RedacteurenR. Královic, P. Urzyczyn
    Plaats van productieBerlin
    UitgeverijSpringer
    Hoofdstuk4
    Pagina's39-57
    Aantal pagina's19
    ISBN van elektronische versie978-3-540-37793-1
    ISBN van geprinte versie978-3-540-37791-7
    DOI's
    StatusGepubliceerd - 2006

    Publicatie series

    NaamLecture Notes in Computer Science (LNCS)
    Volume4162
    ISSN van geprinte versie0302-9743

    Vingerafdruk

    Duik in de onderzoeksthema's van 'From deduction graphs to proof nets: boxes and sharing in the graphical presentation of deductions'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit