论文标题
具有扩展规则的多项式演算的下限
A Lower Bound for Polynomial Calculus with Extension Rule
论文作者
论文摘要
在本文中，我们研究了多项式演算系统的扩展，我们可以在其中引入新的变量并取出平方根。我们证明，子集原理的实例，即二进制价值原理，需要对该系统中的理由的指数位大小进行反驳。 Part和Tzameret证明了对二进制值原理的RES-LIN（线性方程式分辨率）的大小（分辨率）的指数下限。我们表明我们的系统p缩小了res-lin，因此我们获得了二进制价值原理的RES-LIN反驳的替代指数下限。
In this paper we study an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations of exponential bit size over rationals in this system. Part and Tzameret proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations) refutations of the binary value principle. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of the binary value principle.
