Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.ufpe.br/handle/123456789/2817
Title: Normalização para o N-grafos
Authors: Vaz Alves, Gleifer
Keywords: Teoria da prova; Normalização; Grafos-de-prova
Issue Date: 2005
Publisher: Universidade Federal de Pernambuco
Citation: 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.
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
URI: https://repositorio.ufpe.br/handle/123456789/2817
Appears in Collections:Dissertações de Mestrado - Ciência da Computação

Files in This Item:
File Description SizeFormat 
arquivo7782_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.