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.

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