Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.ufpe.br/handle/123456789/18618
Title: A combinatorial study of soundness and normalization in n-graphs
Authors: ANDRADE, Laís Sousa de
Keywords: N-Grafos;Sub-N-Grafos;Dedução Natural;Normalização;Duplicação;Grafos direcionados;DFS;Proof-nets;N-Graphs;Sub-N-Graphs;Natural deduction;Normalization;Duplication;Directed graphs;DFS;Proof-nets
Issue Date: 29-Jul-2015
Publisher: Universidade Federal de Pernambuco
Abstract: N-Grafoséumadeduçãonaturaldemúltiplasconclusõesondeprovassãorepresentadascomo grafos direcionados, motivadopela idéia de provas comoobjetos geométricos ecom o objetivo de estudar a geometria de sistemas de Dedução Natural. Seguindo esta linha de pesquisa, este trabalho revisita o sistema sob uma perpectiva puramente combinatorial, determinando condições geométricas nos grafos de prova para explicar seu critério de corretude e crescimento da provadurante anormalização. Aplicandodesenvolvimentosrecentes noscampos degrafos de prova, proof-nets e dos próprios N-Grafos, propomos um algoritmo linear para verificação de provas para o sistema completo, um resultado que pode ser comparado com soluções para proof-nets desenvolvidas por Murawski (2000) e Guerrini (2011), e um procedimento de normalização baseado na noção de sub-N-Grafos, introduzidas por Carvalho, em 2014. Apresentamos primeiramente um novo critério de corretude para meta-arestas, juntamente com a extensão para todo o sistema da prova da sequentização desenvolvida por Carvalho. Para este critério definimos um algoritmo para verificação de provas que utiliza uma busca parecida com a DFS (Busca em Profundidade) para encontrar ciclosinválidos em umgrafo de prova. Como o critério de corretudepara grafos de provas éanálogo ao procedimento paraproof-nets, o algoritmo pode também ser estendido para validar provas em Lógica Linear multiplicativa sem units (MLL−) com complexidade de tempo linear. A nova normalização proposta aqui combina uma versão modificada das reduções beta e permutativas originais de Alves com uma adaptação da operação de duplicação proposta por Carbone para ser aplicada a sub-N-Grafos. O procedimento é mais simples do que o original e funciona como uma extensão da normalização definida por Prawitz e do estudocombinatorial desenvolvidopor Carbone, i.e. provas em formanormal desfrutamdas propriedadesdaseparaçãoesubformulaepossuemumaestruturaquepoderepresentarcomo padrões existentes em provas na forma normal poderiam ser recuperados a partir do grafo da prova original com cortes.
URI: https://repositorio.ufpe.br/handle/123456789/18618
Appears in Collections:Dissertações de Mestrado - Ciência da Computação

Files in This Item:
File Description SizeFormat 
dissertacao-mestrado.pdf2.71 MBAdobe PDFView/Open


This item is protected by original copyright



This item is licensed under a Creative Commons License Creative Commons