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

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

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

.

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

р v Y и ~р v

Z

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

Y v Z

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

x и ~x

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

Рис. 16. 6. Доказательство теоремы (а=>b)&(b=>с)=>(a=>с) методом

резолюции. Верхняя строка - отрицание теоремы в конъюнктивной

нормальной форме. Пустой дизъюнкт внизу сигнализирует, что

отрицание теоремы противоречиво.

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

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

если

существуют два таких дизъюнкта С1 и С2, что

P является (дизъюнктивным) подвыражением С1,

а ~Р– подвыражением С2

то

удалить Р из С1 (результат - СА), удалить ~Р

из С2 (результат - СВ) и добавить в базу

данных новый дизъюнкт СА v СВ.

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

[ дизъюнкт( С1), удалить( Р, Cl, CA),

дизъюнкт( С2), удалить( ~Р, С2, СВ) ] --->

[ assert( дизъюнкт( СА v СВ) ) ].

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

сделано( Cl, C2, Р)

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

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

a v b v a

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

a v b v ~а

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

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

% доказательства теорем

% Противоречие

[ дизъюнкт( X), дизъзюнкт( ~Х) ] --->