[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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:67979 |
| Date | 12 September 2024 |
| Creators | ROBINSON CALLOU DE M BRASIL FILHO |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | English |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0022 seconds