[en] ARGUING NP = PSPACE: ON THE COVERAGE AND SOUNDNESS OF THE HORIZONTAL COMPRESSION ALGORITHM

[pt] ARGUMENTANDO NP = PSPACE: SOBRE A COBERTURA E CORRETUDE DO ALGORITMO DE COMPRESSÃO HORIZONTAL

[pt] ROBINSON CALLOU DE M BRASIL FILHO

[pt] GRAFO ACICLICO DIRECIONADO

[pt] COMPLEXIDADE DE ALGORITMOS

[pt] LOGICA MINIMAL PURAMENTE IMPLICACIONAL

[pt] COMPRESSAO DE PROVA

[en] DIRECTED ACYCLIC GRAPH

[en] ALGORITHM COMPLEXITY

[en] PURELY IMPLICATIONAL MINIMAL LOGIC

[en] PROOF COMPRESSION

[pt] Este trabalho é uma elaboração, com exemplos, e evolução do Algoritmo de Compressão Horizontal (HC) apresentado e seu Conjunto de Regras de Compressão. Este trabalho apresenta uma prova, feita no Provador Interativo de Teoremas Lean, de que o algoritmo HC pode obter uma Derivação Comprimida, representada por um Grafo Acíclico Dirigido, a partir de qualquer Derivação Tipo-Árvore em Dedução Natural para a Lógica Minimal Puramente Implicacional. Finalmente, a partir da Cobertura e Corretude do algoritmo HC, pode-se argumentar que NP = PSPACE.

[en] This work is an elaboration, with examples, and evolution of the presented Horizontal Compression Algorithm (HC) and its set of Compression Rules. This work argues a proof, done in the Lean Interactive Theorem Prover, that the HC algorithm can obtain a Compressed Derivation, represented by a Directed Acyclic Graph, from any Tree-Like Natural Deduction Derivation in Minimal Purely Implicational Logic. Finally, from the Coverage and Soundness of the HC algorithm, one can argue that NP = PSPACE.

EDWARD HERMANN HAEUSLER

EDWARD HERMANN HAEUSLER

JEFFERSON DE BARROS SANTOS

MAURICIO AYALA RINCON

ALEX DE VASCONCELLOS GARCIA

BERNARDO PINTO DE ALKMIM

ALEXANDRE RADEMAKER

MARIO ROBERTO FOLHADELA BENEVIDES

2024-09-12

2024-04-30

[pt] TEXTO

application/pdf

INGLÊS

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=67979@1

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=67979@2

https://doi.org/10.17771/PUCRio.acad.67979