Вторник 08.10. Д.М. Ицыксон (ПОМИ): " Нижние оценки для регулярных резолюций над линейными уравнениями"

Докладчик: 
Д.М. Ицыксон (ПОМИ)
Дата: 
Tuesday, October 8, 2024 - 14:00
Место: 
Zoom
Аннотация: 

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

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

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