Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/11273
Título: | Relating sequent calculi for bi-intuitionistic propositional logic |
Autor(es): | Pinto, Luís F. Uustalu, Tarmo |
Palavras-chave: | Bi-intuitionistic logic Sequent calculus Nested sequents Labelled sequents Cuts |
Data: | 2011 |
Editora: | Open Publishing Association |
Revista: | Electronic Proceedings in Theoretical Computer Science (EPTCS) |
Citação: | Pinto, L., Uustalu, T., "Relating sequent calculi for bi-intuitionistic propositional calculi", Proceedings of 3rd Workshop on Classical Logic and Computation, van Bakel, S., Berardi, S., Berger, U Eds., Electronic Proceedings in Theoretical Computer Science 47, 55-72, 2011 |
Resumo(s): | Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent calculi for bi-intuitionistic propositional logic: (1) a basic standard-style sequent calculus that restricts the premises of implication-right and exclusion-left inferences to be single-conclusion resp. single-assumption and is incomplete without the cut rule, (2) the calculus with nested sequents by Gore et al., where a complete class of cuts is encapsulated into special ``unnest'' rules and (3) a cut-free labelled sequent calculus derived from the Kripke semantics of the logic. We show that these calculi can be translated into each other and discuss the ineliminable cuts of the standard-style sequent calculus. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/11273 |
DOI: | 10.4204/EPTCS.47.7 |
ISSN: | 2075-2180 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
clac10.pdf | Documento principal | 242,82 kB | Adobe PDF | Ver/Abrir |