Prolog
Шрифт:
И наконец, после применения правила 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 (результат - СА), удалить ~Р
данных новый дизъюнкт СА 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), дизъзюнкт( ~Х) ] --->
[ write( 'Обнаружено противоречие'), стоп].
% Удалить тривиально истинный дизъюнкт
[ дизъюнкт( С), внутри( Р, С), внутри( ~Р, С) ] --->
[ retract( С) ].
% Упростить дизъюнкт
[ дизъюнкт( С), удалить( Р, С, С1), внутри( Р, С1) ] --->
[ заменить( дизъюнкт( С), дизъюнкт( С1) ) ].
% Шаг резолюции, специальный случай
[ дизъюнкт( Р), дизъюнкт( С), удалить( ~Р, С, С1),
not сделано( Р, С, Р) ] --->
[ аssеrt( дизъюнкт( С1)), аssert( сделано( Р, С, Р))].
% Шаг резолюции, специальный случай
[ дизъюнкт( ~Р), дизъюнкт( С), удалить( Р, С, С1),
not сделано( ~Р, С, Р) ] --->