Laboratory of Mathematical Logic at PDMI

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

Докладчик: Г. В. Давыдов, И. М. Давыдова.

"О вычислении формул сечения при поиске вывода в исчислении предикатов"
Правило резолюций в методе резолюций Робинсона и правило Б в обратном методе Маслова являются правилами сечения по контрарной паре в первом случае и по исходной "clause" во втором. Выводом исходной формулы является вывод пустого объекта по этим правилам. В докладе предлагается, наоборот, по исходной формуле строить формулу сечения таким образом, что устранение сечения приводит к реконструкции исходных контрарных пар и исходных "clauses". Построенная формула сечения оказывается исходной для следующего шага. Последовательность формул сечения, оканчивающаяся пропозиционально выводимой формулой, является выводом исходной формулы.