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

[pt] Na antologia que M.E. Szabo realizara dos trabalhos de Gentzen e publicara em 1969 se transcrevem, em um apêndice, algumas passagens apresentadas por Bernays ao editor pertencentes a uma primeira prova de consistência para a Aritmética de Peano realizada por Gentzen que não tinha sido publicada até então. À diferença das outras provas de consistência realizadas por Gentzen e já conhecidas na década de trinta, esta prova não utiliza o procedimento de indução transfinita até e0. Ao contrário, baseia-se na definição de um processo de redução de seqüentes que se associa sistematicamente a todo seqüente derivável permitindo reconhecê-lo como verdadeiro. Nós reconstruímos essa prova realizando algumas variações e estudamos o modo pelo qual a técnica principal utilizada (a definição do processo de redução de seqüentes) pode ser vista em relação a resultados da lógica clássica de primeira ordem tais como provas de completude. A parte central da nossa dissertação é a realização de uma versão desta prova de consistência para um sistema formal para a Aritmética de Heyting. / [en] In the antology of Gentzens works made by M.E.Szabo and published in 1969, we find out in an appendix, some passages presented by Bernays to the editor. These texts belong to a first proof of Peanos Arithmetic consistency that Gentzen did not publish. In a different way from the other proofs of consistency made by Gentzen and already known in the thirties, this proof does not use the procedure of transfinite induction up to e0. On the contrary, it is based on the definition of a reduction process for sequents that is systematically associated to every derivable sequent allowing us to recognize it as a true sequent. We reconstructed this proof making some variations and we studied how the main technique used (the definition of the reduction process) could be seen in relation with other results of first order logic like proofs of completness. The main part of our dissertation is another version of this consistency proof for a formal system for Heyting Arithmetic.

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] O tamanho das provas formais possui algumas importantes implicações teóricas na área da complexidade computacional. O problema de determinar se uma fórmula é uma tautologia da Lógica Proposicional Intuicionista e do fragmento puramente implicacional da Lógica Minimal (M(contém)) é PSPACE- Completo. Qualquer lógica proposicional com um sistema de dedução natural que satisfaça o princípio da subfórmula possui o problema de determinar tautologias em PSPACE. Saber se qualquer tautologia em M(contém) admite provas de tamanho polinomialmente limitado está relacionado com saber se NP = PSPACE. Técnicas de compressão de provas reportadas na literatura utilizam duas abordagens principais para comprimir provas: gerar provas já compactadas; comprimir uma prova já gerada. Proposta por Gordeev e Haeusler (6), a Compressão Horizontal é uma técnica de compressão de provas em dedução natural da M(contém) que utiliza grafos direcionados para representar as provas. Dada a prova de uma tautologia qualquer da M(contém), que pode possuir tamanho exponencial em relação ao tamanho da conclusão, o objetivo da Compressão Horizontal é que a prova resultante da compressão possua tamanho polinomialmente limitado em relação ao tamanho da conclusão. Nosso trabalho apresenta a primeira implementação da Compressão Horizontal, juntamente com os primeiros resultados da aplicação da técnica sobre provas de tautologias da M(contém), além disso, compara as taxas de compressão obtidas com técnicas tradicionais de compressão de dados. / [en] The size of formal proofs has some important theoretical implications in computational complexity theory. The problem of determining if some formula of Intuitionistic Propositional Logic and the purely implicational fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any propositional logic with a natural deduction system that satisfies the sub- formula principle is PSPACE. To know if any tautology in M(contains) admits polynomially sized proof is related to whether NP = PSPACE. Proof compression techniques reported in literature use two main approaches to proof compressing: generating already compressed proofs; compressing an already generated proof. Proposed by Gordeev and Haeusler (6), the Horizontal Compression is a natural deduction proof compression technique that uses directed graphs to represent proofs. Given a tautology proof in M(contains), which may have an exponential size in relation to conclusion length, the goal of Horizontal Compression is that the compressed proof has a polynomially limited size in relation to conclusion length. Our work presents the first implementation of Horizontal Compression, together with the first results of the execution of the technique on proofs of M(contains) tautologies.

[pt] A primeira apresentação de um Cálculo de Seqüentes foi feita por Gerhard Gentzen na década de 1930. Neste tipo de sistema, a diferença entre as versões clássica e intuicionista radicardinalidade do sucedente. O sucedente múltiplo foi tradicionalmente considerado como o elemento que representava o aspecto clássico do sistema, enquanto os seqüentes intuicionistas podiam ter, no máximo, uma fórmula no sucedente. Nas décadas seguintes foram formulados diversos cálculos intuicionistas de sucedente múltiplo que atenuaram essa restrição forte na cardinalidade do sucedente. Na década de 1990, estudou-se a relação de conexão ou dependência entre as fórmulas visando assegurar o caráter intuicionista dos sistemas. Nós realizamos uma revisão dos sistemas de se seqüentes intuicionistas e algumas das suas aplicações. Apresentamos a versão do sistema FIL (feita para o caso proposicional por De Paiva e Pereira) para a lógica intuicionista de primeira ordem provando que o mesmo é correto, completo e satisfaz eliminação de corte. / [en] The first Sequent Calculus was presented by Gerhard Gentzen in the thirties. In this system, the difference between intuitionistic logic and classical logic is based on the cardinality of the succedent. Traditionally, the multiple succedent was considered the element that preserved the classical aspect of the system, while intuitionistic sequents have, at most, one formula in the succedent. In the following decades, several multiple succedent intuitionistic calculus were presented that diminish shed this st strong restriction in the cardinality of the su succedent. In the decade of 1990, this cardinality restriction was replaced by a dependency relation between the formula ocurrences in the antecedent and in the succedent of a sequent in order to ensure the intuitionistic character of the system. We make a revision of the intuitionistic systems and some of their applications. We present a version of the system FIL (accomplish shed for the propositional case by De Paiva and Pereira) for first-order logic proving that it is sound, complete and that it satisfies the cut-elimination theorem.

CAVALCANTE, Alexandre Silva. Sistemas esquemáticos de dedução natural: um estudo prova-teórico. 2010. 201 f. Tese (Doutorado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2010. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-12T19:23:49Z No. of bitstreams: 1 2010_tese_ascavalcante.pdf: 842091 bytes, checksum: 559c5a97b93d42e7b0bb2d0c9b1d1520 (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-25T11:32:56Z (GMT) No. of bitstreams: 1 2010_tese_ascavalcante.pdf: 842091 bytes, checksum: 559c5a97b93d42e7b0bb2d0c9b1d1520 (MD5) / Made available in DSpace on 2016-07-25T11:32:56Z (GMT). No. of bitstreams: 1 2010_tese_ascavalcante.pdf: 842091 bytes, checksum: 559c5a97b93d42e7b0bb2d0c9b1d1520 (MD5) Previous issue date: 2010 / The term Theory Test was introduced by Hilbert to identify the study of formal proofs. Research in this area can be classified into: a) Proof Theory of reductive or interpretational, whose goal is to demonstrate, among other things, the consistency of mathematics using only methods finitistas, b) Structural Proof Theory, where the structural characteristics of the formal proofs are investigated by means of deductive systems as Natural Deduction and Sequent Calculus. Prawitz through Theory Proof set a Theory of Meaning for constants logics and proposed schematic introduction rules and elimination to characterize the propositional connectives. Schroeder-Heister settings Prawitz extended and formalized the use of rules as hypotheses, making possible the use of separate calculations for assumptions of calculations for logical constants. We are not interested in the investigation of schematic rules to give meaning to the logical constants. We intend to actually set schematic standardization procedures, based on such schematic rules? Attic, in order to identify sufficient conditions for a system to be normalizável. These results are relevant to the Abstract Theory of Evidence, a term used to identify the study of the conditions abstract and general to the proof-theoretical analysis of formal systems. Abstract Theory of Evidence do not study specific logical calculations, but families of calculations instances of rules schematic. Our proposal is therefore based on rules schematic rules can be instantiated for concrete, in particular, by introducing rules modal operators. We prove also theorems Normalizaçãoo Weak and Strong systems defined in schematic funçãoo schematic of our rules, we obtain sufficient conditions for a system instance is normalizável these rules, we define a procedure that normalizes deductions concrete evidence and compare our standards with evidence schematic standards for systems defined in the literature. / O termo Teoria da Prova foi introduzido por Hilbert para identificar o estudo sobre provas formais. Pesquisas nessa área podem ser classificadas em: a) Teoria da Prova Redutiva ou Interpretacional, cujo objetivo é demonstrar, entre outras coisas, a consistência da matemática utilizando somente métodos finitistas, e b) Teoria da Prova Estrutural, onde características estruturais das provas formais são investigadas por meio de sistemas dedutivos como Dedução Natural e Cálculo de Sequentes. Prawitz, por meio da Teoria da Prova, definiu uma Teoria dos Significados para constantes logicas e propôs regras esquemáticas de introdução e de eliminação para caracterizar os conectivos proposicionais. Schroeder-Heister estendeu as definições de Prawitz e formalizou o uso de regras como hipóteses, tornando possível a utilização de cálculos para suposições separados de cálculos para constantes lógicas. Não estamos interessados na investigação de regras esquemáticas para dar significado a constantes lógicas. Pretendemos, na verdade, definir procedimentos de normalização esquemáticos, baseados em tais regras esquemáticas, com objetivo de identificar condições suficientes para um sistema ser normalizável. Tais resultados são pertinentes à Teoria Abstrata da Prova, termo usado para identificar o estudo das condições abstratas e gerais para a análise prova-teórica de sistemas formais. Teoria Abstrata da Prova não estuda cálculos lógicos específicos, mas famílias de cálculos instâncias de regras esquemáticas. A nossa proposta, portanto, baseia-se em regras esquemáticas que podem ser instanciadas por regras concretas, em particular, por regras que introduzem operadores modais. Provamos, também, Teoremas de Normalização Fraca e Forte para sistemas esquemáticos definidos em função de nossas regras esquemáticas, obtemos condições suficientes para que um sistema instância destas regras seja normalizável, definimos um procedimento que normaliza deduções concretas e comparamos nossas provas de normalização esquemática com provas de normalização para sistemas definidos na literatura.

[pt] O objetivo desta dissertação é construir um tableaux linear intuicionista a partir de um cálculo de sequentes relevante clássico. Os passos principais dessa construção são: i) tradução das regras do cálculo dos sequentes relevante clássico para regras de tableaux (capítulo 3), usando a estratégia apresentada por D Agostino et al. em Tableau Methods for Substructural Logic. ii) construção de um tableaux linear clássico através da linearização do tableaux clássico relevante (capítulo 4). iii) apresentar um tableau intuicionista ao estilo Fitting, em que são adicionados rótulos T s e F s às fórmulas (capítulo 5). / [en] The main goal of this master tesis is intuitionistic linear tableaux from a relevant sequent calculus. The central steps are: i) Apply D Agostino et al. strategy to translate classical relevant sequent calculus rules to tableaux rules for classical relevant logic (Chapter 3). ii) Use Meyer et al. strategy to linearize the classical relevant tableaux (Chapter 4). iii) Build a new intuicionistic linear tableaux with Fitting labels.

[pt] É um fato conhecido que provas clássicas podem ser demasiadamente grandes. Estudos em teoria da prova descobriram diferenças exponenciais entre provas normais (ou provas livres do corte) e suas respectivas provas não normais. Por outro lado, provadores automáticos de teorema usualmente se baseiam na construção de provas normais, livres de corte ou provas de corte atômico, pois tais procedimento envolvem menos escolhas. Provas de algumas tautologias são conhecidamente grandes quanto realizadas sem a regra do corte e curtas quando a utilizam. Queremos com este trabalho apresentar procedimentos para reduzir o tamanho de provas proposicionais. Neste sentido, apresentamos dois métodos. O primeiro, denominado método vertical, faz uso de axiomas de extensão e alguns casos é possível uma redução considerável no tamanho da prova. Apresentamos um procedimento que gera tais axiomas de extensão. O segundo, denominado método horizontal, adiciona fórmulas máximas por meio de unificação via substituição de variáveis proposicionais. Também apresentamos um método que gera tal unificação durante o processo de construção da prova. O primeiro método é aplicado a dedução natural enquanto o segundo à Dedução Natural e Cálculo de Seqüentes. As provas produzidas correspondem de certo modo a provas não normais (com a regra do corte). / [en] It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut-free proofs and their respective non-normal proofs. The task of automatic theorem proving is, on the other hand, usually based on the construction of normal, cut-free or only-atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies such that the cut-free proof is huge while the non-cut-free is small. The aim of this work is to reduce the weight of proposicional deductions. In this sense we present two methods. The fi first, namely vertical method, uses the extension axioms. We present a method that generates a such extension axiom. The second, namely horizontal method, adds suitable (propositional) unifi fications modulo variable substitutions.We also present a method that generates a such unifi fication during the proving process. The proofs produced correspond in a certain way to non normal proofs (non cut-free proofs).

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-04-03T22:46:24Z No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-04-11T20:56:41Z (GMT) No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Made available in DSpace on 2017-04-11T20:56:41Z (GMT). No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) Previous issue date: 2017-02-15 / Em L?gica Cl?ssica, podemos utilizar as hip?teses um n?mero indeterminado de vezes. Por exemplo, a prova de um teorema pode fazer uso do mesmo lema v?rias vezes. Por?m, em sistemas f?sicos, qu?micos e computacionais a situa??o ? diferente: um recurso n?o pode ser reutilizado ap?s ser consumido em uma a??o. Em L?gica Linear, f?rmulas s?o vistas como recursos a serem utilizados durante a prova. ? essa no??o de recursos que faz a L?gica Linear ser interessante para a modelagem de sistemas. Para tanto, a L?gica Linear controla o uso da contra??o e do enfraquecimento atrav?s dos exponenciais ! e ?. Este trabalho tem como objetivo fazer um estudo sobre a L?gica Linear com Subexponenciais (SELL), que ? um refinamento da L?gica Linear. Em SELL, os exponenciais da L?gica Linear possuem ?ndices, isto ?, ! e ? ser?o substitu?dos por !i e ?i, onde ?i? ? um ?ndice. Um dos pontos fundamentais de Teoria da Prova ? a prova da Elimina??o do Corte, que neste trabalho ? demonstrada tanto para L?gica Linear como para SELL, onde apresentamos detalhes que normalmente s?o omitidos. A partir do teorema de Elimina??o do Corte, podemos concluir a consist?ncia do sistema (para as l?gicas que estamos utilizando) e outros resultados como a propriedade de subf?rmula. O trabalho inicia-se com um cap?tulo de Teoria da Prova, e em seguida se faz uma exposi??o sobre a L?gica Linear. Assim, com essas bases, apresenta-se a L?gica Linear com Subexponenciais. SELL tem sido utilizada, por exemplo, na especifica??o e verifica??o de diferentes sistemas tais como sistemas bioqu?micos, sistemas de intera??o multim?dia e, em geral, em sistemas concorrentes com modalidades temporais, espaciais e epist?micas. Com essa base te?rica bastante clara, apresenta-se a especifica??o de um sistema bioqu?mico utilizando SELL. Al?m disso, apresentamos v?rias inst?ncias de SELL que tem interpreta??es interessantes do ponto de vista computacional. / In Classical Logic, we can use a given hypothesis an indefinite number of times. For example, the proof of a theorem may use the same lemma several times. However, in physical, chemical and computational systems, the situation is different: a resource cannot be reused after being consumed in one action. In Linear Logic, formulas are seen as resources to be used during a proof. This feature makes Linear Logic an interesting formalism for the specification and verification of such systems. Linear Logic controls the rules of contraction and weakening through the exponentials ! and ?. This work aims to study Linear Logic with subexponentials (SELL), which is a refinement of Linear Logic. In SELL, the exponentials of Linear Logic are decorated with indexes, i.e., ! and ? are replaced with !i and ?i, where ?i? is an index. One of the main results in Proof Theory is the Cut-Elimination theorem. In this work we demonstrate that theorem for both Linear Logic and SELL, where we present details that are usually omitted in the literature. From the Cut-Elimination Theorem, we can show, as a corollary, the consistency of the system (for the logics considered here) and other results as the subformula property. This work begins with an introduction to Proof Theory and then, it presents Linear Logic. On these bases, we present Linear Logic with subexponentials. SELL has been used, for example, in the specification and verification of various systems such as biochemical systems, multimedia interaction systems and, in general, concurrent systems with temporal, spatial and epistemic modalities. Using the theory of SELL, we show the specification of a biochemical system. Moreover, we present several instances of SELL that have interesting interpretations from a computational point of view.