Решение проблемы выводимого окружения
Аксиомы состояния-преемника позволяют решить проблему представительного окружения, но не проблему выводимого окружения. Рассмотрим t-шаговый план р, такой, что St=Result(p, S0). Чтобы определить, какие флюентные высказывания являются истинными в состоянии St, необходимо рассмотреть каждую из F аксиом окружения в каждом из t временнь/х шагов. Поскольку аксиомы имеют средний размер АЕ/ F, это соответствует объему работы по логическому выводу, измеряемому величиной 0{AEt). Основной объем этой работы связан с копированием флюентных высказываний в неизменном виде из описания одной ситуации в описание следующей.
Для решения проблемы выводимого окружения можно воспользоваться следующими двумя подходами. Во-первых, можно отбросить ситуационное исчисление и изобрести новую формальную систему для записи аксиом. Указанная задача была решена в таких формальных системах, как исчисление флюентных высказываний (fluent calculus). Во-вторых, можно изменить механизм логического вывода таким образом, чтобы в нем аксиомы окружения обрабатывались более эффективно. На то, что должна существовать такая возможность, указывает сам факт, что трудоемкость этого простого подхода оценивается величиной 0{AEt); но почему она должна зависеть от количества действий А, если точно известно, какое именно действие выполняется в каждом временном шаге? Чтобы определить, как можно улучшить состояние дел, вначале рассмотрим формат аксиом окружения:
Poss{a,s) =>
Fi {Result (a, s) ) (a = Ai v a = A2 ...)
v Fi(s) л (а Ф Аъ) л (а Ф A4) ...
Таким образом, в каждой аксиоме рассматриваются несколько действий, которые могут сделать это флюентное высказывание истинным, и несколько действий, которые могут сделать его ложным. Мы можем формализовать такие истинностные преобразования, введя предикат PosEffect (a, Fi), означающий, что в результате действия а флюентное высказывание Fi становится истинным, и предикат NegEЈЈect{a, Fi), означающий, что после выполнения действия а флюентное высказывание Fi становится ложным. Это означает, что приведенную выше систему аксиом можно переписать следующим образом:
Poss(a,s) =>
Fi {Result (a, s) ) <=$ PosEffect (a, Fi) v [Fi(s) л -NegEffect (a, Fi) ] PosEffect(Alt Fi) PosEffect(A2, Fi) NegEffect(Al, Fi) NegEffect(Ait Fi)
Ответ на вопрос о том, может ли такая операция формирования системы аксиом быть выполнена автоматически, зависит от точного формата аксиом окружения. Для того чтобы обеспечить использование подобных аксиом в эффективной процедуре логического вывода, необходимо провести три описанных ниже преобразования.
1. Проиндексировать предикаты PosEffect и NegEffect по их первому параметру таким образом, чтобы после получения информации о действии, которое произошло в момент времени t, можно было бы найти его результаты за время 0(1).
2. Проиндексировать аксиомы таким образом, чтобы после определения того, что Fi представляет собой результат какого-то действия, мы могли найти аксиому для Fi за время 0(1). В таком случае не придется даже рассматривать аксиомы, касающиеся тех флюентных высказываний, которые не являются результатом данного действия.
3. Представить каждую ситуацию как. предыдущую ситуацию плюс некоторая дельта. Таким образом, если ничего не изменяется от одного шага к другому, то не нужно вообще выполнять никакой работы. При использовании старого подхода требовалось выполнять объем работы 0(F), вырабатывая утверждение для каждого флюентного высказывания Fi {Result (a, s) ) из предыдущих Fi(s) утверждений.
Поэтому в каждом временном шаге мы рассматриваем текущее действие, собираем данные о его результатах и обновляем множество истинных флюентных высказываний. Среднее количество таких обновлений в каждом временном шаге соответствует F, поэтому общая сложность измеряется величиной О (Ft). В этом и состоит решение проблемы выводимого окружения.