Prolog
Шрифт:
сделано( Cl, C2, Р)
В условных частях правил производится распознавание подобных утверждений и обход соответствующих повторных действий.
Правила, показанные на рис. 16.7, предусматривают также обработку специальных случаев, в которых требуется избежать явного представления пустого дизъюнкта. Кроме того, имеются два правила для упрощения дизъюнктов. Одно из них убирает избыточные подвыражения. Например, это правило превращает выражение
a v b v a
в более простое выражение a v b. Другое правило распознает те дизъюнкты, которые всегда истинны, например,
a v b v ~а
и удаляет их из базы данных, поскольку они бесполезны при поиске противоречия.
% Продукционные правила для задачи автоматического
% доказательства теорем
% Противоречие
[ дизъюнкт( X), дизъзюнкт( ~Х) ] --->
[ 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).
транс( Формула) :-
тр( Формула, НовФ), !, % Шаг трансформации
транс( НовФ).
транс( Формула) :- % Дальнейшая трансформация невозможна
assert( дизъюнкт( Формула) ).
% Правила трансформаций для пропозициональных формул
тр( ~( ~Х), X) :- !. % Двойное отрицание
тр( X => Y, ~Х v Y) :- !. % Устранение импликации
тр( ~( X & Y), ~Х v ~Y) :- !. % Закон де Моргана
тр( ~( X v Y), ~Х & ~Y) :- !. % Закон де Моргана