NormalizaÃÃo para os N-Grafos

AUTOR(ES)

Gleifer Vaz Alves

DATA DE PUBLICAÇÃO

2005

RESUMO

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 works. Here we cite two investigations which share this goal, e.g., Ungar [Ung92] and Cellucci [Cel92]. However, taking a careful look at these works we notice that a normalization procedure, which handles inherent features of a proof structure with more than one conclusion, is only mildly addresses. Therefore, our work has as center goal the definition of a normalization procedure for proof-graphs. Indeed, using graphs to represent derivations is the key feature to define normalization for a structure with more than one conclusion. Here the proof-graphs are represented by N-Graphs, that is a symmetrical natural deduction proof system with logical and structural rules. This rules are described in a multiple conclusion framework. In order to create normalization for N-Graphs, we have constructed five reductions sets: logical, structural, cycle, repeated cycle sequence and weakening permutative reductions. The reductions definitions were based on the works of Prawitz, Ungar and Cellucci. In addition to this, they were strongly inspired by N-Graphs multiple conclusion framework, especially to tackle the inherent issues of such a normalization proof structure. Furthermore we have developed the normalization theorem, the normalization direct proof, as well as the termination and (weak) confluence properties. Having defined the normalization for N-Graphs, we are able to devise some forthcoming works, such as, computational applications, a correspondence between formal proofs and concurrent processes and an investigation towards an identity of proofs criteria

ASSUNTO(S)

normalization normalizaÃÃo grafos-de-prova ciencia da computacao proof theory proof-graphs teoria da prova

Documentos Relacionados

• Em DireÃÃo aos N-Grafos Intuicionistas
• NormalizaÃÃo da gestÃo de P&D&I: uma contribuiÃÃo para a capacidade de inovaÃÃo das empresas brasileiras
• Standardization of Theses and Dissertations in the Context of the Digital Library
• SimulaÃÃo de turbinas a gÃs utilizando modelagem por meio de grafos de ligaÃÃo e identificaÃÃo linear e nÃo-linear.
• Teorema de geometrizaÃÃo para girassÃis de grafos com valÃncia mÃnima trÃs