用定理证明器构造条件计划
Constructing Conditional Plans by a Theorem-Prover
摘要：
条件规划的研究拒绝了关于规划所操作的系统的状态和变化的知识不存在不确定性或不完全性的假设，没有这些假设，实现目标的操作序列取决于系统的初始状态和不确定性变化的结果。此设置引发了如何表示计划以及如何执行计划搜索的问题。答案与简单的经典框架中的答案大不相同。在本文中，我们接近条件规划从一个新的观点，这是出于在经典规划中使用可满足性算法。由于固有的计算限制，将条件规划转换为命题逻辑中的公式是不可行的。相反，我们将条件规划转化为量化的布尔公式。我们讨论了三种形式化的条件规划量化布尔公式，并提出了实验结果与定理证明。
英文摘要：
The research on conditional planning rejects the assumptions that there is no uncertainty or incompleteness of knowledge with respect to the state and changes of the system the plans operate on. Without these assumptions the sequences of operations that achieve the goals depend on the initial state and the outcomes of nondeterministic changes in the system. This setting raises the questions of how to represent the plans and how to perform plan search. The answers are quite different from those in the simpler classical framework. In this paper, we approach conditional planning from a new viewpoint that is motivated by the use of satisfiability algorithms in classical planning. Translating conditional planning to formulae in the propositional logic is not feasible because of inherent computational limitations. Instead, we translate conditional planning to quantified Boolean formulae. We discuss three formalizations of conditional planning as quantified Boolean formulae, and present experimental results obtained with a theorem-prover.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
