Основные положения МР (выводы)

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: Ú

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

Не нашли, что искали? Воспользуйтесь поиском: