Laboratory of Mathematical Logic at PDMI

Вторник, 8 октября, Zoom. Начало в 14:00.

Докладчик: Д.М. Ицыксон (ПОМИ).

Тема: Нижние оценки для регулярных резолюций над линейными уравнениями.

Abstract

Аннотация: Система доказательств резолюция над линейными уравнениями (Res(⊕)) оперирует дизъюнкциями линейных уравнений (линейными дизъюнктами) над полем GF(2); эта система расширяет обычную резолюцию с помощью линейной алгебры над полем GF(2). За последние десять лет было доказано несколько экспоненциальных нижних оценок на размер древовидных Res(⊕) опровержений. Суперполиномиальные нижние оценки на размер опровержений в системе Res(⊕) без ограничений до сих пор неизвестны.

В докладе будет рассказана экспоненциальная нижняя оценка на размер вывода в регулярной версии системы Res(⊕). Регурярная Res(⊕) --- это подсистема Res(⊕), естественным образом обобщающая регулярную резолюцию.
Это первая суперполиномиальная нижняя оценка на фрагмент системы Res(⊕), который строго сильнее древовидной Res(⊕).

Доклад основан на совместной работе с Климом Ефременко и Михалом Гарликом.