# 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

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

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.