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