Шаг 2. Если множество Мk состоит из одного литерала, то выдать sk в качестве наиболее общего унификатора и завершить работу. В противном случае найти множество Nk рассогласований в Mk.
Шаг 3. Если в множестве Nk существует переменная vk и терм tk, не содержащий vk, то перейти к шагу 4, иначе выдать сообщение о том, что множество М не унифицируемо и завершить работу.
Шаг 4. Положить sk+1={vk, tk}○sk, т.е. подстановка sk+1 получается из sk заменой vk на tk и, возможно, добавлением равенства vk=tk. В множестве Mk выполнить замену vk=tk, полученное множество литералов взять в качестве Mk+1.
Шаг 5. Положить k=k+1 и перейти к шагу 2.
Пусть М={P(x,f(y)), P(a,u)}. Проиллюстрируем работу алгоритиа унификации на множестве М. На первом проходе алгоритма будет найдена подстановка s1={x=a}, так как множество рассогласований N0={x,a}. Множество M1 будет равно {P(a,f(y)),P(a,u)}. На втором проходе алгоритма подстановка будет расширена до s2={x=a, u=f(y)} и M2={P(a,f(u))}. Так как M2 состоит из одного литерала, то алгоритм закончит работу и выдаст s2.
Рассмотрим второй пример. Пусть M={P(x,f(y)), P(a,b)}. На первом проходе алгоритма будет найдена подстановка s1=(x=a) и M1={P(a,f(y)), P(a,b)}. На третьем шаге второго прохода будет выдано сообщение о том, что множество М неунифицируемо, так как множество рассогласования N1={f(y),a} не содержит переменной.
Отметим, что при выполнении шага 4 из множества Mk удаляется одна из переменных (переменная vk), а новая переменная не возникает. Это означает, что алгоритм унификации всегда заканчивает работу, так как шаг 4 не может выполняться бесконечно. Довольно ясно, что если алгоритм заканчивает работу на шаге 3, то множество М неунифицируемое. Также понятно, что если алгоритм заканчивает работу на шаге 2, то sk – унификатор множества М. А вот то, что sk – наиболее общий унификатор, доказать не так то просто. Тем не менее, сделаем это.
Теорема 4.2. Пусть М – конечное непустое множество литералов. Если М унифицируемо, то алгоритм унификации заканчивает работу на шаге 2 и выдаваемая алгоритмом подстановка sk – наиболее общий унификатор множества М.
Доказательство. Пусть t – некоторый унификатор множества М. Индукцией по k докажем существование подстановки ak такой, что t=ak◦sk.
База индукции: k=0. Тогда sk=e и в качестве ak можно взять t.
Шаг индукции: Предположим, что для всех значений k, удовлетворяющих неравенству 0£k£ l, существует подстановка ak такая, что t=ak○sk.
Если sl(M) содержит один литерал, то на следующем проходе алгоритм остановится на шаге 2. Тогда sl будет наиболее общим унификатором, поскольку t=al○sl.
Пусть sl(M) содержит более одного литерала. Тогда алгоритм унификации найдет множество рассогласований Nl. Подстановка al должна унифицировать множество Nl, поскольку t=al○sl – унификатор множества М. Поскольку Nl – унифицируемое множество рассогласований, то оно содержит (хотя бы одну) переменную v.
Пусть t – терм из Nl, отличный от v. Множество Nl унифицируется подстановкой al, поэтому al(v)=al(t). Отсюда следует, что t не содержит v. Можно считать, что на шаге 4 алгоритма для получения sl+1 использовано равенство v=t, т.е. sl+1={v=t}○sl. Из равенства al(v)=al(t) следует, что al содержит равенство v=al(t).
Пусть al+1=al\{v=al(t)}. Тогда al+1(t)=al(t), так как t не содержит v. Далее, имеем равенства
al+1○{v=t}=al+1È{v=al+1(t)}=al+1È{v=al(t)}=al.
Это означает, что al=al+1○{v=t}. Следовательно,
t=al○sl=al+1○{v=t}○sl=al+1○sl+1.
Итак, для любого k существует подстановка ak такая, что t=ak○sk. Так как множество M унифицируемо, то алгоритм должен закончить работу на шаге 2. Тогда последняя подстановка sk будет унификатором множества М, поскольку множество sk(М) будет наиболее общим унификатором, так как для произвольного унификатора t существует подстановка sk такая, что t=ak○sk.
