slideshow 3

Logic seminar

A lower bound for Polynomial Calculus with extension rule

Yaroslav Alekseev
Chebyshev Laboratory, St Petersburg State University


Monday, 16. November 2020 - 15:30 to 17:00

Zoom meeting 472 648 284 -

In this talk we consider 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.