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

Рассмотрим примеры применения метода резолюций.

Пример 3.14

Ранее нами был рассмотрен силлогизм о Сократе и получена соответствующая предикатная формула:

Vx ((Н (х) —> М (х)) л //(Сократ)) —> М (Сократ).

Здесь Н — быть человеком, М — быть смертным. Требуется доказать, что эта формула общезначима. Докажем это методом опровержения: формула общезначима, если ее отрицание невыполнимо. Берем отрицание исходной формулы (Сократ обозначим через С):

Исключаем импликации, работаем с отрицаниями:

Мы получили предваренную форму в конъюнкции с М©.

Опуская квантор общности и ненужные скобки, получаем выражение, уже представленное в КНФ:

Таким образом, получается следующая система предложений:

• 1) H (x)v М (х),
• 2) Я©,
• 3) М©.

Применяя подстановку s = С/х, проводим резолюцию:

• 4) ЩС), (1,2)
• 5) Л. (3, 4)

Общезначимость исходного силлогизма доказана.

Пример 3.15

Посылка: каждый предприниматель, который занимается бизнесом, получает прибыль.

Заключение

: если прибыли нет, никто заниматься бизнесом не будет. Введем обозначение предикатных констант: S (x, у) — х ЗАНИМАЕТСЯ ДЕЛОМ у В — БИЗНЕС; Р — ПРИБЫЛЬ; Я (х, у) — х ПОЛУЧАЕТ у. Посылка запишется в следующем виде:

Если у каждого предпринимателя х есть дело у И это дело — бизнес В, то это дело приносит прибыль Р, И он ее получает (Р), а заключение — в виде.

Если никто не получает прибыль, то каким бы делом он ни занимался, это будет не бизнес.

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

После сколемизации приводим к предваренной форме:

Заметим, что квантор (после переименования) зависит только от Va). Матрицу приводим к КНФ:

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

• 1) S±x, у) v B (y)v Р (/(х)У,
• 2) (5(х, у) v й (у)) v R (x, f{x)).

Теперь займемся заключением. Надо найти его отрицание:

Матрица: P (z) л S (a, b)л В (Ь). Предложения от заключения:

• 3) Р (2).
• 4) S{a, b),
• 5) В (Ь).

Резолюции для всех предложений (1)—(5):

• 6) S (x, y) vB (y), (1,3) (s=f (x)/z),
• 7) B (b), (4, 6) (s = a/x, b/y),
• 8) Л. (5, 7).

Рассмотрим еще один пример, который пригодится нам в дальнейшем.

Пример 3.16.

Имеются следующие утверждения:

«Кто работает с интегралами, тот математик»:

1. Ух[И (х) -> М (.т)|,.

«Дети не математики»:

2. /хД (х)^>М (х).

«Некоторые дети обладают математическими способностями»:

3. Зх[Д (х)лС (х)

Требуется доказать следующее заключение:

4. 1г[С (т)лй (т)|.

«Некоторые из тех, кто имеет способности к математике, не работают с интегралами».

Первое и второе утверждения приводятся к предложениям:

• 1'. И (х) v М (х),
• 2'. Д (х)/ М (х).

В третьем утверждении проведем сколемизацию, после этого оно распадается на два однолитерных предложения:

• 3 '.Л (в>,
• 4'. С (а).

От четвертого утверждения надо взять отрицание.

Получаем последнее предложение:

5. С (х) v И (х).

С предложениями (Г)—(4') и (5) проводим резолюцию (соответствующие подстановки подразумеваются).

• 6. И (а)₉ (4', 5)
• 7. Ща), (6, Г)
• 8. Д (а), (7, 2')
• 9. Л. (8, 3').