从大到小：最小蕴涵逻辑中证明的高效简洁表示
Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logic
摘要：
以前的一篇文章表明，在最小蕴涵逻辑$M_{\supset}$的自然演绎中，重言式的任何线性高度有界正规证明都是巨大的，因为它是冗余的。更准确地说，在一个超多项式大小和线性高度有界的证明族中的任何证明都有一个子导子，它在其中超多项式出现多次。在这篇文章中，我们证明了通过折叠所有重复的子导子，我们得到了一个更小的结构，一个有根的有向无环图（r-DAG），其在$α$的大小上是多项式上界的，并且证明$α$是可以在多项式时间内验证的重言式。换句话说，对于$M_{\supset}$中重言式的每一个巨大的证明，我们都获得了一个简洁的有效性证明。此外，我们展示了一个算法，能够检查这种有效性在多项式时间上的证书的大小。评论如何在这篇文章中的结果是相关的证明的猜想$NP=CoNP$出现在结论。
英文摘要：
A previous article shows that any linear height bounded normal proof of a tautology in the Natural Deduction for Minimal implicational logic $M_{\supset}$ is as huge as it is redundant. More precisely, any proof in a family of super-polynomially sized and linearly height bounded proofs have a sub-derivation that occurs super-polynomially many times in it. In this article, we show that by collapsing all the repeated sub-derivations we obtain a smaller structure, a rooted Directed Acyclic Graph (r-DAG), that is polynomially upper-bounded on the size of $α$ and it is a certificate that $α$ is a tautology that can be verified in polynomial time. In other words, for every huge proof of a tautology in $M_{\supset}$, we obtain a succinct certificate for its validity. Moreover, we show an algorithm able to check this validity in polynomial time on the certificate's size. Comments on how the results in this article are related to a proof of the conjecture $NP=CoNP$ appears in conclusion.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
