ETDs @PUC-Rio
| Título: | ARGUING NP = PSPACE: ON THE COVERAGE AND SOUNDNESS OF THE HORIZONTAL COMPRESSION ALGORITHM | ||||||||||||
| Autor: |
ROBINSON CALLOU DE M BRASIL FILHO |
||||||||||||
| Colaborador(es): |
EDWARD HERMANN HAEUSLER - Orientador |
||||||||||||
| Catalogação: | 12/SET/2024 | Língua(s): | ENGLISH - UNITED STATES |
||||||||||
| Tipo: | TEXT | Subtipo: | THESIS | ||||||||||
| Notas: |
[pt] 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. [en] All data contained in the documents are the sole responsibility of the authors. The data used in the descriptions of the documents are in conformity with the systems of the administration of PUC-Rio. |
||||||||||||
| Referência(s): |
[pt] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=67979&idi=1 [en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=67979&idi=2 |
||||||||||||
| DOI: | https://doi.org/10.17771/PUCRio.acad.67979 | ||||||||||||
| Resumo: | |||||||||||||
|
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.
|
|||||||||||||
|
|||||||||||||