7.7. ОДНА ФОРМАЛИЗАЦИЯ ДЛЯ РЕШЕНИЯ ЗАДАЧ В ПРОСТРАНСТВЕ СОСТОЯНИИ

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

следовали логически из родительских п. п. формул. Преобразования, связанные с операторами, изменяли описания состояний, и совершались независимо от системы логического вывода в исчислении предикатов.

При небольшой переформулировке удается включить описание действий операторов в рамки формализма исчисления предикатов. Чтобы это сделать, добавим в каждый предикат терм состояния, указывающий состояние, к которому предикат применим, тогда в нашем предыдущем примере начальное состояние описывалось бы с помощью множества п. п. формул Здесь термом состояния является

В такой формулировке операторы рассматриваются как функции, отображающие одно состояние в другое. Так, значением оператора «схватить будет новое состояние, возникающее в результате применения оператора «схватить» к состоянию Основной эффект применения оператора «схватить» можно описать с помощью п. п. формулы

означающий «для всех если обезьяна находится на ящике, а ящик расположен в точке с в состоянии то в состоянии, возникающем в результате применения оператора «схватить» к состоянию обезьяна будет иметь бананы».

При таком способе описания операторные описания — это просто дополнительные «аксиомы», которые можно объединить с п. п. формулами, описывающими начальное состояние Если наша цель состоит в создании состояния удовлетворяющего некоторой целевой п. п. формуле то эту задачу можно решить формально, найдя сначала доказательство для предположения а затем использовав процесс извлечения ответа для получения решения. Ответное утверждение будет содержать выражение для целевого состояния в форме композиции операторных функций.

Для иллюстрации этого подхода воспользуемся упрощенной формой задачи об обезьяне и бананах. Предположим, что у нас только три оператора — «схватить», «взобраться», «передвинуть», и условия их применимости несколько отличаются от прежних. (Эта упрощенная форма больше всего подходит для решения иллюстративных задач. Читателю предлагается поработать также с четырехоператорным вариантом задачи, который рассматривался в предыдущем разделе.) Действие этих операторов можно описать следующими п. п. формулами:

1. , т. е. «для всех х и если обезьяна не находится на ящике в состоянии то в состоянии, возникающем в результате

применения оператора «передвинуть (х)». к состоянию ящик будет расположен в точке х.

2. , т. е. для всех в состоянии, возникающем в результате применения оператора «взобраться» к состоянию обезьяна находится на ящике.

3. т. е. для всех если обезьяна находится на ящике, а ящик расположен в точке с в состоянии то в состоянии, возникающем в результате применения оператора «схватить» к состоянию обезьяна будет иметь бананы.

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

Нам понадобится также адекватное описание начального состояния

Теперь поставить вопрос перед нашим формальным решателем задач — это просто сформулировать предположение

Далее надо преобразовать приведенные выше аксиомы и отрицание предположения в форму предложений и получить дерево опроверженйя, изображенное на рис. 7.12. Ответным утверждением, извлеченным обычным образом из этого дерева, будет утверждение

Отсюда видно, что искомое состояние достигается с помощью последовательности операторов

Интересно сопоставить этот формальный подход к решению задачи с методом пространства состояний (использующим исчисление предикатов для проверки выполнения условий достижения цели и применимости операторов), рассмотренным в предыдущем разделе. Формальный подход дает то преимущество, что для выполнения операторных вычислений не требуется никакого специального механизма. Вычисления выполняются автоматически с помощью механизма дедукции, воплощенного в доказателе теорем. Таким образом, не требуется никаких специальных методов перебора в пространстве состояний (или перебора при сведении задачи к подзадачам), кроме тех, которые

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

Рис. 7.12. (см. скан) Доказательство для задачи об обезьяне и бананах.

Другой недостаток формальной процедуры — необходимость явного описания с помощью специальных аксиом тех отношений, которые не изменяются под воздействием операторов. Так, в нашем примере пришлось сформулировать и использовать тот факт, что положение ящика не изменяется при действии оператора «взобраться». Доказательство того, что определенные отношения в дочерних состояниях по-прежнему удовлетворяются, утомительно и значительно увеличивает затраты усилий при поиске полного доказательства. Проблема, связанная с тем, что на одни отношения операторы воздействуют, а на другие нет, иногда называется проблемой системы отсчета. В наших

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