Laboratory of Mathematical Logic at PDMI

Пятница, 7 апреля, 203. Начало в 17:15.

Докладчик: А. Кноп.

Тема: Задача поиска и диаграммы принятия решений.

Abstract

Классический результат Хватала и Семереди гласит, что размер древесного доказательства равен минимальному размеру дерева ищущему невыполненный клоз и аналогичное утверждение верно для регулярных резолюций и для 1-BP.

Однако подобные результаты для более сложных классов диаграмм не были известны. В докладе мы рассмотрим системы доказательств похожие на систему доказательств IPS. Доказаны результаты об эквивалентности доказательств в этих системах и задач поиска невыполненного клоза, а так же доказаны нижние и верхние оценки в данных системах.