A Proof System for Unsolvable Planning Tasks
A Proof System for Unsolvable Planning Tasks
复制标题
无法解决的规划任务的证明系统
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
M. Helmert
中科院分区：
文献类型：
--
作者：
Salomé Eriksson;Gabriele Röger;M. Helmert
虽然传统的经典规划集中在寻找计划的可解决的任务，检测不可解决的情况，最近吸引了越来越多的兴趣。为了排除错误的结果，期望规划系统提供可以独立验证的不可解性证书。我们提出了一个基于规则的证明系统的不可解性证明建立了一个知识库的可验证的基本语句，并应用一组推导规则来推断这些语句的任务的不可解性。我们认为，这种方法是更灵活的比最近提出的感应证书的不可解性，并展示了我们的证明系统可以用于广泛的规划技术。
While traditionally classical planning concentrated on finding plans for solvable tasks, detecting unsolvable instances has recently attracted increasing interest. To preclude wrong results, it is desirable that the planning system provides a certificate of unsolvability that can be independently verified. We propose a rule-based proof system for unsolvability where a proof establishes a knowledge base of verifiable basic statements and applies a set of derivation rules to infer the unsolvability of the task from these statements. We argue that this approach is more flexible than a recent proposal of inductive certificates of unsolvability and show how our proof system can be used for a wide range of planning techniques.