Laboratory of Mathematical Logic at PDMI

Вторник, 16 ноября, комната 106. Начало в 18:00.

16 ноября.
Б.Ю.Конев. Доклад о патентованном алгоритме Stalmark'а установления тавтологичности пропозициональных формул. Судя по результатам машинных тестов, алгоритм является достаточно эффективным, авторы утверждают, что время его работы зависит не от количества неизвестных, а от "логической структуры формулы". Алгоритм достаточно прост, но никаких оценок для него не известно. Доклад будет сделан на основе статьи John Harrison "Stalmark's Algorithm as a HOL Derived Rule", однако, детали реализации освещаться не будут.