Laboratory of Mathematical Logic at PDMI

Пятница, 1 марта, комната 106. Начало в 18:00.

Докладчик: Э. Гирш (совместная работа с Д.Григорьевым и Д.Пасечником).

ПОЛУАЛГЕБРАИЧЕСКИЕ ДОКАЗАТЕЛЬСТВА
Вывод пропозициональной тавтологии в полуалгебраической системе доказательств заключается в опровержении некоторой системы полиномиальных неравенств. Эти системы являются довольно сильными: в них имеются короткие доказательства принципа Дирихле, Цейтинских тавтологий, нераскрашиваемости k-клики в (k-1) цвет и т.д. Тем не менее, для наиболее слабых из полуалгебраических систем получены экспоненциальные нижние оценки на длину вывода.