Defesa de Tese de Doutorado do aluno Robinson Callou de M. Brasil Filho
Título da Tese: Arguing NP = PSPACE: On the Coverage and Soundness of the Horizontal Compression Algorithm
Resumo: This work is an elaboration, with examples, on the presented Horizontal Compression Algorithm (HC) and its set of compression rules. This work argues a proof, done with the Lean Interactive Theorem Prover, that the HC algorithm can obtain a dag-like compressed derivation 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.
Orientador: Prof. Dr. Edward Hermann Haeusler
Banca: Prof. Dr Alex de Vasconcellos Garcia | Prof. Dr. Alexandre Rademaker | Prof. Dr. Jefferson de Barros Santos | Prof. Dr. Mauricio Ayala Rincon | Prof. Dr. Mario Roberto Folhadela Benevides | Prof. Dr. Bernardo Pinto de Alkmim
Assista a defesa pelo link https://puc-rio.zoom.us/j/93015522144?pwd=SXA4bTIzSnYxNUwzK3NwT2ZMeXgwUT09