[pt] O objetivo desta dissertação é construir um tableaux linear intuicionista
a partir de um cálculo de sequentes relevante clássico. Os passos principais
dessa construção são: i) tradução das regras do cálculo dos sequentes relevante
clássico para regras de tableaux (capítulo 3), usando a estratégia apresentada
por D Agostino et al. em Tableau Methods for Substructural Logic. ii) construção de um tableaux linear clássico através da linearização do tableaux
clássico relevante (capítulo 4). iii) apresentar um tableau intuicionista ao estilo
Fitting, em que são adicionados rótulos T s e F s às fórmulas (capítulo 5). / [en] The main goal of this master tesis is intuitionistic linear tableaux from
a relevant sequent calculus. The central steps are: i) Apply D Agostino et
al. strategy to translate classical relevant sequent calculus rules to tableaux
rules for classical relevant logic (Chapter 3). ii) Use Meyer et al. strategy
to linearize the classical relevant tableaux (Chapter 4). iii) Build a new
intuicionistic linear tableaux with Fitting labels.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:58715 |
| Date | 25 April 2022 |
| Creators | HUGO HOFFMANN BORGES |
| Contributors | LUIZ CARLOS PINHEIRO DIAS PEREIRA |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0023 seconds