SciTech.blog

# 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.