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

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.