解决表示框架问题

10.3.3 解决表示框架问题

解决表示框架问题只需要稍微改变一下关于如何写公理的观点。取代写下每个行动的效果，我们考虑每个流谓词是如何在时间上演化的[36]。我们使用的公理称为后继状态公理。它们的形式如下：

SUCCESSOR-STATE AXIOM:

行动是可能的

（结果状态中的流为真 ⇔ 行动的效应使此流为真

∨ 此流原本为真而行动没有改变它）

在不考虑不可能行动的限制下，注意这个定义使用了⇔，而不是。这意味着公理判定流为真当且仅当右侧成立。换句话说，我们将下一个状态中的每个流的真值表示为行动和当前状态下真值的一个函数。这就意味着下一个状态完全由现在的状态决定，因此就不需要额外的框架公理了。

关于智能体位置的后继状态公理告诉我们：在执行一个行动后智能体处于 y，要么行动是可能的并且由移动到y组成，要么智能体已经处于y并且行动不是移动到其它某处：

(At(Agent, y, Result(a, s)) ⇔ a = Go(x, y)

∨ (At(Agent,y, s) ∧ a ≠ Go(y, z)))

关于Holding 的公理告诉我们：在执行一个行动后，智能体将持有 g，要么行动是抓住g并且抓住是可能的，要么智能体已经持有g并且行动不是放开g：

(Holding(g, Result(a, s)) ⇔ a = Grab(g)

∨ (Holding(g, s) ∧ a ≠ Release(g)))

后继状态公理解决了表示框架问题，因为公理的总规模为O(AE)个文字：A个行动各有E种效应，每个恰好只提到了一次。这些文字分散在F条不同的公理中，所以公理的平均规模为AE / F。

细心的读者可能已经注意到这些公理处理的是智能体的At流，而不是金子的；这样我们仍然不能证明三步的规划可以达到使金子处于[1, 1]的目标。我们需要说明智能体由x移动到y有一个隐含效果（implicit effect），那就是它携带的任何金子也将移动（金子上的蚂蚁、蚂蚁上的细菌也一样，等等）。隐含效果的处理被称为分支问题（ramification problem）。我们会在以后讨论一般的分支问题，不过对于这个特定领域，可以通过为At写一个更一般的后继状态公理来解决。包容前一版本的新公理说明对象o将处于y，如果智能体走到y并且o就是智能体或是智能体持有的东西；或者o已经在y，而智能体没有走到其它地方，o是智能体或是智能体持有的东西。

(At(o, y, Result(a, s)) ⇔ (a = Go(x, y) ∧ (o = Agent ∨ Holding(o, s)))

∨ (At(o, y, s) ∧ ¬(∃z y ≠ z ∧ a = Go(y, z) ∧

(o = Agent ∨ Holding(o, s))))

还有一个技术细节：使用这些公理的推断过程必须能够证明不同一性。最简单的不同一性在常量之间——例如，Agent ≠ G1。一阶逻辑的一般语义学允许不同的常量指代同一个对象，所以知识库必须包含一条避免这种情况的公理。唯一名称公理规定了知识库中的任何一对常量具有不等性。当这一点由定理证明机假设而不是写在知识库里时，我们称之为唯一名称假设。我们同样需要规定行动项之间的不等性：Go([1, 1], [1, 2])是不同于Go([1, 2], [1, 1])或者Grab(G1)的行动。首先，我们说每种类型的行动是独特的——任何Go行动不可能是Grab行动。对任何一对名为A和B的行动，有

A(x1, …, xm) ≠ B(y1, …, yn)

接下来，我们说明同一名称的两个行动项指代同一行动，当且仅当它们涉及的对象完全相同：

A(x1, …, xm) = A(y1, …, ym) ⇔ x1= y1∧ … ∧ xm= ym

这些统称为唯一行动公理（unique action axiom）。初始状态描述、后继状态公理、唯一名称公理和唯一行动公理结合起来就足以证明提出的规划能够完成目标了。