Last Update: 24 November 2008, 3:31 p.m.
Note: or material is highlighted
using some of the notation of:
Suppose that there is a robot that can do the following actions on blocks:
Let Do(A,s) =def Do(A_n, Do(A1;...;A_n-1,s)).
Let KB contain descriptions of initial situation s1, the effect axioms, the definition of Do, etc.
Let φ(x,s) be a proposition expressing the goal situation.
Then "the planning problem" is to find A such that KB ||- &phi(x, Do(A,s))
& suppose φ = On(a,c,s1).
Then a plan is: A = Unstack(b,a); Stack(a,c).
I.e., show KB ||- On(a,c, Do(A,s1)).
From II(2), can infer: Clear(a, Do(Unstack(b,a),s1)).
From I(3), the above "Clear" proposition, & II(1), we would like to infer:
But to infer that, we need:
But, from the fact that c is initially clear, we cannot infer that it remains clear!
That is the frame problem!