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: LOGIC PROOFS COMPACTATION
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Autor(es): VASTON GONCALVES DA COSTA

Colaborador(es):  EDWARD HERMANN HAEUSLER - Orientador
Número do Conteúdo: 10018
Catalogação:  01/06/2007 Idioma(s):  PORTUGUESE - BRAZIL

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=10018@1
Referência [en]:  https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=10018@2
Referência DOI:  https://doi.org/10.17771/PUCRio.acad.10018

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

Descrição Arquivo
COVER, ACKNOWLEDGEMENTS, RESUMO, ABSTRACT, SUMMARY AND LISTS  PDF
CHAPTER 1  PDF
CHAPTER 2  PDF
CHAPTER 3  PDF
CHAPTER 4  PDF
CHAPTER 5  PDF
REFERENCES AND APPENDICES  PDF
Agora você pode usar seu login do SAU no Maxwell!!
Fechar Janela



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