Planning as abduction

24 Feb 2018, 07:14 • logic

Automated planning is the task of finding a plan to achieve a goal given some prerequisites. Planning problems can be cast in terms of abductive theories which allows us to use an abductive prover to find the best plan.

A planning problem consists of a description of the initial state, the desired goal state and a set of actions an agent can perform to manipulate the state. For example, the initial state might be

\[ monkeyAt(l_1,0) \land bananaAt(l_5,0) \]

and the goal state might be

\[ monkeyEatsBanana(t) \]

for some time t. The actions to achieve that goal might be something like

\[ \begin{array}{c} monkeyAt(l_i,t) \leadsto monkeyAt(l_{i+1},t+1) \\ monkeyAt(l_i,t) \leadsto monkeyAt(l_{i-1},t+1) \\ monkeyAt(l_i,t) \land bananaAt(l_i,t) \leadsto monkeyAt(l_i,t+1) \land monkeyEatsBanana(t+1) \\ \end{array} \]

These intuitive rules represent the actions the agent (monkey) can perform at sometime t. Note that if we replace \(\leadsto\) with \(\supset\), we get an abductive theory. However, we also need to provide rules that "do nothing" as time flows by, such as

\[ bananaAt(l,t) \supset bananaAt(l,t+1) \]

Finding a plan is now simply finding an abductive proof. The set of observables is the goal and a valid plan is represented by a proof that makes the initial state true. It's easy to see that due to how abductive reasoning works, there's a one-to-one correspondence between proofs and plans. Moreover, since the observables are all ground, the abductive task is effectively propositional.