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: U
Ответ можно интерпретировать следующим образом:
- быть родителем у,
- быть родителем родителя у, следовательно, прародитель у – это родитель родителя у.
Еще по теме 4.5. Основные положения МР (выводы):
- Основные положения диссертации, выносимые на защиту, относятся к выводам и предложениям о том, что:
- 8. Доказывая и развивая каждое отдельное положение, не упускайте из виду главной мысли и других основных положений
- Научную новизну имеют также теоретические положения и практические выводы, выносимые на защиту:
- 3.3. Основные выводы
- Из рассмотренных положений можно сделать вывод о том, что, хотя продавцы и покупатели как участники рыночных отношений
- Основные выводы
- §8. Основные выводы
- Основные выводы
- Основные выводы
- Основные результаты и выводы
- Основные результаты и выводы.
- 1.5. Основные выводы
- 2.3. Основные выводы
- 4.3. Основные выводы