[en] AN EXPERIMENTAL APPROACH ON MINIMAL IMPLICATIONAL NATURAL DEDUCTION PROOFS COMPRESSION

• Ano de defesa: 2020
• Autor(a) principal: JOSE FLAVIO CAVALCANTE BARROS JUNIOR
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: MAXWELL
• Palavras-chave em Português: [pt] TEORIA DA PROVA; [pt] COMPRESSAO DE PROVA; [pt] LOGICA MINIMAL; [en] PROOF THEORY; [en] PROOF COMPRESSION; [en] MINIMAL LOGIC
• Link de acesso: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=47267&idi=1; https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=47267&idi=2; http://doi.org/10.17771/PUCRio.acad.47267

[pt] O tamanho das provas formais possui algumas importantes implicações teóricas na área da complexidade computacional. O problema de determinar se uma fórmula é uma tautologia da Lógica Proposicional Intuicionista e do fragmento puramente implicacional da Lógica Minimal (M(contém)) é PSPACE- Completo. Qualquer lógica proposicional com um sistema de dedução natural que satisfaça o princípio da subfórmula possui o problema de determinar tautologias em PSPACE. Saber se qualquer tautologia em M(contém) admite provas de tamanho polinomialmente limitado está relacionado com saber se NP = PSPACE. Técnicas de compressão de provas reportadas na literatura utilizam duas abordagens principais para comprimir provas: gerar provas já compactadas; comprimir uma prova já gerada. Proposta por Gordeev e Haeusler (6), a Compressão Horizontal é uma técnica de compressão de provas em dedução natural da M(contém) que utiliza grafos direcionados para representar as provas. Dada a prova de uma tautologia qualquer da M(contém), que pode possuir tamanho exponencial em relação ao tamanho da conclusão, o objetivo da Compressão Horizontal é que a prova resultante da compressão possua tamanho polinomialmente limitado em relação ao tamanho da conclusão. Nosso trabalho apresenta a primeira implementação da Compressão Horizontal, juntamente com os primeiros resultados da aplicação da técnica sobre provas de tautologias da M(contém), além disso, compara as taxas de compressão obtidas com técnicas tradicionais de compressão de dados.