Пятница 07.04. А. Кноп: "Задача поиска и диаграммы принятия решений"
Докладчик:
А. Кноп
Дата:
Friday, April 7, 2017 - 17:15
Место:
203
Аннотация:
Классический результат Хватала и Семереди гласит, что размер древесного доказательства равен минимальному размеру дерева ищущему невыполненный клоз и аналогичное утверждение верно для регулярных резолюций и для 1-BP.
Однако подобные результаты для более сложных классов диаграмм не были известны. В докладе мы рассмотрим системы доказательств похожие на систему доказательств IPS. Доказаны результаты об эквивалентности доказательств в этих системах и задач поиска невыполненного клоза, а так же доказаны нижние и верхние оценки в данных системах.