$$\newcommand{\bra}[1]{\left<#1\right|}\newcommand{\ket}[1]{\left|#1\right>}\newcommand{\bk}[2]{\left<#1\middle|#2\right>}\newcommand{\bke}[3]{\left<#1\middle|#2\middle|#3\right>}$$
X
INFORMAÇÕES SOBRE DIREITOS AUTORAIS


As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.

A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.

A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.

A violação de direitos autorais é passível de sanções civis e penais.
Coleção Digital

Avançada


Estatísticas | Formato DC |



Título: SOME RESULTS IN A PROOF-THEORY BASED ON GRAPHS
Autor: MARCELA QUISPE CRUZ
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):  EDWARD HERMANN HAEUSLER - ADVISOR
LEW GORDEEV - CO-ADVISOR

Nº do Conteudo: 28745
Catalogação:  19/01/2017 Idioma(s):  ENGLISH - UNITED STATES
Tipo:  TEXT Subtipo:  THESIS
Natureza:  SCHOLARLY PUBLICATION
Nota:  Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio.
Referência [pt]:  https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=28745@1
Referência [en]:  https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=28745@2
Referência DOI:  https://doi.org/10.17771/PUCRio.acad.28745

Resumo:
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.

Descrição Arquivo
COVER, ACKNOWLEDGEMENTS, ABSTRACT, RESUMO, SUMMARY AND LIST OF FIGURES  PDF
CHAPTER 1  PDF
CHAPTER 2  PDF
CHAPTER 3  PDF
CHAPTER 4  PDF
CHAPTER 5  PDF
CHAPTER 6  PDF
CHAPTER 7  PDF
REFERENCES  PDF
Logo maxwell Agora você pode usar seu login do SAU no Maxwell!!
Fechar Janela



* Esqueceu a senha:
Senha SAU, clique aqui
Senha Maxwell, clique aqui