6
Всевозможные действия робота определяются множеством операторов.
Оператор входит в это множество, если существует хотя бы одна модель среды, в
которой этот оператор может быть применен. Необходимо точно определить эф-
фект действия каждого оператора. Условия применимости оператора, формули-
руемые на языке логики предикатов, позволяют установить, можно ли применить
этот оператор в данной модели. Если его можно применить, то необходимо ука-
зать, как трансформируется модель среды после применения оператора.
Пусть М – модель среды, а В – условие применимости некоторого операто-
ра. Неудовлетворимость множества формул {М
U В} означает, что этот опера-
тор может быть применен. Часто оператор может зависеть от параметра, т. е.
)( pBB =
. В этом случае для применимости оператора достаточно найти хотя бы
одно значение параметра p
′
, для которого {
)( pBM
′
U
} является проти-
воречием.
Кроме этого, логическое следование некоторого утверждения из множества
посылок (аксиом) необходимо доказывать и при проверке достижимости цели
управления в данной модели. Пусть B – цель управления, сформулированная па
языке логики предикатов, а М – модель среды, построенная в результате некото-
рых предшествующих действий. Если В логически следует из М, т. е. {М
U В}
является противоречием, то цель управления достигнута. В противном случае
надо искать операторы, применимые в данной модели, с целью дальнейших пре-
образований.
Для построения машинных программ, автоматически доказывающих логи-
ческие следования некоторых утверждений на основе заданного набора посылок,
составляющих содержание модели, можно пользоваться различными правилами
вывода, разработанными в математической логике. Наиболее перспективным
правилом вывода в настоящее время признан метод резолюций (или иначе – ме-
тод резольвенций [11]) Дж. А. Робинсона (1965), который дает наиболее механи-
зируемый алгоритм доказательства. Его преимущество состоит в проверке ми-
нимального числа частных случаев при поиске противоречия.
Рассмотрим простой пример планирования действий манипуляционного
робота, с помощью которого можно проиллюстрировать применение аппарата
логики предикатов. Этот пример представляет такую перефразировку известной
задачи об обезьяне и бананах [9], которая в достаточной степени соответствует
задачам манипуляционных роботов. Кроме этого, в нашем примере, так же как и
в известной системе STRIPS [8], процесс логического доказательства теорем бу-
дет полностью отделен от процесса поиска в пространстве моделей среды (в от-
личие от других систем, в которых для отыскания нужной последовательности
операторов используются исключительно лишь формальные методы логики). В
нашем случае метод доказательства теорем используется только внутри некото-
рой заданной модели среды для ответов на вопросы, касающиеся применимости
различных операторов и достижимости цели. Это позволяет проиллюстрировать
сразу два аспекта рассматриваемого здесь эвристического направления искусст-