Математическая логика и теория алгоритмов

таковой существует. Предположим, что на к-ы шаге получена подста­ новка 0^. Если все литералы из [L] в результате становятся идентич­ ными, то 0 = 0i и есть наиболее общий унификатор. В противном слу­ чае каждый из литералов в рассматривается как цепочка символов и выделяется позиция первого символа, в которой не все из литералов имеют одинаковый символ. Рассмотрим пример двух лите­ ралов. Стрелками пометим позиции, где появились различные симво­ лы (при просмотре слева направо): {Р{а, j{a, g(z)), /г(х)), P{a,j{a, и), g(w))} , t • * Затем конструируется множество рассогласования W, содержа­ щее правильно построенные выражения из каждого литерала, которые начинаются с позиции рассогласования (правильно построенное выражение представляет собой либо терм, либо литерал). Так, для рассмотренного примера множеством рассогласования будет W = {g(z), и}. Далее модифицируем (если можно) подстановку 6^, чтобы уст­ ранить это рассогласование. Пусть существуют такие элементы и и t в множестве рассогласования W, что и - переменная, не входящая в элемент (терм) t. В таком случае заменяем в литералах перемен­ ную и элементом (термом) f из W. Если множество рассогласования W не содержит элементов с указанным свойством, то множество литера­ лов {Li} унифицировать нельзя. Можно доказать, следующую теорему. Теорема 3.9 (теорема Робинсона). Описанный алгоритм нахо­ дит наиболее общий унификатор для множества унифицируемых литерагюв и сообщает о неудаче, если литералы неунифицируемы. Рассмотрим пример. Пусть S = {Р{а, х, J{g(yy)), P{z, f{z), fiu))}. Найдем общий унификатор. 109