[en] BUILDING TABLEAUX FOR INTUITIONISTIC LINEAR LOGIC

[pt] CONSTRUINDO TABLEAUX PARA LÓGICA LINEAR INTUICIONISTA

[pt] HUGO HOFFMANN BORGES

[pt] TEORIA DA PROVA

[pt] TABLEAUX

[pt] LOGICA RELEVANTE

[pt] LOGICA LINEAR

[en] PROOF THEORY

[en] TABLEAU

[en] RELEVANT LOGIC

[en] LINEAR LOGIC

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

LUIZ CARLOS PINHEIRO DIAS PEREIRA

EDWARD HERMANN HAEUSLER

LUIZ CARLOS PINHEIRO DIAS PEREIRA

JEFFERSON DE BARROS SANTOS

JEAN BAPTISTE JOINET

2022-04-25

2022-03-11

[pt] TEXTO

application/pdf

PORTUGUÊS

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=58715@1

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=58715@2

https://doi.org/10.17771/PUCRio.acad.58715