Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/11310
Título: | Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents |
Autor(es): | Pinto, Luís F. Uustalu, Tarmo |
Palavras-chave: | Bi-intuitionistic propositional logic Labelled sequents Proof search Counter-models |
Data: | 2009 |
Editora: | Springer |
Revista: | Lecture Notes in Computer Science |
Citação: | GIESE, M. ; WAALER, A., ed. lit. – “International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009), 18, Oslo, Norway, 2009”. Berlin : Springer, 2009. p. 295-309. |
Resumo(s): | Bi-intuitionistic logic is a conservative extension of intuitionistic logic with a connective dual to implication, called exclusion. We present a sound and complete cut-free labelled sequent calculus for bi-intuitionistic propositional logic, BiInt, following S. Negri's general method for devising sequent calculi for normal modal logics. Although it arises as a natural formalization of the Kripke semantics, it is does not directly support proof search. To describe a proof search procedure, we develop a more algorithmic version that also allows for counter-model extraction from a failed proof attempt. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/11310 |
ISBN: | 9783642027154 |
DOI: | 10.1007/978-3-642-02716-1_22 |
ISSN: | 0302-9743 |
Versão da editora: | http://www.springerlink.com/content/fqh703t1p45718w2/ |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
tableaux09-LPintoTUustalu.pdf | Documento principal | 255,65 kB | Adobe PDF | Ver/Abrir |