Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/3832
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Pinto, Luís F. | - |
dc.contributor.author | Dyckhoff, Roy | - |
dc.date.accessioned | 2006-01-05T17:45:27Z | - |
dc.date.available | 2006-01-05T17:45:27Z | - |
dc.date.issued | 1999 | - |
dc.identifier.citation | "Theoretical Computer Science". ISSN 0304-3975. 212:1/2 (1999) 141-155. | eng |
dc.identifier.issn | 0304-3975 | eng |
dc.identifier.uri | https://hdl.handle.net/1822/3832 | - |
dc.description.abstract | We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's {\bf G3}) are inter-permutable (using a set of basic "permutation reduction rules'' derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. We refer to Schwichtenberg's proof elsewhere that a modification of this system is strongly normalising. | eng |
dc.description.sponsorship | Centro de Matemática da Universidade do Minho (CMAT). | por |
dc.description.sponsorship | União Europeia (UE) - Programa ESPRIT BRA 7232 GENTZEN. | por |
dc.language.iso | eng | eng |
dc.publisher | Elsevier 1 | eng |
dc.rights | openAccess | eng |
dc.subject | Intuitionistic logic | eng |
dc.subject | Proof theory | eng |
dc.subject | Natural deduction | eng |
dc.subject | Sequent calculus | eng |
dc.title | Permutability of proofs in intuitionistic sequent calculi | eng |
dc.type | article | por |
dc.peerreviewed | yes | eng |
dc.relation.publisherversion | The original publication is available at www.sciencedirect.com | eng |
sdum.number | 1/2 | eng |
sdum.pagination | 141-155 | eng |
sdum.publicationstatus | published | eng |
sdum.volume | 212 | eng |
oaire.citationStartPage | 141 | por |
oaire.citationEndPage | 155 | por |
oaire.citationIssue | 1-2 | por |
oaire.citationVolume | 212 | por |
dc.identifier.doi | 10.1016/S0304-3975(98)00138-8 | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Theoretical Computer Science | por |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
TCS.ps | 178,81 kB | Postscript | Ver/Abrir | |
TCS.pdf | 205,07 kB | Adobe PDF | Ver/Abrir |