Prolog
Шрифт:
[ assert( дизъюнкт( C1)), аssert( сделано( ~Р, С, Р))].
% Шаг резолюции, общий случай
[ дизъюнкт( С1), удалить( Р, С1, СА),
дизъюнкт( С2), удалить( ~Р, С2, СВ),
not сделано( Cl, C2, Р) ] --->
[ assert( дизъюнкт( СА v СВ) ),
assert(
% Последнее правило: тупик
[ ] ---> [ 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). % Дизъюнкция
:-
транс( F & G) :- !, % Транслировать конъюнктивную формулу
транс( F),
транс( G).
транс( Формула) :-
тр( Формула, НовФ), !, % Шаг трансформации
транс( НовФ).
транс( Формула) :- % Дальнейшая трансформация невозможна
assert( дизъюнкт( Формула) ).
% Правила трансформаций для пропозициональных формул
тр( ~( ~Х), X) :- !. % Двойное отрицание
тр( X => Y, ~Х v Y) :- !. % Устранение импликации
тр( ~( X & Y), ~Х v ~Y) :- !. % Закон де Моргана
тр( ~( X v Y), ~Х & ~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), !.
тр( ~Х, ~Х1) :- % Трансформация подвыражения
тр( X, X1).
Рис. 16. 8. Преобразование пропозициональных формул в множество
дизъюнктов с записью их в базу данных при помощи assert.
?- транс( ~(( а=>b) & ( b=>c) => ( а=>с)) ), пуск.
Ответ программы "Обнаружено противоречие" будет означать, что исходная формула является теоремой.
Назад | Содержание | Вперёд
Назад | Содержание | Вперёд
16. 4. Заключительные замечания
Нашего простого интерпретатора было вполне достаточно для того, чтобы проиллюстрировать некоторые идеи, лежащие в основе программирования в терминах образцов. Применение этого интерпретатора для более сложных приложений потребовало бы его доработки в целом ряде направлений. Ниже приводится несколько критических замечаний, а также ряд конкретных предложений по усовершенствованию алгоритма интерпретации.