论文标题
关于巨大自然扣除证明的固有冗余ii：分析$ m _ {\ im im} $超级多项式证明
On the Intrinsic Redundancy in Huge Natural Deduction proofs II: Analysing $M_{\imply}$ Super-Polynomial Proofs
论文作者
论文摘要
本文精确地定义了自然扣除系统中的巨大证据，以最小的含义命题逻辑\ mil。这就是我们所说的一个无限的超级物质证明家庭。我们考虑了扩展的正常形式映射证明的巨大家庭，这是一种以适当的方式来明确帮助计算正常证明的电子零件的设备。因此，我们表明，对于那些超级多项式家族的几乎所有成员，至少一个子范围或每个派生都多次重复多次超多个元素。我们称之为超级多项式冗余的最后一个属性。几乎全部，恰恰意味着证据的结论很大，表明每个证明的结论都比这种大小更大，而且巨大也是高度冗余的。该结果指出了先前提出的压缩方法的完善，以及conp = np的替代和简单的证据。
This article precisely defines huge proofs within the system of Natural Deduction for the Minimal implicational propositional logic \mil. This is what we call an unlimited family of super-polynomial proofs. We consider huge families of expanded normal form mapped proofs, a device to explicitly help to count the E-parts of a normal proof in an adequate way. Thus, we show that for almost all members of a super-polynomial family there at least one sub-proof or derivation of each of them that is repeated super-polynomially many times. This last property we call super-polynomial redundancy. Almost all, precisely means that there is a size of the conclusion of proofs that every proof with conclusion bigger than this size and that is huge is highly redundant too. This result points out to a refinement of compression methods previously presented and an alternative and simpler proof that CoNP=NP.
