论文标题
关于最小纯粹含义逻辑中DAG衍生的水平压缩
On the horizontal compression of dag-derivations in minimal purely implicational logic
论文作者
论文摘要
本报告在最小逻辑$ m _ {\ supset} $的纯粹含义片段中定义了（纯）类似dag的派生。引入水平崩溃的规则集和算法{\ bf hc}。解释为什么{\ bf hc}可以将$ M _ {\ supset} $ tautology的任何多项式高度的树状的证据转化为类似于DAG的证明。绘制一个证明{\ bf hc}在水平崩溃应用程序后，在其dag的版本中保留了$ m _ {\ supset} $中任何类似树的nd的声音。我们展示了有关将压缩方法应用于一类（巨大的）命题证明的一些实验结果，以及具有非汉密尔顿图的示例进行定性分析。贡献包括对水平压缩集（HC）的全面呈现，即HC规则保留健全性的证明的（草图），以及当提交的树状证明是高度的高度和粉底型的一聚体时，压缩的DAG样证明是多项式上限的。最后，在附录中，我们概述了一种算法，该算法在多项式时间验证了类似于DAG的证据的大小是否是其结论的有效证明。在结论中，我们讨论了使用Interactive TheoRem Prover saverive verneive sirace证明了对HC压缩DAG的形式结果的哪一部分。
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.
