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，但它能计算出更短的规划，且探索的状态更少。我们讨论了知识表示与推理领域内关于规划的先前研究，并指出了相关方向。由此证明，在情境演算中进行演绎式提升启发式规划实际上是可行的。