Normalização para o 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á diversos trabalhos voltados ao teorema da eliminação-do-corte para o cálculo de sequentes clássico, bem como, investigações direcionadas à normalização para a dedução natural (DN) clássica. Por outro lado, são encontrados poucos trabalhos que buscam definir 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 [Ung92] e Cellucci [Cel92]. Todavia, nenhuma investigação apresenta um tratamento direcionado às questões inerentes à 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 DN, 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 dígrafos. Para a definição da normalização dos NGrafos, foram construídos cinco conjuntos de reduções: lógicas, estruturais, com ciclos, sequência com repetição de ciclos entrelaçados e permutação do enfraquecimento. Essas reduções foram baseadas nos trabalhos de Prawitz, Ungar e Cellucci, bem como, inspiradas pela própria estrutura de múltipla conclusão dos N-Grafos. Ademais, foram definidos o teorema e a prova da normalização, sendo que a prova foi construída de forma direta, diferentemente da prova indireta dada por 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