Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.ufpe.br/handle/123456789/2786
Title: Normalização para os N-Grafos
Authors: Vaz Alves, Gleifer
Keywords: Grafos-de-prova; Teoria da Prova; Normalização
Issue Date: 2005
Publisher: Universidade Federal de Pernambuco
Citation: Vaz Alves, Gleifer; José Guerra Barreto de Queiroz, Ruy. Normalização para os N-Grafos. 2005. Dissertação (Mestrado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2005.
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
URI: https://repositorio.ufpe.br/handle/123456789/2786
Appears in Collections:Dissertações de Mestrado - Ciência da Computação

Files in This Item:
File Description SizeFormat 
arquivo7176_1.pdf958.85 kBAdobe PDFView/Open


This item is protected by original copyright



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.