Лаборатория алгоритмических методов

Дата:

Friday, April 7, 2017 - 17:15

Аннотация:

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

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