добавить в базу
данных новый дизъюнкт
На нашем формальном языке это можно записать так:
[ дизъюнкт( С1), удалить( Р, Cl, CA),
дизъюнкт( С2), удалить( ~Р, С2, СВ) ] --->
[ assert( дизъюнкт( СА v СВ) ) ].
Это правило нуждается в небольшой доработке. Дело в том, что мы не должны допускать повторных взаимодействий между дизъюнктами, так как они порождают новые копии уже существующих формул. Для этого в программе рис. 16.7 предусматривается запись в базу данных информации об уже произведенных взаимодействиях в форме утверждений вида
сделано( Cl, C2, Р)
В условных частях правил производится распознавание подобных утверждений и обход соответствующих повторных действий.
Правила, показанные на рис. 16.7, предусматривают также обработку специальных случаев, в которых требуется избежать явного представления пустого дизъюнкта. Кроме того, имеются два правила для упрощения дизъюнктов. Одно из них убирает избыточные подвыражения. Например, это правило превращает выражение
в более простое выражение
и удаляет их из базы данных, поскольку они бесполезны при поиске противоречия.
% Продукционные правила для задачи автоматического
% доказательства теорем
% Противоречие
[ дизъюнкт( X), дизъзюнкт( ~Х) ] --->
[ write( 'Обнаружено противоречие'), стоп].
% Удалить тривиально истинный дизъюнкт
[ дизъюнкт( С), внутри( Р, С), внутри( ~Р, С) ] --->
[ retract( С) ].
% Упростить дизъюнкт
[ дизъюнкт( С), удалить( Р, С, С1), внутри( Р, С1) ] --->
[ заменить( дизъюнкт( С), дизъюнкт( С1) ) ].
% Шаг резолюции, специальный случай
[ дизъюнкт( Р), дизъюнкт( С), удалить( ~Р, С, С1),
not сделано( Р, С, Р) ] --->
[ аssеrt( дизъюнкт( С1)), аssert( сделано( Р, С, Р))].
% Шаг резолюции, специальный случай
[ дизъюнкт( ~Р), дизъюнкт( С), удалить( Р, С, С1),
not сделано( ~Р, С, Р) ] --->
[ assert( дизъюнкт( C1)), аssert( сделано( ~Р, С, Р))].
% Шаг резолюции, общий случай
[ дизъюнкт( С1), удалить( Р, С1, СА),
дизъюнкт( С2), удалить( ~Р, С2, СВ),
not сделано( Cl, C2, Р) ] --->
