Программирование на языке Пролог для искусственного интеллекта

16.2. Простой интерпретатор программ, управляемых образцами

Для описания модулей, управляемых образцами, мы применим следующую синтаксическую конструкцию:

ЧастьУсловия ---> ЧастьДействия

Часть условия представляет собой список условий:

[ Условие1, Условие2, Условие3, ...]

где Условие1, Условие2 и т.д. — обычные прологовские цели. Предварительное условие запуска модуля считается выполненным, если все цели, содержащиеся в списке, достигнуты. Часть действия — это список действий:

[ Действие1, Действие2, ...]

Каждое отдельное действие — это, как и раньше, прологовская цель. Для того, чтобы выполнить список действий, нужно выполнить все действия из списка. Другими словами, все соответствующие цели должны быть удовлетворены. Среди допустимых действий будут действия, соответствующие манипулированию базой данных: добавить, удалить или заменить те или иные объекты базы данных.

На рис. 16.4 показано, как выглядит наша программа вычисления наибольшего общего делителя, записанная в соответствии с введенным нами синтаксисом.

% Продукционные правила для нахождения наибольшего общего
% делителя (алгоритм Евклида)
:- op( 300, fx, число).
[ число X, число Y, X > Y ] --->
 [ НовХ is X - Y, заменить( число X, число НовХ) ].
[ число X ] ---> [ write( X), стоп ].
% Начальное состояние базы данных
число 25.
число 10.
число 15.
число 30.

Рис. 16.4. Программа, управляемая образцами, для получения наибольшего общего делителя множества чисел.

Самый простой способ реализации этого языка — использовать механизмы управления базой данных, встроенные в Пролог. Добавить объект в базу данных или удалить объект из базы данных можно, применяя встроенные процедуры

assert ( Объект)   retract( Объект)

Заменить один объект на другой также просто:

заменить( Объект1, Объект2) :-
 retract( Объект1), !,
 assert( Объект2).

Здесь задача оператора отсечения — не допустить, чтобы оператор retract удалил из базы данных более чем один объект (при возвратах).

% Простой интерпретатор для программ, управляемых образцами
% Работа с базой данных производится при помощи процедур
% assert и retract
:- op( 800, xfx, --->).
пуск :-
 Условие ---> Действие,          % правило
 проверить( Условие),            % Условие выполнено?
 выполнить( Действие).
проверить( []).                  % Пустое условие
проверить( [Усл | Остальные]) :- % проверить конъюнкцию
 call( Усл),                     % условий
 проверить( Остальные).
выполнить( [ стоп] ) :- !. % Прекратить выполнение
выполнить( []) :-          % Пустое действие (цикл завершен)
 пуск.                     % Перейти к следующему циклу
выполнить [Д | Остальные] ) :-
 саll( Д),
 выполнить( Остальные).
заменить( А, В) :-         % Заменить в базе данных А на В
 retract( A), !,
 assert( В).

Рис. 16.5. Простой интерпретатор для программ, управляемых образцами.

Простой интерпретатор для программ, управляемых образцами, показан на рис. 16.5. Следует признать, что в интерпретаторе допущены значительные упрощения. Так, например, в него заложено чрезвычайно простое и жесткое правило разрешения конфликтов: всегда запускать первый из потенциально активных модулей (в соответствии с тем порядком, в котором модули записаны в программе). Таким образом, программисту предоставлено единственное средство управления процессом интерпретации — он может указать тот или иной порядок следования модулей. Начальное состояние базы данных задается в виде прологовских предложений, записанных в исходной программе. Запуск программы производится при помощи вопроса

?- пуск.

16.3. Простая программа для автоматического доказательства теорем

В настоящем разделе мы реализуем простую программу для автоматического доказательства теорем в виде системы, управляемой образцами. Эта программа будет основана на принципе резолюции — популярном методе, обычно используемом в машинном доказательстве теорем. Мы ограничимся случаем пропозициональной логики, поскольку нашей целью будет дать всего лишь простую иллюстрацию используемого принципа. На самом деле, принцип резолюции можно легко обобщить на случай исчисления высказываний первого порядка (с применением логических формул, содержащих переменные). Базовый Пролог можно рассматривать как частный случай системы доказательства теорем, основанной на принципе резолюции.

Задачу доказательства теорем можно сформулировать так: дана формула, необходимо показать, что эта формула является теоремой, т.е. она верна всегда, независимо от интерпретации встречающихся в ней