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

Начнем с очень простой задачи воздушной транспортировки. В начальном состоянии (время 0) самолет Ρ1 находится в аэропорту SFO, а самолет Р2 — в аэропорту JFK. Задача состоит в том, чтобы Р1 находился в JFK, а Р2 — в SFO; иными словами, самолеты должны поменяться местами. Прежде всего, потребуются отдельные пропозициональные символы для формирования утверждений о каждом временном этапе. Для обозначения временного этапа будут использоваться верхние индексы, как и в главе 7. Поэтому начальное состояние можно записать следующим образом:

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

Сама цель должна быть связана с конкретным временным этапом. Поскольку мы не знаем заранее, какое количество этапов потребуется для достижения цели, то можно попытаться сформулировать утверждение, что цель истинна в начальном состоянии, во время т=0. Это означает, что мы вводим утверждение . Если эта попытка окажется неудачной, повторим ее снова во время Т=1 и т.д. до тех пор, пока не достигнем осуществимого плана с минимальной длиной. Для каждого значения τ база знаний будет включать только высказывания, покрывающие временные этапы от 0 вплоть до Т. Чтобы обеспечить завершение работы алгоритма, можно наложить произвольный верхний предел, . Этот алгоритм приведен в листинге 11.7. Альтернативный подход, позволяющий избежать использования многочисленных попыток решения, обсуждается в упр. 11.17.