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

то

 удалить P из C1 (результат — CA), удалить ~P из C2 (результат — CB) и добавить в базу данных новый дизъюнкт CA v CB.

На нашем формальном языке это можно записать так:

[ дизъюнкт( C1), удалить( P, C1, CA),
  дизъюнкт( C2), удалить( ~P, C2, CB) ] --->
 [ assert( дизъюнкт( СА v СВ) ) ].

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

сделано( C1, C2, P)

В условных частях правил производится распознавание подобных утверждений и обход соответствующих повторных действий.

Правила, показанные на рис. 16.7, предусматривают также обработку специальных случаев, в которых требуется избежать явного представления пустого дизъюнкта. Кроме того, имеются два правила для упрощения дизъюнктов. Одно из них убирает избыточные подвыражения. Например, это правило превращает выражение

a  v  b  v  a

в более простое выражение a v b. Другое правило распознает те дизъюнкты, которые всегда истинны, например,

a  v  b  v  ~а

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

% Продукционные правила для задачи автоматического
% доказательства теорем
% Противоречие
[ дизъюнкт( X), дизъзюнкт( ~X) ] --->
 [ write( 'Обнаружено противоречие'), стоп].
% Удалить тривиально истинный дизъюнкт
[ дизъюнкт( С), внутри( P, С), внутри( ~P, С) ] --->
 [ retract( С) ].
% Упростить дизъюнкт
[ дизъюнкт( С), удалить( P, С, C1), внутри( P, C1) ] --->
 [ заменить( дизъюнкт( С), дизъюнкт( C1) ) ].
% Шаг резолюции, специальный случай
[ дизъюнкт( P), дизъюнкт( С), удалить( ~P, С, C1),
  not сделано( P, С, P) ] --->
 [ аssеrt( дизъюнкт( C1)), аssert( сделано( P, С, P))].
% Шаг резолюции, специальный случай
[ дизъюнкт( ~P), дизъюнкт( С), удалить( P, С, C1),
  not сделано( ~P, С, P) ] --->
 [ assert( дизъюнкт( C1)), аssert( сделано( ~P, С, P))].
% Шаг резолюции, общий случай
[ дизъюнкт( C1), удалить( P, C1, CA),
  дизъюнкт( C2), удалить( ~P, C2, CB),
  not сделано( C1, C2, P) ] --->
 [ assert( дизъюнкт( CA v CB) ),
   assert( сделано( C1, C2, P) ) ].
% Последнее правило: тупик
[] ---> [ write( 'Нет противоречия'), стоп ].
% удалить( P, E, E1) означает, получить из выражения E
% выражение E1, удалив из него подвыражение P
удалить( X, X v Y, Y).
удалить( X, Y v X, Y).
удалить( X, Y v Z, Y v Z1) :-
 удалить( X, Z, Z1).
удалить( X, Y v Z, Y1 v Z) :-
 удалить( X, Y, Y1).
% внутри( P, E) означает P есть дизъюнктивное подвыражение
% выражения E
внутри( X, X).
внутри( X, Y) :-
 удалить( X, Y, _ ).

Рис. 16.7. Программа, управляемая образцами, для автоматического доказательства теорем.

Остается еще один вопрос: как преобразовать заданную пропозициональную формулу в конъюнктивную нормальную форму? Это несложное преобразование выполняется с помощью программы, показанной на рис. 16.8. Процедура

транс( Формула)

транслирует заданную формулу в множество дизъюнктов C1, C2 и т.д. и записывает их при помощи assert в базу данных в виде утверждений

дизъюнкт( C1).
дизъюнкт( C2).
...

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

?- транс(~(( а=>b) & ( b=>c) => ( а=>с)) ), пуск.

Ответ программы 'Обнаружено противоречие' будет означать, что исходная формула является теоремой.

% Преобразование пропозициональной формулы в множество
% дизъюнктов с записью их в базу данных при помощи assert
:- op( 100, fy, ~).           % Отрицание