Sequent Calculus
Mostrando 1-6 de 6 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. Especificação de sistemas utilizando lógica linear com subexponencias
Logic programming is defined as the use of logic formulas representing programs and proof search of these formulas as the execution of the program (computation). This is an interesting paradigm because of the specifications formality, which is inherited from the logic itself and facilitates the proof of some properties that would not be so obvious if the pro
Publicado em: 2010
-
3. Em DireÃÃo aos N-Grafos Intuicionistas
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
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. 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
-
6. 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