Мы рассмотрим обобщение системы Polynomial Calculus, в котором дополнительно можно извлекать квадратный корень из многочлена и вводить новые переменные, записывающие многочлены от исходных переменных. Мы докажем экспоненциальную нижнюю оценку на размер опровержения в этой системе равенства $BVP_n$ ($1 + 2 x_1 + 2^2 x_2 + ... + 2^n x_n = 0$), при этом для доказательства нижней оценки на размер доказательства нам не потребуется нижняя оценка на степень. Благодаря тому, что эта система полиномиально моделирует Res-Lin (систему, оперирующую дизъюнкциями линейных уравнений; введена Разом и Цамеретом), мы получим альтернативное доказательство нижней оценки Парта и Цамерета на размер доказательств $BVP_n$ в Res-Lin.

Семинар будет проходить онлайн в конференции zoom. Ссылка для подключения будет выслана в рассылку за пару часов до доклада.