XINFORMAÇÕ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.
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
Título: AN EXPERIMENTAL APPROACH ON MINIMAL IMPLICATIONAL NATURAL DEDUCTION PROOFS COMPRESSION Autor: JOSE FLAVIO CAVALCANTE BARROS JUNIOR
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):
EDWARD HERMANN HAEUSLER - ADVISOR
Nº do Conteudo: 47267
Catalogação: 26/03/2020 Liberação: 26/03/2020 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=47267@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=47267@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.47267
Resumo:
Título: AN EXPERIMENTAL APPROACH ON MINIMAL IMPLICATIONAL NATURAL DEDUCTION PROOFS COMPRESSION Autor: JOSE FLAVIO CAVALCANTE BARROS JUNIOR
Nº do Conteudo: 47267
Catalogação: 26/03/2020 Liberação: 26/03/2020 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=47267@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=47267@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.47267
Resumo:
The size of formal proofs has some important theoretical implications
in computational complexity theory. The problem of determining if some
formula of Intuitionistic Propositional Logic and the purely implicational
fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any
propositional logic with a natural deduction system that satisfies the sub-
formula principle is PSPACE. To know if any tautology in M(contains) admits
polynomially sized proof is related to whether NP = PSPACE. Proof
compression techniques reported in literature use two main approaches
to proof compressing: generating already compressed proofs; compressing
an already generated proof. Proposed by Gordeev and Haeusler (6), the
Horizontal Compression is a natural deduction proof compression technique
that uses directed graphs to represent proofs. Given a tautology proof in
M(contains), which may have an exponential size in relation to conclusion length,
the goal of Horizontal Compression is that the compressed proof has a
polynomially limited size in relation to conclusion length. Our work presents
the first implementation of Horizontal Compression, together with the first
results of the execution of the technique on proofs of M(contains) tautologies.
Descrição | Arquivo |
COMPLETE |