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

(2) ~ ( x v y ) эквивалентно ~x & ~у

(3) ~ ( x & у ) эквивалентно ~x v ~у

(4) ~ ( ~x ) эквивалентно x

Применяя правило 1, получаем

~(~(( a => b ) & ( b => с )) v ( а => с ))

Далее, правила 2 и 4 дают

( а => b ) & ( b => с ) & ~( а => с )

Трижды применив правило 1, получаем

( ~а v b ) & ( ~b v с ) & ~ ( ~а v с )

И наконец, после применения правила 2 получаем искомую конъюнктивную нормальную форму

( ~а v b ) & ( ~b v с ) & а & ~с

состоящую из четырех дизъюнктов. Теперь можно приступить к резолюционному процессу.

Элементарный шаг резолюции выполняется всегда, когда имеется два дизъюнкта, в одном из которых встретилось элементарное утверждение p , а в другом — ~p . Пусть этими двумя дизъюнктами будут

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),