Ф. Парт (АФТУ)
Параметризованные системы доказательств

Вопрос о равенстве классов co-NP и NP имеет естественную переформулировку в терминах систем доказательств и сложности доказательств. Аналогично, те или иные классы задач с параметром W[t] могут быть отделены от соответствующих им co-классов посредством исследования параметризованных систем доказательств и оценке снизу размера доказательств в таких системах. В докладе будет рассмотрена параметризованная версия tree-like резолюций для задачи ограниченной невыполнимости и приведена классификация (модифицированная теорема Риса) длины доказательств в этой системе для семейств параметризованных противоречий, являющихся записями для конечных моделей формулы логики первого порядка, не имеющей конечных моделей.