Laboratory of Mathematical Logic at PDMI

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

Докладчик: А. Куликов.

Тема: Системы доказательств, использующие кэширование формул.

Abstract

Доклад по статье P.Beame, R.Impagliazzo, T.Pitassi, N.Segerlind "Memoization and DPLL: Formula Caching Proof Systems". Идея кэширования формул в алгоритме, действующем методом расщепления, заключается в том, что формулы, невыполнимость которых уже доказана, более не расщепляются (когда вновь появляются в других ветвях дерева расщепления). Как известно, метод расщепления соответствует регулярной резолюции. Таким образом, идею кэширования можно использовать и в системах доказательств, что и делается (несколькими способами) в данной статье; полученные системы доказательств сравниваются.

ТАКЖЕ МОЖНО БУДЕТ ОБСУДИТЬ ДЕНЬ И ВРЕМЯ ДАЛЬНЕЙШИХ ЗАСЕДАНИЙ.