Решение проблемы представительного окружения
Для решения проблемы представительного окружения достаточно лишь немного изменить точку зрения на то, как следует записывать аксиомы. Вместо регистрации результатов каждого действия мы будем рассматривать, как каждый флюентный предикат развивается во времени2. Применяемые при этом аксиомы называются аксиомами состояния-преемника. Они имеют следующую форму: Аксиома состояния-преемника: Действие возможно =>
(Флюентное высказывание является истинным в
результирующем состоянии <==> Оно стало истинным в результате действия v оно было истинным и прежде, а действие оставило его неизменным)
Пояснив, что мы не рассматриваем невозможные действия, хотим обратить внимание читателя на то, что в приведенном выше определении используется логическая связка а не =>. Таким образом, в этой аксиоме указано, что данное флюентное высказывание будет истинным тогда и только тогда, когда выполняется его правая часть. Иными словами, истинностное значение каждого флюентного высказывания в следующем состоянии определено как функция действия и истинностного значения в текущем состоянии. Это означает, что следующее состояние полностью задано текущим состоянием и поэтому нет необходимости использовать дополнительные аксиомы окружения.
В аксиоме состояния-преемника для местонахождения агента утверждается, что агент находится в квадрате у после выполнения некоторого действия, либо если это действие было возможным и заключалось в перемещении в квадрат у, либо если агент уже находился в квадрате у и его действие не заключалось в том, чтобы перемещаться куда-то в другое место:
Poss{a, s) =>
{At(Agent, у, Result{a,s)) <=$ а = Go{x, у)
v {At{Agent, у, s) л а Ф Go(у, z)))
В аксиоме для флюентного предиката Holding утверждается, что агент владеет золотом д после выполнения некоторого действия, если этим действием было схватывание золота д и такое схватывание было возможно или если агент уже владел золотом д и выполненное агентом действие не заключалось в отпускании золота:
Poss{a, s) =>
{Holdingig, Result (a, s) ) а = Grab(g)
v {Holding(g, s) л а Ф Release(g)))
«3е Аксиомы состояния-преемника позволяют решить проблему представительного окружения, поскольку общий размер этих аксиом измеряется величиной в О(АЕ) литералов: каждый из Е результатов каждого из А действий упоминается один и только один раз. Литералы распределяются по F разным аксиомам, поэтому аксиомы имеют средний размер AEIF.
Внимательный читатель должен был заметить, что в этих аксиомах участвует флюентное высказывание At, касающееся агента, но не золота, поэтому мы все еще не можем доказать, что приведенный выше трехшаговый план позволяет достичь цели — переноса золота в квадрат [1,1]. Мы должны указать, что неявным результатом перемещения агента из квадрата х в квадрат у является то, что переместится также все золото, которое он несет (а также все муравьи, которые заползли в это золото, все пылинки и бактерии на этих муравьях и т.д.). Учет таких неявных результатов связан с решением так называемой проблемы распространения последствий (ramification problem). Более подробно мы рассмотрим эту проблему позже, но для данной конкретной проблемной области ее можно решить, дописав более общую аксиому состояния-преемника для высказывания At. В новой аксиоме, которая обобщает предыдущую версию, утверждается, что объект о находится в квадрате у, либо если агент перешел в квадрат у и о — это или агент, или то, что держит агент, либо если объект о уже находился в квадрате у и агент никуда не переходил, притом что о является или агентом, или тем, что держит агент.
Poss{a,s) =>
At {о, у, Result {a, s)) {a = Go{x, у) л (о = Agent v Holdingio, s) ) )
v {At(o, y, s) л —i(3z у Ф z A a = Go{y, z) л (о = Agent v Holdingio, s) )) )
Возникает еще одна формальная сложность: процесс логического вывода, в котором используются эти аксиомы, должен позволять доказывать неравенства. Простейшего рода неравенство задается между константами, например AgentG Общая семантика логики первого порядка допускает, чтобы разные константы ссылались на один и тот же объект, поэтому база знаний должна включать какую-то аксиому, позволяющую предотвратить такую ситуацию. В аксиоме уникальных имен (unique names axiom) провозглашается неравенство для каждой пары констант в базе знаний. Если же это условие подразумевается в программе автоматического доказательства теорем, а не записывается в базу знаний, то называется предположением об уникальности имен (unique names assumption). Необходимо также сформулировать условие неравенства между термами действий, например, утверждение о том, что Go ([1,1], [1,2])— это действие, отличное от Go ( [ 1, 2 ] , [ 1,1 ] ) или Grab (Gx). Прежде всего необходимо указать, что каждый тип действия является различным, т.е., например, что действие Go — это не действие Grab. Для каждой пары имен действий Айв необходимо иметь:
A{xlt ...,xm) Ф B(yi, ...,уп)
Затем требуется указать, что два терма действия с одним и тем же именем действия ссылаются на одно и то же действие тогда и только тогда, когда все участвующие в них объекты являются одинаковыми:
A(xi, ..., хт) = A(yi, ... ,ут) О Xi = yi л ... л хт = ут
Все эти аксиомы, вместе взятые, называются аксиомами уникального действия (unique action axiom). Такая комбинация описания начального состояния, аксиом состояния-преемника, аксиом уникальности имен и аксиом уникального действия является достаточной для доказательства того, что предлагаемый план позволяет достичь цели.