Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/3832
Título: | Permutability of proofs in intuitionistic sequent calculi |
Autor(es): | Pinto, Luís F. Dyckhoff, Roy |
Palavras-chave: | Intuitionistic logic Proof theory Natural deduction Sequent calculus |
Data: | 1999 |
Editora: | Elsevier 1 |
Revista: | Theoretical Computer Science |
Citação: | "Theoretical Computer Science". ISSN 0304-3975. 212:1/2 (1999) 141-155. |
Resumo(s): | 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. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/3832 |
DOI: | 10.1016/S0304-3975(98)00138-8 |
ISSN: | 0304-3975 |
Versão da editora: | The original publication is available at www.sciencedirect.com |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
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 |