Неизвестно - Prolog

Правила, показанные на рис. 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) :- !. % Закон де Моргана

тр( 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) => ( а=>с)) ), пуск.