论文标题
从最小的含义逻辑中从巨大到小的：有效的简洁证明表示
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.
