masterThesis
Normalização para o N-grafos
Registro en:
Vaz Alves, Gleifer; José Guerra Barreto de Queiroz, Ruy. Normalização para o N-grafos. 2005. Dissertação (Mestrado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2005.
Autor
Vaz Alves, Gleifer
Institución
Resumen
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 Coordenação de Aperfeiçoamento de Pessoal de Nível Superior