Normalização para os N-Grafos

Abstract

Os principais métodos da teoria da prova geral são: eliminação-do-corte e normalização. Na teoria da prova há muitos trabalhos voltados ao teorema da eliminação-do-corte para o cálculo de seqüentes clássico. Por outro lado, encontram-se relativamente poucas investigações direcionadas à normalização para a dedução natural clássica. Essa distinção é acentuada quando se tem a normalização para a lógica clássica através de uma estrutura de prova com mais de uma conclusão. Mencionem-se dois autores que apresentam normalização para uma estrutura com mais de uma conclusão, e.g. Ungar e Cellucci. Todavia, nenhuma investigação apresenta um tratamento direcionado às questões inerentes da definição de um procedimento de normalização dentro de uma estrutura de prova com mais de uma conclusão, onde as derivações sejam, de fato, representadas como grafos-de-prova. Portanto, o objetivo central deste trabalho é a definição do procedimento de normalização para os N-Grafos. Os N-Grafos foram definidos por de Oliveira e compõem um sistema de provas simétrico para a dedução natural, onde as regras lógicas e estruturais são apresentadas em uma estrutura de prova com múltipla conclusão e as derivações são representadas como digrafos. Para a definição da normalização dos N-Grafos, foram construídos cinco conjuntos de reduções: lógicas, estruturais, com ciclos, com seqüências de repetição de links e com permutação do enfraquecimento. Essas reduções foram baseadas nos trabalhos de Prawitz, Ungar e Cellucci, bem como, inspiradas pela própria estrutura de grafos-de-prova dos N-Grafos. Ademais, foram definidos o teorema e a prova da normalização, sendo que a prova foi construída de forma direta, em contrapartida à prova indireta de Ungar. Posteriormente, foram estabelecidas as propriedades da terminação e da confluência (fraca) para a normalização dos N-Grafos. Através da construção da normalização para os N-Grafos é possível destacar algumas propostas de trabalhos futuros como, por exemplo, a relação entre provas formais, e processos concorrentes e a investigação da correspondência entre a normalização e a identidade de provas