This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic $M_{\imply}$. 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_{\imply}$ tautology into a smaller dag-like proof. Sketch a proof that {\bf HC} preserves the soundness of any tree-like ND in $M_{\imply}$ 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.

翻译：本报告定义了在极小逻辑$M_{\imply}$的纯蕴涵片段中的（纯净）类DAG推导。引入水平压缩规则集与算法{\bf HC}。解释{\bf HC}如何能将任意多项式高度有界的$M_{\imply}$重言式树状证明转化为更小的类DAG证明。概述了在水平压缩应用后，{\bf HC}能保持$M_{\imply}$中任意树状自然演绎（ND）在类DAG版本中的可靠性的证明思路。我们展示了将该压缩方法应用于一类（大型）命题证明的实验结果，并给出了一个涉及非哈密顿图示例的定性分析。主要贡献包括：水平压缩（HC）规则集的全面呈现、HC规则保持可靠性的证明（概要）、以及证明了当待处理树状证明的高度与基础均为多项式有界时，压缩后的类DAG证明具有多项式上限。最后，在附录中概述了一个算法，该算法能在类DAG证明规模的多项式时间内验证其是否为有效结论证明。