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.

翻译：在本文中,我们研究了多角计算校准系统的延伸,我们可以在此过程中引入新的变量并取一个平方根。我们证明子数和原则的例子,即二进制值原则,需要对这一系统中的理性进行指数化比特大小的反驳。部分和Tzameret证明,对二进制值原则的反比(分辨率超过线性方程)的反比的反比是指数性较低的。我们显示,我们的系统模拟Res-Lin,因此我们得到了一个替代的指数性较低的约束,以适应Res-Lin对二进制值原则的反比。