Понедельник 02.06. Дмитрий Ицыксон: "Резолюция по линейным комбинациям: обзор последних достижений"
PDMI seminars
Тема: Резолюция по линейным комбинациям: обзор последних достижений
Место: ПОМИ, 311
Время: 02.06.2025, 18:00
Докладчик: Дмитрий Ицыксон
Abstract:
Мы рассмотрим систему доказательств резолюция по линейным комбинациям (Res(⊕)), в которой невыполнимость формулы доказывается посредством анализа четности суммы нескольких переменных — то есть с помощью разбора случаев. Основная открытая задача состоит в том, чтобы показать существование формул, для которых в данной системе невозможно получить короткое (полиномиальное) опровержение, то есть выявить трудные для Res(⊕) формулы. Долгое время трудные формулы были известны только для древовидного варианта системы, в котором разные рассматриваемые случаи нельзя анализировать одновременно. За последние два–три года были достигнуты значительные успехи в изучении более общего варианта системы, позволяющего вести разбор разных случаев одновременно. В докладе мы обсудим эти результаты.