[ 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, ~). % Отрицание
:- op( 110, xfy, &). % Конъюнкция
:- op( 120, xfy, v). % Дизъюнкция
:- op( 130, xfy, =>). % Импликация
транс( F & G) :- !, % Транслировать конъюнктивную формулу
транс( F),
транс( G).
транс( Формула) :-
тр( Формула, НовФ), !, % Шаг трансформации
транс( НовФ).
транс( Формула) :- % Дальнейшая трансформация невозможна
assert( дизъюнкт( Формула) ).
% Правила трансформаций для пропозициональных формул
тр( ~( ~X), X) :- !. % Двойное отрицание
тр( X => Y, ~X v Y) :- !. % Устранение импликации
тр( ~( X & Y), ~X v ~Y) :- !. % Закон де Моргана
тр( ~( X v Y), ~X & ~Y) :- !. % Закон де Моргана
тр( X & Y v Z, (X v Z) & (Y v Z) ) :- !.
% Распределительный закон
тр( X v Y & Z, (X v Y) & (X v Z) ) :- !.
% Распределительный закон
тр( X v Y, X1 v Y) :- % Трансформация подвыражения
тр( X, X1), !.
тр( X v Y, X v Y1) :- % Трансформация подвыражения
тр( Y, Y1), !.
тр( ~X, ~Х1) :- % Трансформация подвыражения
тр( X, X1).
Рис. 16.8. Преобразование пропозициональных формул в множество дизъюнктов с записью их в базу данных при помощи assert.
