Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the horizontal compression of dag-derivations in minimal purely implicational logic

Edward Hermann Haeusler, José Flávio Cavalcante Barros Junior, Robinson

TL;DR

The paper presents Horizontal Compression (HC) as a method to transform tree-like Natural Deduction proofs in the pure implicational fragment of minimal logic, $M_{}$, into polynomial-size dag-like proofs (DLDS) by horizontally collapsing identical formula occurrences. It introduces the HC rules, the DLDS formalism, and a Flow-based mechanism to verify soundness, establishing polynomial bounds when input proofs have height and foundation poly-bounded structure. It also reports on experimental results comparing HC with Huffman compression on large propositional proofs and outlines partial formalization in an Interactive Theorem Prover. The work advances proof compression and verification, offering a framework with potential for rigorous formalization and practical proof-checking improvements.

Abstract

This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic $M_{\supset}$. Introduce the horizontal collapsing set of rules and the algorithm {\bf HC}. Explain why {\bf HC} can transform any polynomial height-bounded tree-like proof of a $M_{\supset}$ tautology into a smaller dag-like proof. Sketch a proof that {\bf HC} preserves the soundness of any tree-like ND in $M_{\supset}$ in its dag-like version after the horizontal collapsing application. We show some experimental results about applying the compression method to a class of (huge) propositional proofs and an example, with non-hamiltonian graphs, for qualitative analysis. The contributions include the comprehensive presentation of the set of horizontal compression (HC), the (sketch) of the proof that HC rules preserve soundness and the demonstration that the compressed dag-like proofs are polynomially upper-bounded when the submitted tree-like proof is height and foundation poly-bounded. Finally, in the appendix, we outline an algorithm that verifies in polynomial time on the size of the dag-like proofs whether they are valid proofs of their conclusions.In the conclusion we discuss what part of the formal results on the HC-compressed dag-like proofs have been proved with the use of Interactive Theorem Prover assistance.

On the horizontal compression of dag-derivations in minimal purely implicational logic

TL;DR

The paper presents Horizontal Compression (HC) as a method to transform tree-like Natural Deduction proofs in the pure implicational fragment of minimal logic, , into polynomial-size dag-like proofs (DLDS) by horizontally collapsing identical formula occurrences. It introduces the HC rules, the DLDS formalism, and a Flow-based mechanism to verify soundness, establishing polynomial bounds when input proofs have height and foundation poly-bounded structure. It also reports on experimental results comparing HC with Huffman compression on large propositional proofs and outlines partial formalization in an Interactive Theorem Prover. The work advances proof compression and verification, offering a framework with potential for rigorous formalization and practical proof-checking improvements.

Abstract

This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic . Introduce the horizontal collapsing set of rules and the algorithm {\bf HC}. Explain why {\bf HC} can transform any polynomial height-bounded tree-like proof of a tautology into a smaller dag-like proof. Sketch a proof that {\bf HC} preserves the soundness of any tree-like ND in in its dag-like version after the horizontal collapsing application. We show some experimental results about applying the compression method to a class of (huge) propositional proofs and an example, with non-hamiltonian graphs, for qualitative analysis. The contributions include the comprehensive presentation of the set of horizontal compression (HC), the (sketch) of the proof that HC rules preserve soundness and the demonstration that the compressed dag-like proofs are polynomially upper-bounded when the submitted tree-like proof is height and foundation poly-bounded. Finally, in the appendix, we outline an algorithm that verifies in polynomial time on the size of the dag-like proofs whether they are valid proofs of their conclusions.In the conclusion we discuss what part of the formal results on the HC-compressed dag-like proofs have been proved with the use of Interactive Theorem Prover assistance.
Paper Structure (14 sections, 31 theorems, 12 equations, 62 figures, 7 algorithms)

This paper contains 14 sections, 31 theorems, 12 equations, 62 figures, 7 algorithms.

Table of Contents

  1. Introduction
  2. Horizontally compressing Natural Deduction derivations into a Dag-like Derivations
  3. Dag-like proofs basic definitions
  4. Dropping out the discharging ($E_d$) edges
  5. The Horizontal compressing procedure
  6. The compression rules
  7. On the classification and type of rules
  8. More on DGTD, DLDS and compression rules soundness preservation
  9. HC rules and DLDS validity preservation
  10. On the size of compressed Natural Deduction proofs
  11. On the experimental compression rate of the algorithm
  12. Conclusion and further research
  13. A polynomial time algorithm to verify validity of DLDS
  14. An example using the function $Flow$

Key Result

Proposition 1

Let $\Pi$ be a Natural Deduction derivation of $\alpha$ from $\Gamma$ in $M_{\supset}$. There is a tree-like derivation $\mathcal{T}=\langle V,E_D,E_d,r,l\rangle$, such that:

Figures (62)

  • Figure 1: Deriving $A_1\supset A_5$ from $A_1\supset A_2$, $A_1\supset(A_2\supset A_3)$, $A_2\supset(A_3\supset A_4)$ and $A_3\supset(A_4\supset A_5)$
  • Figure 2: Labelled graph representation of derivation \ref{['fig:example-deriv']}
  • Figure 3: (a)$u$ and $v$ collapse (b) After collapse $HCom(u,v)$
  • Figure 4: Matching of the HC-compression rule $\mathbf{R0EE}$ with the derivation-tree in figure \ref{['fig:graph-derivation1']}
  • Figure 5: Result of the HC-compression rule $\mathbf{R0EE}$ application according the matching shown in figure \ref{['fig:match-rule-derivation1']}
  • ...and 57 more figures

Theorems & Definitions (65)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Proposition 1
  • Proposition 2
  • Definition 5
  • Definition 6
  • Lemma 3: Greedy $\supset$-Intro are complete
  • Definition 7: Decorated Greedy N.D. derivation
  • ...and 55 more