[ 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).
транс( Формула) :-
тр( Формула, НовФ), !, % Шаг трансформации
транс( НовФ).
