Planning as Theorem Proving with Heuristics

TL;DR

This paper introduces TPLH, a theorem proving-based planner using heuristics in situation calculus, demonstrating it can produce shorter plans and explore fewer states despite being slower than some existing planners.

Contribution

We develop TPLH, a novel lifted heuristic planner based on theorem proving in situation calculus, showing its feasibility and advantages over traditional planners.

Findings

TPLH produces shorter plans than competitors.

TPLH explores fewer states during planning.

Despite slower speed, TPLH demonstrates the potential of deductive lifted heuristic planning.

Abstract

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.