[ write( 'Обнаружено противоречие'), стоп].

% Удалить тривиально истинный дизъюнкт

[ дизъюнкт( С), внутри( Р, С), внутри( ~Р, С) ] --->

[ retract( С) ].

% Упростить дизъюнкт

[ дизъюнкт( С), удалить( Р, С, С1), внутри( Р, С1) ] --->

[ заменить( дизъюнкт( С), дизъюнкт( С1) ) ].

% Шаг резолюции, специальный случай

[ дизъюнкт( Р), дизъюнкт( С), удалить( ~Р, С, С1),

not сделано( Р, С, Р) ] --->

[ аssеrt( дизъюнкт( С1)), аssert( сделано( Р, С, Р))].

% Шаг резолюции, специальный случай

[ дизъюнкт( ~Р), дизъюнкт( С), удалить( Р, С, С1),

not сделано( ~Р, С, Р) ] --->

[ assert( дизъюнкт( C1)), аssert( сделано( ~Р, С, Р))].

% Шаг резолюции, общий случай

[ дизъюнкт( С1), удалить( Р, С1, СА),

дизъюнкт( С2), удалить( ~Р, С2, СВ),

not сделано( Cl, C2, Р) ] --->

[ assert( дизъюнкт( СА v СВ) ),

assert( сделано( Cl, C2, Р) ) ].

% Последнее правило: тупик

[ ] ---> [ write( 'Нет противоречия'), стоп ].

% удалить( Р, Е, Е1) означает, получить из выражения Е

% выражение Е1, удалив из него подвыражение Р

удалить( 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).

% внутри( Р, Е) означает Р есть дизъюнктивное подвыражение

% выражения Е

внутри( X, X).

внутри( X, Y) :-

удалить( X, Y, _ ).

Рис. 16. 7. Программа, управляемая образцами, для

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

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

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

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

дизъюнкт( С1).

дизъюнкт( С2).

. . .

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

% Преобразование пропозициональной формулы в множество

% дизъюнктов с записью их в базу данных при помощи assert

:- ор( 100, fy, ~). % Отрицание

:- ор( 110, xfy, &). % Конъюнкция

:- ор( 120, xfy, v). % Дизъюнкция

:- ор( 130, xfy, =>). % Импликация

транс( F & G) :- !, % Транслировать конъюнктивную формулу

транс( F),

транс( G).

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

тр( Формула, НовФ), !, % Шаг трансформации

транс( НовФ).

транс( Формула) :- % Дальнейшая трансформация невозможна