Логическое программирование

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

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

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

Приведенный метод резолюций служит основой языков логического программирования. Главное отличие языков логического программирования от процедурных языков заключается в том, что программа не указывает как что-то сделать, а описывает некоторые элементы и связи между ними (модель) и ставит цель, т. е. задает вопрос об этой системе. На формальном языке это означает проверить истинность предложения на данной системе. При этом компьютер самостоятельно выбирает стратегию для решения поставленных вопросов.

Логическая программа представляет собой конечный набор выражений следующих видов:

факты: , (1)

правила: , (2)

где ,- атомарные формулы.

Правило читается как: «если истинны , то истинно ». Формула называется заголовком правила.

Правила позволяют выводить новые факты из уже существующих. Факты определяют отношения между объектами.

Для выполнения программы необходимо обратиться к целевому запросу (цели), которая представляет собой последовательность атомарных формул вида:

. (3)

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

Каждому факту (1) поставим в соответствие предложение:

А:, где - все переменные, входящие в формулу .

Каждому правилу (2) поставим в соответствие предложение:

В:, где - все переменные, входящие в формулы

Запросу (3) поставим в соответствие формулу:

С:,

где кванторы связывают все переменные.

Нужно доказать

Для доказательства используется метод резолюций.

Дата добавления: 2014-01-15