猴子摘香蕉问题是一个典型的规划问题,下面要介绍的就是如何用归结法求解规划问题的方法。从方法上来说,用归结法求解规划问题并没有什么特殊性,采用的还是提取问题的答案的方法。也就是说,通过修改证明树,获取问题的答案。我们希望该答案得到的就是规划问题的解。为此,巧妙的在谓词表达式中引入一个状态项s,该状态可以表示猴子在做了一个动作之后系统所处于的状态。同时还引入了pushbox(x,s)、climbbox(s)和grasp(s)三个函数,分别表示在状态s下,猴子将箱子推到x位置、猴子爬到箱子上和猴子摘香蕉三个动作。用ONBOX(s)、AT(x,y,s)和HB(s)三个谓词分别表示在状态s下,猴子是否在箱子上、x是否在y位置和猴子是否摘到了香蕉。
这样,当问题简化为a=b时(即初始状态下认为猴子和箱子在同一个位置),问题可以用谓词描述为:
(1)初始状态下,"猴子不在箱子上",表示为:
~ONBOX(
(2)对于任何状态s和任何位置x,如果在状态s下"猴子不在箱子上(~ONBOX(s))",则经过动作"把箱子推到位置x(pushbox(x,s))"后的下一个状态,"箱子在x处(AT(box,x,pushbox(x,s)))"。表示为:
( x)( s)(~ONBOX(s)→AT(box,x,pushbox(x,s)))
注意:这里已经假设了猴子与箱子在同一个位置(即a=b的情况)。
(3)对于任何状态s,如果在状态s下,猴子在经过动作"爬上箱子(climbbox(s))"后的下一个状态,猴子就在箱子上了。表示为:
s)(ONBOX(climbbox(s)))
(4)对于任何一个状态s,如果在状态s下,"猴子在箱子上(ONBOX(s))",并且"箱子在c处(AT(box,c,s))",则经过"猴子摘香蕉(grasp(s))"动作后的下一个状态,"猴子摘到了香蕉(HB(grasp(s)))"。表示为:
s)((ONBOX(s)∧AT(box,c,s))→HB(grasp(s)))
(5)对于任何一个状态s和任何一个位置x,如果在状态s下,"箱子在x处(AT(box,x,s))",则猴子在经过动作"爬上箱子(climbbox(s))"之后的下一个状态,"箱子还在x处(AT(box,x,climbbox(s)))"。表示为:
x)(s)(AT(box,x,s)→AT(box,x,climbbox(s)))
(6)求解的目标就是:存在一个状态s,在该状态下,猴子摘到了香蕉。即:
s)HB(s)
  有了以上表示方法后,采用基于归结的提取回答的方法,通过修改证明树,可以得到问题的解答为HB(grasp(climbbox(pushbox(c, s0))))。该解答告诉我们猴子摘香蕉问题的行为序列为:(1)猴子把箱子推到c处;(2)猴子爬到箱子上;(3)猴子摘香蕉。
图4.20给出了该问题的修改证明树。

下面介绍一种基于归结的提取回答方法用于求解猴子摘香蕉问题的方法。为此在谓词中引入状态项s,以说明谓词应用的具体状态条件,如把初始状态的公式集表示为:
{~ONBOX(s0), AT(box, b, s0), AT(monkey, a, ), ~HB()}
此外对规则也必须按谓词演算的体系进行形式化描述,如对grasp(s)的作用要用如下的合式公式表示:
s)(ONBOX(s)∧AT(box, c, s)→HB(grasp(s)))
其含义是对任何一个状态s,若猴子在箱子上,且箱子处在c点处,那么在s状态下应用grasp操作的情况下,猴子就拿到了香蕉。
下面以一个简单的初始状态a=b和只需要三条规则的情况来说明如何形式化,并应用提取回答过程进行求解的方法。这时初始状态公式集为
{~ONBOX(), AT(box, b, ), AT(monkey, b, ), ~HB()}
可简化为~ONBOX(),于是有
(1)~ONBOX(
(2)(x)(s)(~ONBOX(s)→AT(box, x, pushbox (x, s)))
(3)(s)(ONBOX(climbbox(s)))
(4)(s)((ONBOX(s)∧AT(box, c, s))→HB(grasp (s)))
(5)(x)(s)(AT(box, x, s)→AT(box, x, climbbox(s)))
(6)(s)HB(s)
公式组中,(1)是初始状态,(6)是目标公式,(2)-(4)是规则描述公式,(5)是推理公理,表示猴子爬上箱子时,箱子的位置仍然不变,当然还可以引入其他的推理公理。
为了用归结法证明目标公式,把它们公为子句表示形式:
(1)~ONBOX(
(2)ONBOX(s1)∨AT(box, x1, push(x1, s1))
(3)ONBOX(climbbox(s2))
(4)~ONBOX(s3)∨~AT(box, c, s3)∨HB(grasp(s3))
(5)~AT(box, x4, s4)∨AT(box, x4, climbbox(s4))
(6)~HB(S5)