Natural Deduction
Mostrando 1-12 de 12 artigos, teses e dissertações.
-
1. Sistemas EsquemÃticos de DeduÃÃo Natural: um Estudo Prova-TeÃrico / Schematic Natural Deduction Systems: A Proof-Theoretical Study
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
IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia. Publicado em: 12/03/2010
-
2. 2-CATEGORY AND PROOF THEORY / 2-CATEGORIA E TEORIA DA PROVA
Natural Deduction for intuitionistic logic has been related to Category Theory by what now is known as Categorical Logic. This relationship is strongly based on the Curry-Howard Isomorphism between Natural Deduction and typed (lambda)-Calculus. This dissertation describes some aspects of these relationship with the aim of proposing a 2-categorical view of ca
Publicado em: 2009
-
3. Transformations for proof-graphs with cycle treatment augmented via geometric perspective techniques
O presente trabalho é baseada em dois aspectos fundamentais: (i) o estudo de procedimentos de normalização para sistemas de provas, especialmente para a lógica clássica com dedução natural; e (ii) a investigação de técnicas da perspectiva geométrica aplicadas em propriedades da teoria da prova. Com isso, a motivação específica deste trabalho re
Publicado em: 2009
-
4. LOGIC PROOFS COMPACTATION / COMPACTAÇÃO DE PROVAS LÓGICAS
É 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 pro
Publicado em: 2007
-
5. A infinitary system of the logic of least fixed-point / Um sistema infinitÃrio para a lÃgica de menor ponto fixo
A noÃÃo de menor ponto-fixo de um operador à amplamente aplicada na ciÃncia da computaÃÃo como, por exemplo, no contexto das linguagens de consulta para bancos de dados relacionais. Algumas extensÃes da LÃgica de Primeira-Ordem (FOL)1 com operadores de ponto-fixo em estruturas finitas, como a lÃgica de menor ponto-fixo (LFP)2, foram propostas para l
Publicado em: 2007
-
6. Uma investigação acerca das regras para a negação e o absurdo em dedução natural
O objetivo desta tese é o de propor uma elucidação da negação e do absurdo no âmbito dos sistemas de dedução natural para as lógicas intuicionista e clássica. Nossa investigação pode ser vista como um desenvolvimento de uma proposta apresentada por Russell há mais de cem anos e a qual ele parece ter abandonado posteriormente. Focaremos a atenç�
Publicado em: 2006
-
7. NormalizaÃÃo para os N-Grafos
The main tools of general proof theory are cut-elimination (classical sequent calculus) and normalization (classical natural deduction). In proof theory, both tools are used by several related investigations. But, when we consider a normalization procedure for classical logic with a proof structure which presents more than one conclusion, we find few related
Publicado em: 2005
-
8. A GENERAL APPROACH TO QUANTIFIERS IN NATURAL DEDUCTION / UMA ABORDAGEM GERAL PARA QUANTIFICADORES EM DEDUÇÃO NATURAL
There are many kinds of deductive calculus. The axiomatic ones are the more usual. However, from the point of view of proof theory, Natural Deduction systems seem to be more interesting. This is the motivation for developping a technique that aims to ease the transformation from deductive calculus to Natural Deduction style. This work concentrates on the asp
Publicado em: 2004
-
9. Hierarquias de sistemas de dedução natural e de sistemas de tableaux analiticos para os sistemas Cn de da Costa
In this work, we introduce the hierarchy of propositional natural deduction systems DNCn, 1≤n≤ω, and the hierarchy of quantificational natural deduction systems DNCn*, 1≤n≤ω. We prove that each one of the systems of the hierarchies is equivalent to the corresponding system of the hierarchy of da Costa´s propositional paraco
Publicado em: 2004
-
10. EXTRAÇÃO DE CONTEÚDO COMPUTACIONAL DE PROVAS INTUICIONISTAS / EXTRACTION OF COMPUTATIONAL CONTENTS FROM INTUITIONIST PROOFS
Garantir que programas são implementados de forma a cumprir uma especificação é uma questão fundamental em computação, por isso, têm sido propostos vários métodos que almejam provar a correção dos programas. Este trabalho apresenta um método, baseado no isomorfismo de Curry-Howard, que extrai conteúdos computacionais de provas intuicionistas, c
Publicado em: 2004
-
11. Um estudo de C omega em calculo de sequentes e dedução natural
Following Raggio s 1968 and 1978 papers on Cn1
w systems, it isdeveloped here an analysis of Cw in Sequent Calculus and Natural Deduction, presenting respectively the Cut Elimination and the Strong Normalization Theorems as main results. Relevant characteristics are the treatment applied to negation and the permissibility of normal proof definition Publicado em: 2001
-
12. Study of the dynamics of neutralization escape mutants in a chimpanzee naturally infected with the simian immunodeficiency virus SIVcpz-ant.
Here we report on the use of spectral map analysis of time-paired sequential neutralization data of 11 serum samples of a chimpanzee naturally infected with a simian immunodeficiency virus (SIVcpz-ant) and 8 primary consecutive SIVcpz-ant isolates, taken at about 4-month intervals. The analysis reveals the existence of three SIVcpz-ant isolate and serum neut