1 |
[en] BUILDING TABLEAUX FOR INTUITIONISTIC LINEAR LOGIC / [pt] CONSTRUINDO TABLEAUX PARA LÓGICA LINEAR INTUICIONISTAHUGO HOFFMANN BORGES 25 April 2022 (has links)
[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.
|
Page generated in 0.5423 seconds