CONSTRUINDO TABLEAUX PARA LÓGICA LINEAR INTUICIONISTA

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.