Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/3868
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | - |
dc.date.accessioned | 2006-01-11T15:46:43Z | - |
dc.date.available | 2006-01-11T15:46:43Z | - |
dc.date.issued | 2000 | - |
dc.identifier.citation | MONTANARI, Ugo ; ROLIM, José D. P. ; WELZL, Emo, ed. – “Automata, languages and programming : 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000 : proceedings”. Berlin [etc.] : Springer Verlag, cop. 2000. ISBN 3-540-67715-1. p. 600-611. | eng |
dc.identifier.uri | https://hdl.handle.net/1822/3868 | - |
dc.description.abstract | Cut-free proofs in Herbelin's sequent calculus are in 1-1 correspondence with normal natural deduction proofs. For this reason Herbelin's sequent calculus has been considered a privileged middle-point between L-systems and natural deduction. However, this bijection does not extend to proofs containing cuts and Herbelin observed that his cut-elimination procedure is not isomorphic to $\beta$-reduction. In this paper we equip Herbelin's system with rewrite rules which, at the same time: (1) complete in a sense the cut elimination procedure firstly proposed by Herbelin; and (2) perform the intuitionistic "fragment'' of the tq-protocol - a cut-elimination procedure for classical logic defined by Danos, Joinet and Schellinx. Moreover we identify the subcalculus of our system which is isomorphic to natural deduction, the isomorphism being with respect not only to proofs but also to normalisation. Our results show, for the implicational fragment of intuitionistic logic, how to embed natural deduction in the much wider world of sequent calculus and what a particular cut-elimination procedure normalisation is. | eng |
dc.description.sponsorship | Fundação para a Ciência e a Tecnologia (FCT). | eng |
dc.language.iso | eng | eng |
dc.publisher | Springer Verlag | eng |
dc.rights | openAccess | eng |
dc.subject | Cut-elimination | eng |
dc.subject | Normalisation | eng |
dc.subject | Herbelin's sequent calculus | eng |
dc.title | Revisiting the correspondence between cut-elimination and normalisation | eng |
dc.type | conferencePaper | eng |
dc.peerreviewed | yes | eng |
sdum.pagination | 600-611 | eng |
sdum.publicationstatus | published | eng |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
revisiting.pdf | 204,41 kB | Adobe PDF | Ver/Abrir |