Return to search

[en] BUILDING TABLEAUX FOR INTUITIONISTIC LINEAR LOGIC / [pt] CONSTRUINDO TABLEAUX PARA LÓGICA LINEAR INTUICIONISTA

[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.

Identiferoai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:58715
Date25 April 2022
CreatorsHUGO HOFFMANN BORGES
ContributorsLUIZ CARLOS PINHEIRO DIAS PEREIRA
PublisherMAXWELL
Source SetsPUC Rio
LanguagePortuguese
Detected LanguagePortuguese
TypeTEXTO

Page generated in 0.0019 seconds