В главе 5 был изложен принцип резолюций для исчисления высказываний, где нахождение контрарных пар не вызывало трудностей. Для логики предикатов это не так. Действительно, пусть имеются дизъюнкты типа
C1: P(x) ÚØR(x),
C2: ØP(g(x)) ÚQ(y),
то резольвента может быть получена только после применения к C1 подстановки g(x) вместо x. После такой подстановки получим:
C1': P(g(x)) ÚØR(g(x)),
C2': ØP(g(x)) Ú Q(y),
резольвента C = ØR(g(x)) Ú Q(y). Однако для случая
C1: P(f(x)) ÚØR(x),
C2: ØP(g(x)) Ú Q(y),
никакая подстановка неприменима и никакая резольвента не образуется. Отсюда следует определение подстановки.
Подстановкой называется конечное множество вида {t1/x1, t2/x2, …, tn/xn}, где любой ti – терм, а любая xi – переменная (1£ i £ n), отличная от ti.
Пусть Q = {t1/x1, t2/x2, …, tn/xn} – подстановка, а W – выражение. Тогда WQ называется примером выражения W, полученным заменой всех вхождений в W переменной xi (1£ i £ n) на вхождение терма ti.
Пусть Q = {t1/x1, t2/x2, …, tn/xn} и l = {u1/y1, u2/y2, …, um/ym} – две подстановки. Тогда композицией Q ° l двух подстановок Q и l называется подстановка, состоящая из множества {t1l/x1, t2l/x2, …, tnl/xn, u1/y1, u2/y2, …, um/ym }, в котором вычеркиваются til/xi в случае til = xi и ui/yi , если yi находится среди x1, x2, …, xn.
Подстановка Q называется унификатором для множества выражений {W1, W2, …, Wk}, если W1Q = W2Q = … = WkQ. Говорят, что множество выражений {W1, W2, …, Wk} унифицируемо, если для него имеется унификатор.
Унификатор s для множества выражений {W1, W2, …, Wk} называется наиболее общим унификатором (НОУ) тогда и только тогда, когда для каждого унификатора Q для этого множества выражений найдется подстановка l такая, что Q = s ° l.
Пример.Пусть W = {P(x, a, f(g(a))), P(z, y, f(u)}. Тогда s = {z/x, a/y, g(a)/u} есть НОУ, а Q = {b/x, a/y, b/z, g(a)/u} есть унификатор.
Существует алгоритм унификации, который позволяет находить НОУ, если множество выражений W унифицируемо.
1. Установить k = 0, Wk = W, sk = e.
2. Если Wk не является одноэлементным множеством, то перейти к п. 3, в противном случае положить s = sk и окончить работу алгоритма.
3. Каждая из литер в Wk рассматривается как цепочка символов и выделяются первые подвыражения литер, не являющихся одинаковыми у всех элементов Wk, т. е. образуется так называемое множество рассогласований типа {xk, tk}. Если в этом множестве xk – переменная, а tk – терм, отличный от xk, то перейти к п.4, в противном случае множество W неунифицируемо.
4. Пусть sk+1 = sk°{tk/xk} и Wk+1 = Wk {tk/xk}.
5. Установить k = k+1 и перейти к п. 2.
Пример.Найти НОУ для W = {P(y, g(z), f(x)), P(a, x, f(g(y)))}.
1. so = e, Wo = W.
2. Так как Wo не является одноэлементным множеством, то составить множество рассогласований {y, a} и подстановку {a/y}.
3. Найти унификатор s1 = so°{a/y} = e°{a/y} = {a/y} и W1 = Wo{a/y} = {P(a, g(z), f(x)), P(a, x, f(g(a)))}.
4. Так как W1 опять неодноэлементно, то множество рассогласований будет {g(z), x}, т. е. { g(z)/x }.
5. s2 = s1°{g(z)/x} = {a/y, g(z)/x}, W2 = W1{g(z)/x} = {P(a, g(z), f(g(z))), P(a, g(z), f(g(a)))}.
6. Множество рассогласований {z, a}, т. е. {a/z}.
7. s3 = s2°{a/z} = {a/y, g(a)/x, a/z}, W3 = W2{a/z} = {P(a, g(a), f(g(a))), P(a, g(a), f(g(a)))} ={P(a, g(a), f(g(a)))}, s3 есть НОУ для W.
Если две или более одинаковые литеры (одного и того же знака) дизъюнкта С имеют НОУ s, то Сs называется фактором дизъюнкта С. Пусть С1 и С2 – два дизъюнкта, не имеющие общих переменных и пусть L1 и L2 = ØL1 – литеры в дизъюнктах С1 и С2 соответственно, имеющие НОУ s. Тогда бинарной резольвентой для С1 и С2 является дизъюнкт вида С = (С1s - L1s)È(С2s - L2s). Бинарная резольвента может быть получена одним из четырех способов:
1) резольвента для С1 и С2;
2) резольвента для С1 и фактора дизъюнкта С2;
3) резольвента для фактора дизъюнкта С1 и С2;
4) резольвента для фактора дизъюнкта С1 и фактора дизъюнкта С2.
Пример.Пусть С1 = P(f(g(a)))Ú ØR(b), С2 = ØP(x) Ú ØP(f(y)) ÚQ(y).
Тогда С2s = С2¢ = ØP(f(y)) Ú Q(y) и резольвентой для С1 и С2¢ будет C = ØR(b) ÚQ(g(a)).
Принцип резолюций обладает важным свойством – полнотой, которое устанавливается теоремой Робинсона: множество дизъюнктов S невыполнимо тогда и только тогда, когда существует вывод из S пустого дизъюнкта.
Однако в силу неразрешимости логики предикатов для выполнимого множества дизъюнктов процедура, основанная на принципе резолюций, будет работать бесконечно долго.
Пример. Рассмотрим следующие утверждения:
1. Существуют студенты, которые любят всех преподавателей.
2. Ни один из студентов не любит невежд.
3. Следовательно, ни один из преподавателей не является невеждой.
На языке логики предикатов эти утверждения имеют вид:
$x(C(x)Ù"y(P(y)®L(x,y)))
"x(C(x)®"y(H(y)®ØL(x,y)))
"y(P(y) ® ØH(y))
Применим принцип резолюций.
1. С(a).
2. Ø P(y)ÚL(a, y).
3. Ø C(x) ÚØH(y) ÚØ L(x,y).
Ø"y(Ø P(y)Ú ØH(y)) = $y(P(y) Ù H(y)).
4. P(b).
5. H(b).
6. L(a, b) (2, 4). s = {b/y}.
7. ØH(y) ÚØ L(a,y) (1, 3). s = {a/x}.
8. Ø L(a,b) (5, 7). s = {b/y}.
9. ÿ(6, 8).
Принцип резолюций является более эффективной процедурой вывода, чем процедура Эрбрана. Но и он имеет существенный недостаток, заключающийся в формировании всевозможных резольвент, большинство из которых оказывается излишними и ненужными. С 1965 г. и по сей день появляются всевозможные модификации принципа резолюций, направленные на нахождение более эффективных стратегий поиска нужных дизъюнктов. Однако подробное рассмотрение этих модификаций выходит за рамки данного учебного пособия.