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.

翻译：五十年前，将规划视为情境演算中的定理证明被认为是一个不可能的项目而被放弃。但我们开发了一种基于定理证明的提升启发式（TPLH）规划器，它使用A*搜索算法在情境树中搜索规划。该规划器由一个基于删除松弛的领域无关启发式函数控制。我们将TPLH与Fast Downward（FD）和Best First Width Search（BFWS）规划器在多个标准基准上进行了比较。由于我们的启发式函数实现未优化，TPLH的速度慢于FD和BFWS，但它能计算出更短的规划，并且探索的状态更少。我们讨论了关于知识表示与推理（KR&R）中规划的先前研究，并指出了相关方向。由此证明，基于演绎推理的提升启发式规划在情境演算中实际上是可行的。