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

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

Иван Братко

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

Для преобразования этой формулы в конъюнктивную нормальную форму можно использовать следующие известные правила:

(1) x => у эквивалентно ~x v у

(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( С) ].