# Planning as Theorem Proving with Heuristics

arXiv: https://arxiv.org/abs/2303.13638 · HTML: https://mlsanity.com/paper/2303.13638/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 109 references that are in the map.
- First posted on arXiv 23 Mar 2023.

## Builds on (most cited first, 6 of 6)

- [The LAMA Planner: Guiding Cost-Based Anytime Planning with Landmarks](https://mlsanity.com/paper/1401.3839/) (2014)
- [Answer Set Planning: A Survey](https://mlsanity.com/paper/2202.05793/) (2022)
- [Bounded Situation Calculus Action Theories](https://mlsanity.com/paper/1509.02012/) (2015)
- [plasp 3: Towards Effective ASP Planning](https://mlsanity.com/paper/1812.04491/) (2018)
- [Planning as Tabled Logic Programming](https://mlsanity.com/paper/1507.03979/) (2015)
- [A Logical Semantics for PDDL+](https://mlsanity.com/paper/2111.11588/) (2021)

## Built on by (most cited first, 1 of 1)

- [Planning with Dynamically Changing Domains](https://mlsanity.com/paper/2508.02697/) (2025)

## Abstract (arXiv)

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.