Em direção aos N-Grafos intuicionistas

Abstract

A apresentação dos N-Grafos foi feita por De Oliveira no ano 2001. Este é um sistema de provas que possui regras lógicas representadas graficamente por meio de digrafos. Estes grafos de provas se baseiam na dedução natural e no cálculo de sequentes de Gentzen, combinando idéias de quatro abordagens geométricas consolidadas na literatura de teoria da prova: tabelas de desenvolvimento (Kneale, 1957), redes-de-prova (Girard, 1987), logical flow graphs (Buss, 1991), e principalmente provas-como-grafos (Statman, 1974).

Nesta dissertação é dado prosseguimento ao estudo dos N-grafos que foram propostos para a lógica proposicional clássica, o qual não possui uma versão para a lógica proposicional intuicionista. Realizamos uma revisão dos cálculos para a lógica intuicionista, destacando entre elas o trabalho apresentado por Gentzen na década de 1930, assim como as versões para múltiplas conclusões posteriores a este, como por exemplo o sistema LJ' (Maehara, 1954), os sistemas propostos por Kleene (Kleene, 1964) e o sistema FIL (De Paiva e Pereira, 2005). Assim a intenção desta dissertação é fazer um estudo sobre as dificuldades e possíveis soluções para a construção de um sistema de provas no estilo N-Grafos para a lógica intuicionista. Apresentando assim uma proposta de solução dos N-Grafos para a lógica intuicionista proposicional