Пятница, 7 августа, Zoom. Начало в 11:00.
Докладчик: Ярослав Алексеев (СПбГУ).
Тема: Нижняя оценка для обобщения системы PC и моделирование системы Res-Lin.
Abstract
Мы рассмотрим обобщение системы Polynomial Calculus, в котором дополнительно можно извлекать квадратный корень из многочлена и вводить новые переменные, записывающие многочлены от исходных переменных. Мы докажем экспоненциальную нижнюю оценку на размер опровержения в этой системе равенства
![$ BVP_n $](../../../sites/default/files/tex/9fbdc815bc90655f42cb9ad24c9c27fe4431369e/index.png)
(
![$ 1 + 2 x_1 + 2^2 x_2 + ... + 2^n x_n = 0 $](../../../sites/default/files/tex/b1b4967c41348c8fdb76663f55595244576d1725/index.png)
), при этом для доказательства нижней оценки на размер доказательства нам не потребуется нижняя оценка на степень. Благодаря тому, что эта система полиномиально моделирует Res-Lin (систему, оперирующую дизъюнкциями линейных уравнений; введена Разом и Цамеретом), мы получим альтернативное доказательство нижней оценки Парта и Цамерета на размер доказательств
![$ BVP_n $](../../../sites/default/files/tex/9fbdc815bc90655f42cb9ad24c9c27fe4431369e/index.png)
в Res-Lin.
Семинар будет проходить онлайн в конференции zoom. Ссылка для подключения будет выслана в рассылку за пару часов до доклада.
Видео:
https://www.youtube.com/watch?v=7TlFIncDuck