¾3 = fa=z; f(a)=x; g(y)=ug –НОУ для E. JПример 5.16.

Множество выражений: E = fQ(f(a); g(x)); Q(y; y)g Рассмотрим вкратце попытку унифицировать эти выражения.

¾1 = ff(a)=yg; E1 = fQ(f(a); g(x)); Q(f(a); f(a))g;

E1 содержит более одного выражения; множество рассогласований D1 = fg(x); f(a)g. В D1 нет переменной, нет НОУ. Отсюда заключаем, что E не может быть унифицировано. J

Теорема 5.2 (теорема унификации) Если E – конечное непустое унифицироемое множество выражений, то алгоритм унификации всегда закончит работу на шаге 2 и последняя ¾k будет наиболее общим унификатором для E.

(Без доказательства).

5.5Метод резолюций для логики первого порядка

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

Определение. Если два или более литералов (с одинаковым знаком) клоза C имеют НОУ ¾, то C¾ называется склейкой клоза C.

Пример склейки 5.17.

Клоз C : P (x) _ P (f(y)) _ :Q(x); НОУ: ¾ = ff(y)=xg;

Пример 5.18. Если C¾ – единичный клоз, то склейка называется единичной склейкой.

З а м е ч а н и е. Клоз, содержащий m литералов называется m-литерным клозом. Однолитерный клоз называется единичным, 0-литерный – это пустой клоз 2. I

Для удобства будем рассматривать множество литералов как синоним клоза. Например, клоз P _Q_:R представляется в виде множества литералов fP; Q; :Rg.

Пусть C1; C2 – клозы (клозы-посылки), которые не имеют общих переменных. Пусть L1; L2 – литералы в C1 и C2 соответственно.

Определение. Если L1 и :L2 имеют НОУ ¾, то клоз

C = (C1¾ n L1¾) [ (C2¾ n L2¾)

называется бинарной резольвентой клозов C1 и C2.

Литералы L1; L2 называются отрезаемыми литералами.

Пример 5.19.

C1 : P (x) _ Q(x); C2 : :P (a) _ R(x).

Так как x входит в оба клоза (они имеют общую переменную), заменим переменную в C2 : :P (a) _ R(y).

L1 = P (x); L2 = :P (a).

L1 и L2 имеют НОУ: ¾ = fa=xg. Тогда

(C1¾ n L1¾) [ (C2¾ n L2¾) =

=ffP (a); Q(a)g n P (a)g [ ff:P (a); R(y)g n :P (a)g =

=fQ(a); R(y)g = Q(a) _ R(y).

Таким образом, Q(a)_R(y) – бинарная резольвента клозов C1 и C2; P (x) и :P (a) – отрезаемые литералы. J

Определение. Резольвентой клозовпосылок C1 и C2 является одна из следующих резольвент:

1.Бинарная резольвента C1 и C2.

2.Бинарная резольвента C1 и склейки C2.

3.Бинарная резольвента C2 и склейки C1.

4.Бинарная резольвента склейки C1 и склейки C2.

Пример 5.20.

C1 : P (x) _ P (f(y)) _ R(g(y));

C2 : :P (f(g(a))) _ Q(b).