Laboratory of Mathematical Logic at PDMI

Пятница, 23 марта, комната 106. Начало в 17:00.

Докладчик: Б. Ю. Конев.

REDUCTION RULES AND UNIVERSAL VARIABLES FOR FIRST ORDER TABLEAUX AND DPLL
Упрощающие правила (редукции) играют большую роль в автоматическом поиске вывода. Хорошо известна их роль в пропозициональной логике; для логики первого порядка упрощающие правила применяются в основном для резолюционного исчисления. Используемые в исчислениях секвенциального типа "жесткие" переменные затрудняют применение упрощающих правил. Предлагается вариант редукций для секвенциальных исчислений первого порядка, вводимых благодаря "универсальным" переменным и правилу переименования.
Доклад подготовлен по одноименной статье Fabio Massacci.