Структуры данных и модели вычислений
в хорновской клаузальной формуле отсутствуют
и доказать, что истинны , , . Такие формулы принято называть правилами.
Если в хорновской клаузальной формуле отсутствуют атомарные части с отрицанием, то такая формула называется фактом. Если в хорновской клаузальной формуле отсутствует атомарная часть без отрицания, то такая формула называется запросом. Программой в Прологе называется набор фактов и правил.
По заданной программе и запросу система Пролог определяет, является ли запрос логическим следствием фактов и правил программы. При этом если в запросе имеются свободные переменные, то в процессе поиска доказательства эти переменные конкретизируются, то есть принимают конкретные значения, и при успешном его завершении эти конкретизированные значения являются ответом к поставленной задаче. Если же доказательство не будет найдено, то система ответит "no".
Примеры формальных доказательств
Пример.
Вывести из гипотез , ,
заключение , где
Префиксная форма:
Сколемовская форма:
Клаузальная форма (опускаем кванторы общности, а бескванторные части приводим к КНФ и из каждого сомножителя получаем клаузу):
Доказательство с использованием правила резолюции:
Пример.
Рассмотрим предикаты с интерпретацией: В качестве аксиом рассмотрим формулы
Пусть из интерпретации известны факты
Вопрос: "Есть ли брат у Харитона?" — на языке предикатов записывается как
Доказательство
Фактически мы не только получили ответ на наш запрос, но и подтвердили его конкретным значением переменной . Приведенный вывод можно модифицировать, если ввести предикат и вместо цели
поставить новую цель
Упражнение
Рассмотрите вывод, в котором первые 7 формул являются посылками. Для остальных формул выпишите пояснения к применению правила резолюции.
