Основные положения МР (выводы)
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: Ú
Ответ можно интерпретировать следующим образом: — быть родителем у, — быть родителем родителя у, следовательно, прародитель у – это родитель родителя у.