Структуры данных и модели вычислений

         

в хорновской клаузальной формуле отсутствуют


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

Если в хорновской клаузальной формуле отсутствуют атомарные части с отрицанием, то такая формула называется фактом. Если в хорновской клаузальной формуле отсутствует атомарная часть без отрицания, то такая формула называется запросом. Программой в Прологе называется набор фактов и правил.

По заданной программе и запросу система Пролог определяет, является ли запрос логическим следствием фактов и правил программы. При этом если в запросе имеются свободные переменные, то в процессе поиска доказательства эти переменные конкретизируются, то есть принимают конкретные значения, и при успешном его завершении эти конкретизированные значения являются ответом к поставленной задаче. Если же доказательство не будет найдено, то система ответит "no".

Примеры формальных доказательств

Пример.

Вывести из гипотез , ,

заключение , где

Префиксная форма:

Сколемовская форма:

Клаузальная форма (опускаем кванторы общности, а бескванторные части приводим к КНФ и из каждого сомножителя получаем клаузу):

Доказательство с использованием правила резолюции:

Пример.

Рассмотрим предикаты с интерпретацией: В качестве аксиом рассмотрим формулы

Пусть из интерпретации известны факты

Вопрос: "Есть ли брат у Харитона?" — на языке предикатов записывается как

Доказательство

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

поставить новую цель

Упражнение

Рассмотрите вывод, в котором первые 7 формул являются посылками. Для остальных формул выпишите пояснения к применению правила резолюции.


Содержание  Назад  Вперед