Made available in DSpace on 2014-06-12T16:01:12Z (GMT). No. of bitstreams: 2 arquivo7176_1.pdf: 981863 bytes, checksum: b65d9631609e56e387c6959338c69466 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2005 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / 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

Made available in DSpace on 2014-06-12T16:01:20Z (GMT). No. of bitstreams: 2 arquivo7782_1.pdf: 981863 bytes, checksum: b65d9631609e56e387c6959338c69466 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2005 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / 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

Made available in DSpace on 2014-06-12T15:53:19Z (GMT). No. of bitstreams: 2 arquivo1909_1.pdf: 1094258 bytes, checksum: 0313bee566cae55fbe650f2274bb2925 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / A apresentação dos N-Grafos foi feita por De Oliveira no ano 2001. Este é um sistema de provas que possui regras lógicas representadas graficamente por meio de digrafos. Estes grafos de provas se baseiam na dedução natural e no cálculo de sequentes de Gentzen, combinando idéias de quatro abordagens geométricas consolidadas na literatura de teoria da prova: tabelas de desenvolvimento (Kneale, 1957), redes-de-prova (Girard, 1987), logical flow graphs (Buss, 1991), e principalmente provas-como-grafos (Statman, 1974). Nesta dissertação é dado prosseguimento ao estudo dos N-grafos que foram propostos para a lógica proposicional clássica, o qual não possui uma versão para a lógica proposicional intuicionista. Realizamos uma revisão dos cálculos para a lógica intuicionista, destacando entre elas o trabalho apresentado por Gentzen na década de 1930, assim como as versões para múltiplas conclusões posteriores a este, como por exemplo o sistema LJ' (Maehara, 1954), os sistemas propostos por Kleene (Kleene, 1964) e o sistema FIL (De Paiva e Pereira, 2005). Assim a intenção desta dissertação é fazer um estudo sobre as dificuldades e possíveis soluções para a construção de um sistema de provas no estilo N-Grafos para a lógica intuicionista. Apresentando assim uma proposta de solução dos N-Grafos para a lógica intuicionista proposicional

[pt] A teoria da prova tradicional da lógica proposicional trata provas cujos tamanhos podem ser demasiado grandes. Estudos teóricos de prova descobriram diferenças exponenciais entre provas normais ou livres de corte e suas respectivas provas não-normais. Assim, o uso de grafos-de-prova, ao invés de árvores ou listas, para representar provas está se tornando mais popular entre teóricos da prova. Os grafos-de-prova servem como uma forma de proporcionar uma melhor simetria para a semântica de provas e uma maneira de estudar a complexidade das provas proposicionais. O objetivo deste trabalho é reduzir o peso/tamanho de deduções. Apresentamos formalismos de grafos de prova que visam capturar a estrutura lógica de uma dedução e uma forma de facilitar a visualização das propriedades. A vantagem destes formalismos é que as fórmulas e sub-deduções em dedução natural, preservadas na estrutura de grafo, podem ser compartilhadas eliminando sub-deduções desnecessárias resultando na prova reduzida. Neste trabalho, damos uma definição precisa de grafos de prova para a lógica puramente implicacional, logo estendemos esse resultado para a lógica proposicional completa e mostramos como reduzir (eliminando fórmulas máximas) essas representações de tal forma que um teorema de normalização pode ser provado através da contagem do número de fórmulas máximas na derivação original. A normalização forte será uma consequência direta desta normalização, uma vez que qualquer redução diminui as medidas correspondentes da complexidade da derivação. Continuando com o nosso objetivo de estudar a complexidade das provas, a abordagem atual também fornece representações de grafo para lógica de primeira ordem, a inferência profunda e lógica bi-intuitionista. / [en] Traditional proof theory of Propositional Logic deals with proofs which size can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. Thus, the use of proof-graphs, instead of trees or lists, for representing proofs is getting popular among proof-theoreticians. Proof-graphs serve as a way to provide a better symmetry to the semantics of proofs and a way to study complexity of propositional proofs and to provide more efficient theorem provers, concerning size of propositional proofs. The aim of this work is to reduce the weight/size of deductions. We present formalisms of proof-graphs that are intended to capture the logical structure of a deduction and a way to facilitate the visualization. The advantage of these formalisms is that formulas and subdeductions in Natural Deduction, preserved in the graph structure, can be shared deleting unnecessary sub-deductions resulting in the reduced proof. In this work, we give a precise definition of proof-graphs for purely implicational logic, then we extend this result to full propositional logic and show how to reduce (eliminating maximal formulas) these representations such that a normalization theorem can be proved by counting the number of maximal formulas in the original derivation. The strong normalization will be a direct consequence of such normalization, since that any reduction decreases the corresponding measures of derivation complexity. Continuing with our aim of studying the complexity of proofs, the current approach also give graph representations for first order logic, deep inference and bi-intuitionistic logic.