4.3.Правило резолюции для исчисления высказываний

Пусть С₁ и С₂ – предложения в исчислении высказываний.

Пусть , , где Р – пропозициональная переменная, - любые предложения.

Правило вывода называется правилом резолюции, где

С₁, С₂ - родительские предложения,

- резольвента,

- контрарные литералы.

Правило резолюции очень мощное правило вывода и многие ранее рассмотренные правила являются частным случаем правила резолюции.

Примеры.

1. Правило вывода modus ponens:

2. Правило транзитивности

0. Унификация

Если в формулу А вместо переменных подставить формулы , то получится формула В, которая является частным случаем формулы А.

.

Набор подстановок называется унификатором.

Таким образом, унификация состоит в том, что мы пытаемся сделать одинаковыми различные предикаты.

4.4. Правило резолюции для исчисления предикатов

Для применения правила резолюции нужны контрарные литералы в родительских дизъюнктах.

- правило резолюции в исчислении высказываний, если в предложениях С₁ и С₂ есть унифицируемые контрарные литералы Р₁ и Р₂, т. е. , , причем атомарные формулы Р₁ и Р₂ унифицируются общим унификатором .

Пример.

Пусть имеются родительские дизъюнкты:

Д1:

Д2:

Здесь и - контрарные литералы. Их можно унифицировать, если в Д1 заменить x на f(z): {f(z)//x}, а в Д2 заменить y на a: {a//y}.

Получаем:

Д1:

Д2:

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

4.5. Основные положения мр (выводы)

1. Предметная область представляется в виде множества аксиом, которые преобразуются в множество дизъюнктов S.

2. Для доказательства справедливости теоремы В надо взять ее отрицание и, преобразовав в дизъюнкт, добавить к множеству S. Если теорема верна, то новое множество дизъюнктов будет противоречиво.

3. Доказательство противоречивости сводится к доказательству того, что из данного множества дизъюнктов может быть выведен пустой дизъюнкт .

4. Технически метод резолюции состоит из унификации и получения множества резольвент до тех пор, пока не будет получен пустой дизъюнкт.

Пример 1.

А1: Все студенты – граждане.

Т: Голоса студентов – это голоса граждан.

Шаг 1. Запишем аксиому и теорему на языке предикатов первого порядка.

А1: (x , где М – множество людей)

Т: (x , где Г – множество голосов, x,y , где М – множество людей)

Шаг 2. Получим дизъюнкты.

Д1:

Чтобы получить дизъюнкты из теоремы, надо взять ее отрицание.

Таким образом, получаем систему дизъюнктов:

Д1:

Д2:

Д3:

Д4:

Шаг 3. Вывод:

1. Унифицируем Д1 иД2: { }, получаем

2. Получаем резольвенту Д1-Д2: , обозначим ее как Д5

3.Унифицируем Д4 и Д5: { }, получаем

4. Получаем резольвенту Д4 и Д5: , обозначим ее Д6

5. Д3-Д6: (пустой дизъюнкт).

Теорема доказана.

Пример 2.

А1: Если х является родителем у и у является родителем z, то х является прародителем z.

А2: Каждый человек имеет своего родителя.

В: Существуют ли такие х и у, что х является прародителем у?

Шаг 1. Запишем аксиому и вопрос на языке предикатов первого порядка.

А1:

А2:

В:

Шаг 2. Получим дизъюнкты.

Д1:

Д2:

Д3:

Шаг 3. Вывод:

1. Унифицируем Д1 и Д2: , получаем

2. Получаем резольвенту Д1-Д2: , обозначим ее Д4

3. Унифицируем Д2 и Д4: , получаем

4. Получаем резольвенту Д3-Д2: , обозначим ее Д5.

5. Унифицируем Д3 и Д5: //x}, получим

6. Получаем резольвенту Д3-Д5:

Ответ можно интерпретировать следующим образом: - быть родителем у, - быть родителем родителя у, следовательно, прародитель у – это родитель родителя у.