Пятница 07.08. Ярослав Алексеев: "Нижняя оценка для обобщения системы PC и моделирование системы Res-Lin"

Пятница, 7 августа, Zoom. Начало в 11:00.

Докладчик: Ярослав Алексеев (СПбГУ).

Тема: Нижняя оценка для обобщения системы PC и моделирование системы Res-Lin.

Abstract

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

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

Видео: https://www.youtube.com/watch?v=7TlFIncDuck