Чтение онлайн

[ 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) :- !. % Закон де Моргана

тр( 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. Заключительные замечания

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