2.3.2 Логический вывод в логике предикатов

Пример 2.14. Рассмотрим доказательное рассуждение “Каждый человек смертен. Сократ - человек. Следовательно, Сократ смертен.”. Представим схему рассуждения:

(F1) (х) [Человек(х)  Смертен(х)];

(F2) Человек(Сократ);

(R)  Смертен(Сократ).

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

Это доказательное рассуждение, исторически одно из первых, которое было изучено с точки зрения именно формы (а не смысла), приписывается Г. Оккаму (1349 г.). В силлогистике, создателем которой был Аристотель, подобные силлогизмы стали изучаться в их общей форме с использованием замещающих переменных, которые сохраняют форму исходного силлогизма. Так, моделью приведенного рассуждения является форма: “Если все х суть у и если С есть х, то С есть у”. Заметим, что соответствие доказательства методом резолюций структуре доказательства, применяемого человеком в естественном языке, проявляется здесь еще более явно, чем в случае логики высказываний. Например, переложенное на естественный язык обоснование рассуждения: “Каждый человек смертен. Сократ - человек. Следовательно, Сократ смертен.” в соответствии с вышеприведенной схемой метода резолюции выглядит так: “Предположим противное, т.е. что Сократ не смертен. Отсюда, учитывая первое утверждение: Каждый человек смертен, можно заключить, что Сократ - не человек. Но второе утверждение говорит, что Сократ - человек. Следовательно, мы пришли к противоречию, что показывает, что наше предположение неверно.” 

Скулемовская стандартная форма

В логическом выводе используют предикаты в предваренной форме, когда все кванторы вынесены в формуле влево, т.е. предваряют формулу. Эту формулу, которая уже не содержит кванторов, можно свести к конъюнктивной нормальной форме. Преобразование в предваренную форму легко выполнить применением свойств эквивалентности и заменой переменных. Например, приведем формулу (х)P(х)(х)R(x) в предваренную форму:

(х)P(х)(х)R(x)  (х)P(х) (х)R(x)  (х) P(х)(х)R(x)  (х)[P(х)R(x)]  (х)[P(х) R(x)].

Логический вывод легко применяется в случае, если в предваренной форме представления фактов присутствует только квантор всеобщности. В логике предикатов разработан метод, позволяющие исключить квантор существования из формулы в предваренной форме. Этот метод связан с введением так называемых “скулемовских функций”. Рассмотрим этот метод, опуская обоснования, которые можно найти в [ЧЛ83].

Пусть предикат F находится в предваренной форме (Q₁x₁)…(Q_nx_n)M, где М есть предикат в конъюнктивной нормальной форме, а (Q₁x₁)…(Q_nx_n) - префикс кванторов. Пусть Q_r есть самый левый квантор существования, 1rn. Если никакой квантор всеобщности не стоит левее Q_r, то выберем новую константу с, отличную от других констант, входящих в М, заменим все вхождения x_r, встречающиеся в М, на с и вычеркнем (Q_rx_r) из префикса. Если же Q_s1…Q_sm - все кванторы всеобщности, встречающиеся левее Q_r, 1s₁<s₂<…<s_m<rn, выбираем новый m-местный функциональный символ f, отличный от всех других функциональных символов, заменим все, заменим все вхождения x_r, встречающиеся в М, на f(x_s1,x_s2,…x_sm) и вычеркнем (Q_rx_r) из префикса. Эту операцию применим для всех кванторов существования в префиксе слева направо; последняя из полученных формул есть скулемовская стандартная форма, к которой, собственно, и применяется алгоритм логического вывода. Константы и функции, использованные для замены переменных квантора существования, называются скулемовскими константами и функциями.

Пример 2.15. Построим скулемовскую стандартную форму предиката (x)(y)(z)(u)(v)(w) P(x,y,z,u,v,w).

Левее (x) в формуле нет никаких кванторов всеобщности, левее (u) стоят кванторы всеобщности (y) и (z), левее (w) стоят кванторы всеобщности (y), (z) и (v). Заменяем переменную х на константу а, переменную u на двухместную функцию f(y,z), а переменную w - на трехместную функцию g(y,z,v). Скулемовская стандартная форма представленной выше формулы - (y)(z)(v)P(а,y,z,f(y,z),v,g(y,z,v)). 

Пример 2.16. Рассмотрим следующую теорему теории групп [ЧЛ83]. Теорема (о коммутативной группе). Если произведение любого элемента группы G на себя есть единица этой группы, то группа G - коммутативна.

Очевидно, что для доказательства эта теорема должна быть записана формально. Пусть предикат Р(х,у,z) означает следующее утверждение: Если хG и уG, то zG и ху=z (мы опускаем здесь знак бинарной операции умножения группы). Тогда теорема будет выглядеть так (единицу группы обозначим е): (x) Р(х,х,е)  (u) (v) (w)[Р(u,v,w)  Р(v,u,w)].

Доказательство теорем обычно проводится на основе аксиом и других теорем, выведенных из этих аксиом. Аксиомами, определяющими любую группу G, являются следующие четыре:

А1: в группе существует единичный элемент (т.е. для любого хG хе=х и ех=х)

A2: для каждого элемента группы существует обратный элемент (если х^-1 - обратный к х, то х х^-1= х^-1 х = е).

А3: любая группа удовлетворяет свойству ассоциативности (т.е. х, у и zG влечет x(yz) = (xy)z);

Формальное выражение этих аксиом:

А1: (x)[P(е,х,x)P(х,е,x)];

A2: (у)(х)[P(x,y,e)P(y,x,e)].

A3: (x)(у)(z)(u) (v)(w) [P(x,y,u) P(y,z,v) [P(x,v,w)P(u,z,w)] ];

Для доказательства сформулированной выше теоремы В = {(x) Р(х,х,е)  (u) (v) (w)[Р(u,v,w)  Р(v,u,w)]} просто покажем, что она является логическим следствием аксиом А1-А3. Отрицание этой теоремы:

B = {(x) Р(х,х,е) & (u) (v) (w) [Р(u,v,w)  Р(v,u,w)]} =

{(x) Р(х,х,е) & (u) (v) (w) [Р(u,v,w)  Р(v,u,w)]}

Скулемовские формы для аксиом и отрицания следствия:

А1: (x)[P(e,x,x)P(x,e,x)];

A2: (у)[P(i(у),у,e)P(у,i(у),e)];

A3: (x)(у)(z)(u) (v)(w) [P(x,y,u) P(y,z,v) [P(x,v,w)P(u,z,w)] ];

B: (x){Р(х,х,е) & [Р(a,b,c)  Р(b,a,c)]}.

Список дизъюнктов для метода резолюции:

1. P(e,x,x) из А1;

2. P(x,e,x) из А1;

3. P(i(у),у,e) из А2;

4. P(у,i(у),e) из А2;

5. Р(х,х,е) из В;

6. P(x,y,u)  P(y,z,v)  P(x,v,w)  P(u,z,w) из А3;

7. P(x,y,u)  P(y,z,v)   P(u,z,w) P(x,v,w) из А3;

8. Р(a,b,c) из В;

9. Р(b,a,c) из В.



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

В процедуре доказательства методом резолюций для отождествления противоположных пар предикатов (именно предикаты выступают здесь в роли литер, если говорить в терминах метода резолюции для высказываний) используется так называемая “процедура унификации” - приведение аргументов дизъюнктов, для которых ищется резольвента, к унифицированному (одинаковому) виду. В примере 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, _k=.

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

Шаг 3. Если в D_k существует пара выражений v_k и t_k, такие, что v_k - переменная, а t_k - терм (возможно, другая переменная), не содержащий эту переменную, то положить _k+1 = _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, и _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, ₀=. Переходим к шагу 2.

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

3. Шаг 3. Множество рассогласований D₀ содержит пару (a, z), в которой z- переменная, а терм “а” эту переменную не содержит. Полагаем ₁ =₀{а/z}={а/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(а)” эту переменную не содержит. Полагаем ₂ = ₁{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)” эту переменную не содержит. Полагаем ₃ = ₂{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))} - это подстановка ₃ = {а/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 группы (для каждого элемента группы существует обратный элемент).