Программирование на языке Пролог для искусственного интеллекта

p v Y и ~p v Z

Шаг резолюции порождает третий дизъюнкт:

Y v Z

Нетрудно показать, что этот дизъюнкт логически следует из тех двух дизъюнктов, из которых он получен. Таким образом, добавив выражение (Y v Z) к нашей исходной формуле, мы не изменим ее истинности. Резолюционный процесс порождает новые дизъюнкты. Появление "пустого дизъюнкта" (обычно записываемого как "nil") сигнализирует о противоречии. Действительно, пустой дизъюнкт nil порождается двумя дизъюнктами вида

x и ~x

которые явно противоречат друг другу.

Рис. 16.6. Доказательство теоремы (а=>b)&(b=>с)=>(a=>с) методом резолюции. Верхняя строка — отрицание теоремы в конъюнктивной нормальной форме. Пустой дизъюнкт внизу сигнализирует, что отрицание теоремы противоречиво.

На рис. 16.6 показан процесс применения резолюций, начинающийся с отрицания нашей предполагаемой теоремы и заканчивающийся пустым дизъюнктом.

На рис. 16.7 мы видим, как резолюционный процесс можно сформулировать в форме программы, управляемой образцами. Программа работает с дизъюнктами, записанными в базе данных. В терминах образцов принцип резолюции формулируется следующим образом:

если

 существуют два таких дизъюнкта C1 и C2, что P является (дизъюнктивным) подвыражением C1, а ~P — подвыражением C2

то

 удалить P из C1 (результат — CA), удалить ~P из C2 (результат — CB) и добавить в базу данных новый дизъюнкт CA v CB.

На нашем формальном языке это можно записать так:

[ дизъюнкт( C1), удалить( P, C1, CA),
 дизъюнкт( C2), удалить( ~P, C2, CB) ] --->
 [ assert( дизъюнкт( СА v СВ) ) ].

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

сделано( C1, C2, P)

В условных частях правил производится распознавание подобных утверждений и обход соответствующих повторных действий.

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

a v b v a

в более простое выражение a v b. Другое правило распознает те дизъюнкты, которые всегда истинны, например,

a v b v ~а

и удаляет их из базы данных, поскольку они бесполезны при поиске противоречия.

% Продукционные правила для задачи автоматического
% доказательства теорем

% Противоречие
[ дизъюнкт( X), дизъзюнкт( ~X) ] --->
 [ write( 'Обнаружено противоречие'), стоп].

% Удалить тривиально истинный дизъюнкт
[ дизъюнкт( С), внутри( P, С), внутри( ~P, С) ] --->
 [ retract( С) ].

% Упростить дизъюнкт
[ дизъюнкт( С), удалить( P, С, C1), внутри( P, C1) ] --->
 [ заменить( дизъюнкт( С), дизъюнкт( C1) ) ].

% Шаг резолюции, специальный случай
[ дизъюнкт( P), дизъюнкт( С), удалить( ~P, С, C1),
 not сделано( P, С, P) ] --->
 [ аssеrt( дизъюнкт( C1)), аssert( сделано( P, С, P))].

% Шаг резолюции, специальный случай
[ дизъюнкт( ~P), дизъюнкт( С), удалить( P, С, C1),
 not сделано( ~P, С, P) ] --->
 [ assert( дизъюнкт( C1)), аssert( сделано( ~P, С, P))].

% Шаг резолюции, общий случай
[ дизъюнкт( C1), удалить( P, C1, CA),
 дизъюнкт( C2), удалить( ~P, C2, CB),
 not сделано( C1, C2, P) ] --->
 [ assert( дизъюнкт( CA v CB) ),
 assert( сделано( C1, C2, P) ) ].

% Последнее правило: тупик
[] ---> [ write( 'Нет противоречия'), стоп ].

% удалить( P, E, E1) означает, получить из выражения E
% выражение E1, удалив из него подвыражение P
удалить( 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).

% внутри( P, E) означает P есть дизъюнктивное подвыражение
% выражения E
внутри( X, X).
внутри( X, Y) :-
 удалить( X, Y, _ ).

Рис. 16.7. Программа, управляемая образцами, для автоматического доказательства теорем.