Laboratory of Mathematical Logic at PDMI

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

Докладчик: А. Кожевников.

Доклад по статье A.Atserias, M.Bonet
ОБ АВТОМАТИЗАЦИИ МЕТОДА РЕЗОЛЮЦИЙ И СВЯЗАННЫХ С НЕЙ СИСТЕМ ДОКАЗАТЕЛЬСТВ
Создания эффективного алгоритма для доказательства тавтологичности -- одна из важнейших задач информатики. В статье описывается новый алгоритм для доказательств тавтологичности методом резолюций, основанный на системах доказательств Res(k), являющихся обобщениями метода резолюций. Доказывается, что полученный алгоритм не хуже других алгоритмов для метода резолюций, а во многих случаях экспоненциально лучше.
Также в этой статье исследуется "слабая автоматизируемость" резолюционной системы доказательств, то есть, являются ли автоматизируемыми системы, полиноминально моделирующие метод резолюций. Эта проблема сводится к вопросу о существовании интерполянтов в системе доказательств Res(2).
В качестве побочного результата построен новый класс тавтологий, имеющих короткие доказательства методом резолюций, но обладающих при этим большой "шириной". Таким образом, снимается вопрос Алехновича и Разборова об автоматизации метода резолюций за квазиполиномиальное время.
Источник: A.Atserias, M.Bonet, "On the Automatizability of Resolution and Related Propositional Proof Systems", ECCC TR02-010.