Planning as Theorem Proving with Heuristics
This work revives a long-abandoned approach to planning for AI researchers, showing it is feasible but is incremental as it builds on existing heuristic methods.
The authors tackled the problem of planning as theorem proving in situation calculus, which was considered impossible for 50 years, by developing the TPLH planner that uses A* search with a delete relaxation-based heuristic; it computes shorter plans and explores fewer states than Fast Downward and BFWS, though it is slower due to unoptimized implementation.
Planning as theorem proving in situation calculus was abandoned 50 years ago as an impossible project. But we have developed a Theorem Proving Lifted Heuristic (TPLH) planner that searches for a plan in a tree of situations using the A* search algorithm. It is controlled by a delete relaxation-based domain independent heuristic. We compare TPLH with Fast Downward (FD) and Best First Width Search (BFWS) planners over several standard benchmarks. Since our implementation of the heuristic function is not optimized, TPLH is slower than FD and BFWS. But it computes shorter plans, and it explores fewer states. We discuss previous research on planning within KR\&R and identify related directions. Thus, we show that deductive lifted heuristic planning in situation calculus is actually doable.