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

В процедуре доказательства методом резолюций для отождествления противоположных пар предикатов (именно предикаты выступают здесь в роли литер, если говорить в терминах метода резолюции для высказываний) используется так называемая “процедура унификации” - приведение аргументов дизъюнктов, для которых ищется резольвента, к унифицированному (одинаковому) виду. В примере 2.14 при поиске резольвенты двух дизъюнктов ØЧеловек(х)ÚСмертен(х) и Человек(Сократ) вместо переменной х можно подставить конкретное значение “Сократ” именно потому, что квантор всеобщности предваряет первый дизъюнкт: поскольку это высказывание истинно для любого элемента предметной области (множества людей), то оно справедливо и для конкретного человека по имени Сократ.

Рассмотрим алгоритм унификации конечного множества выражений (см. [ЧЛ83]). Алгоритм унификации пытается найти такие наиболее общие замены переменных в выражениях, чтобы эти выражения стали тождественны. Например, чтобы два выражения Р(х) и Р(а) стали тождественны, необходимо просто переменную х заменить на константу а. Обобщим этот примитивный случай: построим алгоритм, который находит минимальную подстановку переменных всегда, когда она есть. Формализуем простейший случай. Чтобы отождествить Р(а) и Р(х) сначала найдем рассогласование выражений, которое равно {а, х}, а потом попытаемся его исключить конкретизацией переменных. В общем случае рассогласование множества выражений W строится выявлением первой слева позиции, на которой не для всех выражений из W стоит один и тот же символ. Далее с этой позиции из каждого выражения в W выделяются подвыражения, совокупность которых и составляет множество рассогласований. Например, если W есть {P(x, f(y, z)), P(x, a), P(x, g(h(x)))}, то первая позиция рассогласования есть пятая, поскольку у всех выражений четыре первые символа “Р(х,” совпадают. Начинающиеся с пятой позиции подвыражения подчеркнуты; они и составляют множество рассогласований: {f(y, z), a, g(h(x))}.

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

Шаг 1. Полагаем k=0, W_k=W, s_k=e.

Шаг 2. Если W_k - содержит только один дизъюнкт, то останов, W - унифицируемо и s_k -наиболее общий унификатор для W. Если нет, найдем D_k - множество рассогласований для W_k.

Шаг 3. Если в D_k существует пара выражений v_k и t_k, такие, что v_k - переменная, а t_k - терм (возможно, другая переменная), не содержащий эту переменную, то положить s_k+1 = s_k·{t_k/v_k}, W_k+1 = W_k{t_k/v_k}, k=k+1 и перейти к шагу 2.

В противном случае останов: множество W не унифицируемо.

В этом алгоритме используются обозначения W_k{t_k/v_k}, что означает подстановку терма t_k вместо всех вхождений переменной v_k, и s_k·{t_k/v_k}, что означает произведение подстановок с очевидным смыслом. Рассмотрим работу алгоритма на примерах.

Пример 2.17 (а). Наиболее общий унификатор для W={P(x, f(х)), P(z, f(z)}, очевидно, {x/z} (или, {z/x}). После замены переменных W₁={P(x, f(х)), P(х, f(х)}={P(x, f(х))}, содержит только один член - единичный дизъюнкт. Таким образом, замена переменных при резолюции является частным случаем унификации.ÿ

Пример 2.17(б). Найдем наиболее общий унификатор для W={P(a, x, f(g(y))), P(z, f(z), f(u))}.

1. Шаг 1. k=0, W₀=W, s₀=e. Переходим к шагу 2.

2. Шаг 2. W₀ не является единичным дизъюнктом. D₀ = {a, z}. Переходим к шагу 3.

3. Шаг 3. Множество рассогласований D₀ содержит пару (a, z), в которой z- переменная, а терм “а” эту переменную не содержит. Полагаем s₁ =s₀·{а/z}=e·{а/z}={а/z}. W₁=W₀·{а/z} = {P(a, x, f(g(y))), P(a, f(а), f(u))}, k=1.

4. Шаг 2. W₁ не является единичным дизъюнктом. D₁ = {х, f(а)}. Переходим к шагу 3.

5. Шаг 3. Множество рассогласований D₁ содержит пару (х, f(а)), в которой х - переменная, а терм “f(а)” эту переменную не содержит. Полагаем s₂ = s₁·{f(а)/х} = {а/z}·{f(а)/х} = {а/z, f(а)/х}. W₂ = W₁{f(а)/х} = {P(a, f(а), f(g(y))), P(a, f(а), f(u))}, k=2.

6. Шаг 2. W₂ не является единичным дизъюнктом. D₂ = {g(y), u}. Переходим к шагу 3.

7. Шаг 3. Множество рассогласований D₂ содержит пару (g(y), u), в которой u- переменная, а терм “g(y)” эту переменную не содержит. Полагаем s₃ = s₂{g(y)/u} = {а/z, f(а)/х}{g(y)/u} = {а/z, f(а)/х, g(y)/u}. W₃ = W₂{g(y)/u} = {P(a, f(а), f(g(y))), P(a, f(а), f(g(y)))} = {P(a, f(а), f(g(y)))}, k=3.

8. Шаг 2. W₃ содержит только единичный дизъюнкт. Алгоритм завершился. Наиболее общий унификатор для W = {P(a, x, f(g(y))), P(z, f(z), f(u))} - это подстановка s₃ = {а/z, f(а)/х, g(y)/u}, т.е. нужно везде подставить вместо z константу а, вместо х - функцию f(а), а вместо u - функцию g(y).ÿ

Пример 2.18. Докажем справедливость следующего рассуждения [ЧЛ83].

Посылки:

F1:: Некоторые пациенты любят докторов.

F2:: Ни один пациент не любит знахарей.

Заключение:

R:: Никакой доктор не является знахарем.

Выделим элементарные высказывания:

Р(х): “х-пациент”;

D(х): “х-доктор”;

Z(х): “х-знахарь”;

L(x,y): “x любит у”.

Предикатная запись рассуждения:

F1:: ($x: P(x))("y: D(y)) L(x,y), Некоторые пациенты любят (всех) докторов.

F2:: ("x: P(x))("y: Z(y) )ØL(x,y), Ни один пациент не любит (всех) знахарей.

Это же можно записать и так: F2:: Ø ($x: P(x))( $y: Z(y) )L(x,y),

R:: ("x: D(x))ØZ(x); Никакой доктор не является знахарем.

Это же можно записать и так: R:: Ø ($x: D(x)) Q(x);

Раскрытие ограниченных предикатов:

F1:: ($x)[P(x)&("y)(D(y)ÞL(x,y))],

F2:: ("x)[P(x) Þ("y)(Z(y) ÞØL(x,y))],

R:: ("x)(D(x)ÞØZ(x));

Отрицание заключения:

ØR:: ($x)Ø(ØD(x)ÚØZ(x)).

Представление посылок и отрицания заключения в предваренной конъюнктивной нормальной форме:

F1:: ($x)("y)[P(x)&(ØD(y)ÚL(x,y))],

F2:: ("x)("y)(ØP(x)ÚØZ(y)ÚØL(x,y)),

ØR:: ($x)D(x)&Z(x).

Представление посылок и отрицания заключения в скулемовской нормальной форме:

F1:: ("y)(P(а)&(ØD(y)ÚL(а,y)),

F2:: ("x)("у)(ØP(x)ÚØZ(у)ÚØL(x,у)),

ØR:: D(b)&Z(b).

Замена переменных:

F1:: ("y)(P(а)&(ØD(y)ÚL(а,y)),

F2:: ("x)("z)(ØP(x)ÚØZ(z)ÚØL(x,z)),

ØR:: D(b)&Z(b).

Здесь произведена замена переменных, связанных квантором всеобщности: в F2 переменная у заменена на z с тем, чтобы не было коллизий с утверждением F1. Алгоритм унификации позволит автоматически произвести необходимую замену переменных при поиске резольвенты. Если этого не сделать, то могут возникнуть коллизии: как, например, унифицировать два предиката Р(х, f(z)) и Р(z, f(x)) из различных дизъюнктов?

Дизъюнкты для доказательства методом резолюции:

(1) Р(а)

(2) ØD(y)ÚL(а,y)

(3) ØP(x)ÚØZ(z)ÚØL(x,z)

(4) D(b)

(5) Z(b)).

Резольвенты:

(6) L(а,b) резольвента (4) и (2)

(7) ØP(а)ÚØZ(b) резольвента (6) и (3)

(8) ØQ(b) резольвента (7) и (1)

(9) ð резольвента (8) и (5) - пустая

Восстановим словесную форму доказательства.

Посылки:

F1:: Некоторые пациенты любят докторов.

F2:: Ни один пациент не любит знахарей.

Заключение:

R:: Следовательно, никакой доктор не является знахарем.

Доказательство.

Предположим противное, т.е. что существует некий доктор, одновременно являющийся и знахарем. Пусть этот человек b (Отрицание следствия, D(b)&Z(b)). Тогда из утверждения (F1:: Некоторые пациенты любят (всех) докторов)следует, что существует пациент (назовем его а), который любит всех докторов, и, конечно, любит конкретного доктора b (L(а,b)). Отсюда и из второго утверждения (F2:: Ни один пациент не любит знахарей) следует, что или а не пациент, или b не доктор (ØP(а)ÚØZ(b)). Но из утверждения F1 мы знаем, что а - пациент, а из отрицания заключения(ØR) по предположению, b -доктор. Таким образом, мы пришли к противоречию, и, следовательно, заключение нашего рассуждения верно.ÿ

Пример 2.16 (продолжение). Докажем теперь теорему о коммутативной группе формально. Для этого нужно просто показать существование пустой резольвенты для множества дизъюнктов Д1-Д9 примера 2.16.

Отметим еще раз, что при нахождении резольвенты двух дизъюнктов, включающих переменные, связанные кванторами всеобщности, эти переменные в разных дизъюнктах не должны совпадать: в каждом дизъюнкте они связаны квантором всеобщности, и "не видны" извне. Поэтому все переменные одного дизъюнкта при применении метода резолюции нужно переименовать так, чтобы они отличались от переменных других дизъюнктов. Эта операция переименования называется разделением переменных. Для данного примера запишем список дизъюнктов после разделения переменных:

Д1: P(e,x1,x1);

Д2: P(x2,e,x2);

Д3: P(i(у1),у1,e);

Д4: P(у2,i(у2),e);

Д5: Р(х3,х3,е);

Д6: ØP(x4,y4,u4) Ú ØP(y4,z4,v4) Ú ØP(x4,v4,w4) Ú P(u4,z4,w4);

Д7: ØP(x5,y5,u5) Ú ØP(y5,z5,v5) Ú Ø P(u5,z5,w5) ÚP(x5,v5,w5);

Д8: Р(a,b,c);

Д9:ØР(b,a,c).

Резольвенты и порождающие их дизъюнкты, построенные при доказательстве теоремы, представлены таблицей:

Заметим, что при доказательстве вовсе не использовалось свойство A2 группы (для каждого элемента группы существует обратный элемент).