Laboratory of Mathematical Logic at PDMI

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

Докладчик: О. Етеревский.

УНИФИКАЦИЯ И ЕЕ ПРИЛОЖЕНИЯ К ПРОБЛЕМЕ РАЗРЕШИМОСТИ
Унификация (unification) -- это подстановка в два терма вместо переменных других термов, так чтобы получившиеся термы совпали. Естественно, это возможно не для любых двух термов. В докладе приводится алгоритм, работающий за полиномиальное время, проводящий унификацию. В алгоритме используются ориентированные графы без циклов (dag). Дается оценка на сложность задачи унификации. Из этой оценки, в свою очередь, следует оценка на сложность проблемы разрешимости для Эрбрановских формул.