A deductive solution for plan generation
A deductive solution for plan generation
复制标题
计划生成的演绎解决方案
作者：
W. Bibel
本文提出了一种求解机器人问题的新的演绎方法。用逻辑公式描述初始和目标情况。原始动作由规则描述，即。e.逻辑公式也是。总而言之，这导致了像逻辑编程或程序综合中的问题描述。一个解决方案是由这个描述的证明生成的，就像在程序合成中一样，只是这里的证明必须是严格线性的。这个限制是我们解决方案的线索;它可以很容易地作为一个选项添加到任何定理证明器中，例如基于下面使用的连接方法的证明器。事实上，这种限制大大加快了证明搜索的速度。同时，我们的方法为框架问题提供了一个优雅的解决方案。
A new deductive method for solving robot problems is presented in this paper. The descriptions of initial and goal situations are given by logical formulas. The primitive actions are described by rules, i. e. logical formulas as well. Altogether this results in a problem description like in logic programming or in program synthesis. A solution is generated by a proof of this description like in program synthesis, except that here proofs have to be strictly linear. This restriction is the clue of our solution; it can be easily added as an option to any theorem prover such as one based on the connection method used hereafter. In fact this restriction speeds up the proof search considerably. At the same time our approach offers an elegant solution of the frame problem.