13.8. Примеры использования метода резолюций

Пример 13.1. Завершим рассмотрение примера 12.1 славы 12. ССФ посылок мы получили в 13.3:

y((D(y)L(a, y)&P(a), xy(Q(y))L(x, y)P(x)).

Найдем отрицание от заключения G и приведем его к ПНФ: получим:

y((D(y)Q(y)) = y(D(y)Q(y))=y(D(y)&Q(y)).

Элиминируем квантор  и получим ССФ: D(b)&Q(b).

Построим резолютивный вывод:

1. D(y)L(a, y)

2. P(a)

3. Q(y)L(x, y)P(x)

4. D(b)

5. Q(b)

6. L(x, b)P(x) {b/y}, резольвента 5, 3

7. L(a, b) {а/х}, резольвента 2, 6

8. D(b) {b/y}, резольвента 1, 7

9. □ резольвента 4,8

Пример 13.2. Посылка: «Каждый, кто хранит деньги, получает проценты». Заключение: «Если не существует процентов, то никто не хранит денег». Пусть S(х, у): «х хранит у», М(х): «х есть деньги», I(x): «x есть проценты» и Е(х, у): «х получает у». Тогда посылка записывается в виде: х(у(S(х, у)&М(у))у(I(у)&Е(х. у))), а заключение: хI(х)ху(S(х, у)М(у)).

Приведем посылку к ССФ:

х(у(S(х, у)&М(у))у(I(у)&Е(х, у))) = х(у(S(х, у)&М(у))у(I(у)&Е(х, у))) = = х(у(S(х, у)М(у))у(I(у)&Е(х, у))) = х(z(I(z)&Е(х, z)))у(S(х, у)М(у)) = = хz((I(z)&Е(х, z))у(S(х, у)М(у))) = хzу((I(z)&Е(х, z))(S(х, у)М(у))) = = хzу((S(х, у)М(у)I(f(x))&=(S(х, у)М(у)Е(x, z))).

ССФ посылки:

ху((S(х, у)М(у)I(z))&(S(х, у)М(у)Е(x, z))).

В результате получим дизъюнкты:

1. S(х, у)М(у)I(f(x),

2. S(х, у)М(у)E(x, f(x).

Возьмем отрицание от заключения и приведем к ПНФ:

(xI(x)xy(S(x, y)M(y))) =

= (xI(x)xy(S(x, y)M(y))) =

= xI(x)&xy(S (x, y)M(y))) =

= xI(x)&xy(S(x, y)&M(y)).

Поскольку полученная формула представляет собой конъюнк­цию двух формул в ПНФ. можно каждую из них приводить к ССФ отдельно: zI(z)&( S(a, b)&M(b)).

Из отрицания заключения получили дизъюнкты:

3. I(z),

4. S(a, b),

5. M(b).

Дальнейшее доказательство очень просто:

6. S(x, y)M(y) {f(x)/z}в 3, резольвента 3, 1

7. М(Ь) {а/х. b/у) в 6, резольвента 6, 4

8. □ резольвента 7. 5

Логическое следование доказано.

Пример 13.3. Посылка: «Студенты есть граждане». Заключе­ние: «Голоса студентов есть голоса граждан.» Пусть S(х): «х — студент», С(х): «х— гражданин» и V(х, у): «х есть голос у». Тогда посылка и заключение запишутся следующим образом:

у(S(у)С(у)) (посылка),

x(у(S(у)&V(х, у))z(С(z)&V(х, z)) (заключение).

Стандартная форма посылки есть у(S(у)С(у)).

Отрицание заключения приведем к ССФ:

(x(y(S(y)&V(x, y))z(C(z)&V(x, z)))) =

= (x(y(S(y)V(x, y))z(C(z)&V(x, z)))) =

= (xyz(S(y)V(x, y)(C(z)&V(x, z)))) =

= xyz(S(y)&V(x, y)&(C(z)&V(x, z))) ;

ССФ: z((S(b)&V(a, b))&(C(z)&V(a, z))),

Запишем множество дизъюнктов и построим резолютивный вывод:

1. S(у)С(у),

2. S(b),

3. V(a, b),

4. C(z)V(a, z),

5. C(b) {b/у} в 1, резольвента 1. 2

6. V(a, b) {b/z} в 4, резольвента 5, 4

7. □ резольвента 6,3.

Пример 13.4. Проверим логичность утверждения Лосева Л. Ф.:

«Вера в сущности своей и есть подлинное знание, и эти две сферы не только не разъединимы, но даже неразличимы».

Доказательство Лосева заключается в следующем.

«Верующий верит в нечто. Вера свой предмет ясно отличает от всякого другого предмета. Тогда этот предмет определен. Но если он определен, он обладает признаками, отличающими его от всякого другого. Это значит, что мы знаем этот предмет. Мы знаем вещь, если по признакам можем отличить ее от всякого другого. Следовательно, вера и есть знание».

Пусть V(х, у): «х верит в у», С(х, у): «х отличен от у», N(х, у): «хзнает у» Формализуем посылки.

1. Верующий верит в нечто.

хуV(х, у).

2. Верующий свой предмет отличает от всякого другого предмета.

ху(V(х, у)zC(y, z)).

3. Мы знаем вещь тогда, когда мы отличаем ее от всякой другой вещи.

хуz(C(y, z)N(x, y)).

4. Следовательно, вера есть знание.

ху(V(х, у)N(x, y)).

После приведения посылок и отрицания заключения к ССФ, получим множество дизъюнктов и резолютивный вывод:

1. V(х, f(х)) – х верит в предмет своей веры.

2. С(f(х), z)V(х, f(х)) – если х верит в f(х), то f(х) отличен от z.

3. N(x, f(x))С(f(х), z) – х знает f(х), если может отличить его от z.

4. V(b, у) – существует b, который верит в у.

5. N(b, у) – b не знает у.

6. С(f(b), z) – {b/х, f(b)/у} в 2 и 4, резольвента 5,3.

7. V(b, f(b)) – резольвента 6. 2.

8. □ – резольвента 1, 7.

Получаем, что вера и знание одно и то же. Это заключение вызывает сомнения, несмотря на то, что логическое следование вы­полнено. Дело в том, что посылки этого утверждения принимаются автором за истинные, однако с их истинностью можно не согласить­ся. Например, утверждение «Мы знаем вещь тогда, когда мы отличаем ее от всякой другой вещи» вызывает сомнение, осознание отличия одной вещи от другой еще не есть знание. Сомнение в истинности одной посылки приводит к тому, что и заключение вызывает сомне­ние, - ведь из противоречивой системы посылок можно вывести что угодно.

Пример 13.5. Согласно принципу Питера, служащий продвига­ется по служебной лестнице до тех пор, пока он не достигнет своего уровня некомпетентности. Следует ли из этого, что не существует компетентных начальников?

Проверим этот вывод, используя метод резолюций. Выберем предикаты: С(х): х - служащий, К(х): х - компетентный, N(x): х -начальник, Р(х): х продвигается по служебной лестнице. Формализуем свои знания о проблеме. В качестве первой посылки возьмем утверждение о том, что компетентный служащий продвигается по служебной лестнице: x(C(x)K(x)P(x)).

Второй посылкой может служить утверждение о том, что началь­ник перестает продвигаться по служебной лестнице: x(N(x)P(x)).

Учтем также тот факт, что начальник - тоже служащий: x(N(x)C(x)).

Тогда вывод, который нужно проверить, можно сформулировать так: «Все начальники некомпетентны»: x(N(x)K(x)).

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

1. N(a)

2. K(а)

3. С(x)K(x)P(x).

4. N(х)Р(х)

5. N(х)C(х)

6. С(а)Р(а) {а/х} в 3, резольвента 2, 3

7. N(а)Р(а) {а/х} в 5, резольвента 5, 6

8. N(а) {а/х} в 4, резольвента 4,7

9. □ резольвента 1, 8.

Итак, мы получили, что компетентных начальников не существует.

Пример 13.6. Рассмотрим задачу о брадобрее: В одном селе брадобрей бреет тех и только тех жителей села, которые не бреются сами. Должен ли брадобрей брить самого себя? Возьмем предикаты: P(х): х брадобрей, Q(х, у): х бреет у. Формализуем посылку и приведем ее к ССФ:

x(Р(x)&y(Q(y, у)Q(x, у))(Q(y, y)Q(x, y))).

ССФ: (P(а)&y(Q(у, у)Q(a, у))&(Q(y, у)Q(a, у))).

Проверим, бреет ли брадобрей самого себя: Q(a, a). Построим вывод:

1. P(a)

2 Q(у, у)Q(a, у)

3. Q(у, у)Q(a, у)

4. Q(у, у)

5. Q(a, a) подстановка {а/у) в 3, склейка 3

6. □ резольвента 4, 5

Логическое следование выполнено, т.е. брадобрей должен брить самого себя.

Поставим противоположный вопрос: брадобрей не должен брить самого себя: Q(a, a), и построим резолютивный вывод:

1. Р(a)

2. Q(у, у)Q(a, у)

3. Q(у, у)Q(a, у)

4. Q(a, a)

5. Q(a, a) подстановка {а/y} в 2, склейка 2

6. □ резольвента 4,5

Логическое следование также выполнено, т.е. брадобрей не должен брить самого себя.

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

Метод резолюций – это очень сильный метод поиска доказа­тельства общезначимости формул (в другой формулировке — логи­ческих следований). Именно поэтому он породил новую парадигму программирования - логическое программирование. Наиболее распространенным языком логического программирования явля­ется ПРОЛОГ. В логическом программировании любая задача ста­вится как задача доказательства логического следования некоторого предложения из заданных посылок. Выполнение программы заклю­чается в поиске доказательства методом резолюций.