Перейдем к логике первого порядка. Относительно переменных в дизъюнктах будем предполагать, что они связаны кванторами общности, но сами кванторы писать не будем. Отсюда следует, что две одинаковые переменные в разных дизъюнктах можно считать различными.

Заметим, прежде всего, что в логике первого порядка правило резолюций в прежнем виде уже не годится. Действительно, множество дизъюнктов S={P(x),ØP(a)} невыполнимо, (так как предполагается, что переменная х связана квантором общности). В то же время, если использовать правило резолюций для логики высказываний, то из S пустого дизъюнкта не получить. Содержательно понятно, что в этом случае надо сделать. Поскольку дизъюнкт P(x) можно прочитать так: для любого х истинно P(x), то P(x) истинно будет и для x=a. Сделав подстановку х=а, получим множество дизъюнктов S^/={P(a),ØP(a)}. Множество S и S^/ одновременно выполнимы (или невыполнимы). Но из S^/ с помощью прежнего правила резолюций выводится тривиальным образом. Этот пример подсказывает, что в логике первого порядка правило резолюций надо дополнить возможностью делать подстановку.

Дадим необходимые определения.

Определение. Подстановкой называется множество равенств

s={x₁=t₁, x₂=t₂,…, x_n=t_n},

где x₁,x₂,…,x_n – различные переменные, t₁,t₂,…,t_n – термы, причем терм t_i не содержит переменной x_i (1£ i £ n).

Если s = (x₁=t₁,...,x_n=t_n) – подстановка, а F – дизъюнкт, то через s(F) будем обозначать дизъюнкт, полученный из F одновременной заменой x₁ на t1; и т.д. x_n на t_n. Например, если s={x₁=f(x₂), x₂=c, x₃=g(x₄)), F=R(x₁,x₂,x₃)ÚØP(f(x₂)), то s(F)=R(f(x₂), c, g(x₄))ÚØP(f(c). Аналогично определяется действие подстановки на терм.

Для удобства введем еще и пустую подстановку – подстановку, не содержащую равенств. Пустую подстановку будем обозначать через e.

Определение. Пусть {E₁,…,E_k} – множество литералов или множество термов. Подстановка s называется унификатором этого множества, если s(E₁)=s(E₂)=…=s(E_k). Множество унифицируемо, если существует унификатор этого множества.

Например, множество атомарных формул

{Q(a,x,f(x)), Q(u,у,z)}

унифицируемо подстановкой {u=a, x=у,z=f(у)}, а множество

{R(x,f(x)), R(u,u)}

неунифицируемо. Действительно, если заменить х на u, то получим множество

{R(u,f(u), R(u,u)}.

Проводить же замену u=f(u) запрещено определением подстановки, да и бесполезно, т.к. она приводит к формулам R(f(u), f(f(u))) и R(f(u), f(u)), которые тоже различны.

Если множество унифицируемо, то существует, как правило, не один унификатор этого множества, а несколько. Среди всех унификаторов данного множества выделяют так называемый наиболее общий унификатор.

Дадим необходимые определения.

Определение. Пусть x={x₁=t₁, x₂=t₂,…, x_k=t_k} и h={y₁=s₁, y₂=s₂,…, y_l=s_l} – две подстановки. Тогда произведением подстановок x и h называется подстановка, которая получается из последовательности равенств

{x₁=h(t₁), x₂=h(t₂),…,x_k=h(t_k), y₁=s₁, y₂=s₂,…, y_l=s_l}                       (4)

вычеркиванием равенств вида x_i=x_i для 1£ i£ k, y_j=s_j, если y_jÎ{x₁,…, x_k}, для 1 £ j £ l.

Для обозначения результата действия подстановки на дизъюнкт мы применяем префиксную функциональную запись, поэтому произведение подстановок x и h будем обозначать через h◦x, подчеркивая тем самым, что сначала действует x, а потом h.

Рассмотрим пример. Пусть x = {x=f(y), z=y, u=g(d)}, h = {x=c, y=z}. Тогда последовательность равенств (4) из определения произведения имеет вид

{x=f(y), z=z, u=g(d), x=c, y=z}.

В этой последовательности вычеркнем второе и четвертое равенство получим произведение

h◦x = {x=f(y), u=g(d), y=z}.

Нетрудно показать, что произведение подстановок ассоциативно, т.е. для любых подстановок x,h,x выполняется равенство x◦(h◦z)=(x◦h)◦z, и что пустая подстановка является нейтральным элементом относительно умножения. Последнее означает выполнение равенств s◦e=e◦s=s для любой подстановки s.

Произведение подстановок s = {x₁=t₁}○{x₂=t₂}○…○{x_n=t_n} мы будем иногда задавать последовательностью равенств: s = (x₁=t₁, x₂=t₂,…, x_n=t_n). Действие подстановки &s на дизъюнкт (и на терм) в этом случае состоит в последовательной (а не одновременной) замене x₁ на t₁, x₂на t₂, и т.д., x_n на t_n.

Определение. Унификатор s множества литералов или термов называется наиболее общим унификатором этого множества, если для любого унификатора t того же множества литералов существует подстановка x такая, что t=x○s.

Например, для множества {P(x,f(а), g(z)), P(f(b),y,v)} наиболее общим унификатором является подстановка s={x=f(b), y=f(a), v=g(z)}. Если в качестве t взять унификатор {x=f(b), y=f(a), z=c, v=g(c)}, то x={z=c}.

Если множество литералов унифицируемо, то наиболее общий унификатор существует. Это утверждение мы докажем в конце параграфа. А сейчас приведем алгоритм нахождения наиболее общего унификатора. Алгоритм называется алгоритмом унификации. Для изложения алгоритма потребуется понятие множества рассогласований.

Определение. Пусть М – множество литералов или термов. Выделим первую слева позицию, в к торой не для всех литералов стоит один и тот же символ. Затем в каждом литерале выпишем выражение, которое начинается символом, занимающим эту позицию. (Этими выражениями могут быть сам литерал, атомарная формула или терм). Множество полученных выражений называется множеством рассогласований в М.

Например, если M={P(x, f(y), a), P(x,u, g(y)), P(x, c, v)}, то первая слева позиция, в которой не все литералы имеют один и тот же символ – пятая позиция. Множество рассогласований состоит из термов f(y), u, c. Множество рассогласований {P(x, y), ØP(a, g(z))} есть само множество. Если M={ØP(x, y),ØQ(a, v)}, то множество рассогласований равно {P(x, y), Q(a, v)}.

Алгоритм унификации

Шаг 1. Положить k=0, M_k=M, s_k=e.

Шаг 2. Если множество М_k состоит из одного литерала, то выдать s_k в качестве наиболее общего унификатора и завершить работу. В противном случае найти множество N_k рассогласований в M_k.

Шаг 3. Если в множестве N_k существует переменная v_k и терм t_k, не содержащий v_k, то перейти к шагу 4, иначе выдать сообщение о том, что множество М неунифицируемо и завершить работу.

Шаг 4. Положить s_k+1={v_k, t_k}○s_k, т.е. подстановка s_k+1 получается из s_k заменой v_k на t_k и, возможно, добавлением равенства v_k=t_k. В множестве M_k выполнить замену v_k=t_k, полученное множество литералов взять в качестве M_k+1.

Шаг 5. Положить k=k+1 и перейти к шагу 2.

Пусть М={P(x,f(y)), P(a,u)}. Проиллюстрируем работу алгоритиа унификации на множестве М. На первом проходе алгоритма будет найдена подстановка s₁={x=a}, так как множество рассогласований N₀={x,a}. Множество M₁ будет равно {P(a,f(y)),P(a,u)}. На втором проходе алгоритма подстановка будет расширена до s₂={x=a, u=f(y)} и M₂={P(a,f(u))}. Так как M₂ состоит из одного литерала, то алгоритм закончит работу и выдаст s₂.

Рассмотрим второй пример. Пусть M={P(x,f(y)), P(a,b)}. На первом проходе алгоритма будет найдена подстановка s₁=(x=a) и M₁={P(a,f(y)), P(a,b)}. На третьем шаге второго прохода будет выдано сообщение о том, что множество М неунифицируемо, так как множество рассогласования N₁={f(y),a} не содержит переменной.

Отметим, что при выполнении шага 4 из множества M_k удаляется одна из переменных (переменная v_k), а новая переменная не возникает. Это означает, что алгоритм унификации всегда заканчивает работу, так как шаг 4 не может выполняться бесконечно. Довольно ясно, что если алгоритм заканчивает работу на шаге 3, то множество М неунифицируемое. Также понятно, что если алгоритм заканчивает работу на шаге 2, то s_k – унификатор множества М. А вот то, что s_k – наиболее общий унификатор, доказать не так то просто. Тем не менее, сделаем это.

Теорема 4.2. Пусть М – конечное непустое множество литералов. Если М унифицируемо, то алгоритм унификации заканчивает работу на шаге 2 и выдаваемая алгоритмом подстановка s_k – наиболее общий унификатор множества М.

Доказательство. Пусть t – некоторый унификатор множества М. Индукцией по k докажем существование подстановки a_k такой, что t=a_k◦s_k.

База индукции: k=0. Тогда s_k=e и в качестве a_k можно взять t.

Шаг индукции: Предположим, что для всех значений k, удовлетворяющих неравенству 0£k£ l, существует подстановка a_k такая, что t=a_k○s_k.

Если s_l(M) содержит один литерал, то на следующем проходе алгоритм остановится на шаге 2. Тогда s_l будет наиболее общим унификатором, поскольку t=a_l○s_l.

Пусть s_l(M) содержит более одного литерала. Тогда алгоритм унификации найдет множество рассогласований N_l. Подстановка a_l должна унифицировать множество N_l, поскольку t=a_l○s_l – унификатор множества М. Поскольку N_l – унифицируемое множество рассогласований, то оно содержит (хотя бы одну) переменную v.

Пусть t – терм из N_l, отличный от v. Множество N_l унифицируется подстановкой a_l, поэтому a_l(v)=a_l(t). Отсюда следует, что t не содержит v. Можно считать, что на шаге 4 алгоритма для получения s_l+1 использовано равенство v=t, т.е. s_l+1={v=t}○s_l. Из равенства a_l(v)=a_l(t) следует, что a_l содержит равенство v=a_l(t).

Пусть a_l+1=a_l\{v=a_l(t)}. Тогда a_l+1(t)=a_l(t), так как t не содержит v. Далее, имеем равенства

a_l+1○{v=t}=a_l+1È{v=a_l+1(t)}=a_l+1È{v=a_l(t)}=a_l.

Это означает, что a_l=a_l+1○{v=t}. Следовательно,

t=a_l○s_l=a_l+1○{v=t}○s_l=a_l+1○s_l+1.

Итак, для любого k существует подстановка a_k такая, что t=a_k○s_k. Так как множество M унифицируемо, то алгоритм должен закончить работу на шаге 2. Тогда последняя подстановка s_k будет унификатором множества М, поскольку множество s_k(М) будет наиболее общим унификатором, так как для произвольного унификатора t существует подстановка s_k такая, что t=a_k○s_k.

Теорема доказана.