[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. / [en] The size of formal proofs has some important theoretical implications in computational complexity theory. The problem of determining if some formula of Intuitionistic Propositional Logic and the purely implicational fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any propositional logic with a natural deduction system that satisfies the sub- formula principle is PSPACE. To know if any tautology in M(contains) admits polynomially sized proof is related to whether NP = PSPACE. Proof compression techniques reported in literature use two main approaches to proof compressing: generating already compressed proofs; compressing an already generated proof. Proposed by Gordeev and Haeusler (6), the Horizontal Compression is a natural deduction proof compression technique that uses directed graphs to represent proofs. Given a tautology proof in M(contains), which may have an exponential size in relation to conclusion length, the goal of Horizontal Compression is that the compressed proof has a polynomially limited size in relation to conclusion length. Our work presents the first implementation of Horizontal Compression, together with the first results of the execution of the technique on proofs of M(contains) tautologies.

[pt] A história recente da Lógica Matemática foi marcada por alguns conflitos entre diferentes correntes filosóficas, cada uma buscando contextualizar a atividade matemática a partir de seu próprio prisma analítico e, por meio disso, tentando conquistar para si mesma o pódio fundacional das Ciências Formais Tais discussões, perenes o bastante para ainda quedarem sem solução, foram fortemente impactadas pela apropriação semântica de alguns resultados técnicos obtidos no campo da teoria da prova, o que redefiniu a relação existente entre as abordagens clássica e intuicionista na matemática. Neste contexto, a presente dissertação tem por finalidade realizar uma descrição da emergente literatura de propostas integrativas entre diferentes sistemas lógicos e matemáticos (apelidadas por Dag Prawitz de ecumenismo lógico), além de investigar alguns impactos que mudanças formais poderiam ocasionar nas concepções filosóficas de algumas teorias matemáticas. No capítulo introdutório, traçamos um panorama geral desta nova proposta ecumênica e analisamos com mais atenção o conflito entre as lógicas Clássica, Intuicionista e Minimal, considerado por muitos como um dos mais influentes na literatura contemporânea. No segundo capítulo, este trabalho fornece uma contribuição original para a literatura ao criar uma nova abordagem ecumênica, além de provar algumas equivalências no interior do sistema Clássico-Intuicionista recentemente criado por Prawitz e compará-lo com uma lógica que criamos usando esta nova abordagem. No terceiro capítulo, contribuímos tanto com a abordagem tradicional quanto com nossa abordagem original ao criar e comparar dua lógicas ecumênicas Minimal-Intuicionistas. Por fim, realizamos uma breve revisão do tímido estado da arte no último capítulo, oferecendo um novo esquema conceitual de interpretação dos sistemas ecumênicos e comentando alguns aspectos promissores do campo, que poderão vir a ser melhor trabalhados no futuro. / [en] The recent history of Mathematical Logic was marked by some conficts between different philosophical positions, each trying to contextualize mathematical activity from its own analytical viewpoint and, with this, trying to conquer the foundational podium of the formal sciences for itself. Such discussions, lasting enough to remain without a solution, were strongly impacted by the semantical appropriation of some technical results obtained in the field of proof theory, which redefined the relation between the classical and intuitionistic approaches to mathematics. In this context, the present dissertation aims to describe the emergent literature about the integration of different logical and mathematical systems (nicknamed logical ecumenism by Dag Prawitz), in addition to investigating some impacts that those formal changes could have on the philosophical conceptions of some mathematical theories. In the introductory chapter, we have outlined a general overview of this new ecumenical proposal and analysed in greater depht the conflicts between Classical, Intuitionistic and Minimal logic, considered by many as one of the most influent on the contemporary literature. In the second chapter, this work provides an original contribution to the literature by creating a new ecumenical approach, in addition to proving some equivalencies within Prawitz s recently created Classical-Intuitionist system, and compares it with the logical system we have created using this new approach. In the third chapter, we contribute both to the traditional approach and our original approach by creating and comparing two Minimal-Intuitionist ecumenical logics. Finally, we briefly review the timid state of the art in the last chapter, offering a new conceptual framework for interpreting ecumenical systems, as well as commenting on some promising aspects of the field, which may be better analyzed in the future.

[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.