关于极小纯蕴涵逻辑中 dag 推导式的水平压缩

本报告定义了极小逻辑 $M_{\supset}$ 的纯蕴涵片段中的(plain)Dag 类推导式。引入水平坍缩规则集与算法 {\bf HC}。解释为何 {\bf HC} 能将 $M_{\supset}$ 重言式的任意多项式高度有界的树状证明转化为更小的 dag 类证明。概述一个证明:在应用水平坍缩后,{\bf HC} 将 $M_{\supset}$ 中任意树状 ND 的可靠性保持为其 dag 类版本。我们展示了将该压缩方法应用于一类(庞大的)命题证明以及一些示例的实验结果,并以非哈密顿图为例作定性分析。贡献包括:水平压缩(HC)规则集的完整表述、HC 规则保持可靠性的证明(草图),以及当所提交的树状证明在高度与基础上有多项式界时,压缩后的 dag 类证明具有多项式上界的论证。最后,在附录中我们勾勒了一个算法,可在 dag 类证明规模上以多项式时间验证它们是否为其结论的有效证明。在结论中,我们讨论了关于 HC 压缩 dag 类证明的形式化结果中有哪些部分是借助交互式定理证明器辅助完成的。