Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Алгоритм унификации. Алгоритм начинает работу с пустой подстановки и шаг за шагом строит наиболее общий унификатор, если таковой суш,ествует. Предположим, что на ^-ом шаге получена подстановка Ok. Если все литералы из {Li} в результате становятся идентичными, то ^ и есть наиболее общий унификатор. В противном случае каждый из литералов в ^ рассматривается как цепочка символов и выделяется позиция первого символа, в которой не все из литералов имеют одинаковый символ. Рассмотрим пример двух литералов. Стрелками пометим позиции, где появились различные символы (при просмот­ ре слева направо): {P(a,f(a, g (z)). h(x)), P(a,f(a, и), g(w))j. k i Затем конструируется множество рассогласования JV, содержащее пра­ вильно построенные выражения из каждого литерала, которые начинаются с позиции рассогласования (правильно построенное выражение представляет со­ бой либо терм, либо литерал). Так, для рассмотренного примера множеством рассогласования будет W={g(z), и}. Далее модифицируем (если можно) подстановку Ok, чтобы устранить это рассогласование. Пусть существуют такие элементы м и ? в множестве рассо­ гласования W, что и - переменная, не входящая в элемент (терм) t. В таком слу­ чае заменяем в литералах переменную и элементом (термом) t. Если множество рассогласования W не содержит элементов с указанным свойством, то множе­ ство литералов {Li} унифицировать нельзя. Можно доказать, следующую теорему. Теорема 3.9 (теорема Робинсона). Описанный алгоритм находит наибо­ лее общий унификатор для множества унифицируемых литералов и сообщает о неудаче, если литералы неунифицируемы Рассмотрим пример. Пусть S = {Р(а, х, f(g(y))), P(z, f(z), f(u))}. Пайдем об­ щий унификатор. 1. Пустая подстановка £ . So = S - ш единичный дизъюнкт, следовательно, не получили наиболее общий унификатор. 2. Множество рассогласования равно: Wo ={а, z}, следовательно, di = £ °{a/z}, тогда 5*7 = 8$^ = {Р(а, x,f(g(y))), P(a,f(a),f(u))} и Sj-HQ единичный дизъюнкт. 3. Множество рассогласований для Sj равно: Wi = {x,f(a)}, тогда 02 = 01 ° {f(a)/x} = {a/z, f(a)/x}, и S2= = {Р(а, f(a)), f(g(y)), P(a, f(a), f(u))} и 5*2 - не единичный дизъюнкт. 75