Classical AI Planning as Theorem Proving: The Case of a Fragment of Linear Logic
Classical AI Planning as Theorem Proving: The Case of a Fragment of Linear Logic
复制标题
作为定理证明的经典人工智能规划：线性逻辑片段的案例
DOI：
--
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
Éric Jacopin
中科院分区：
文献类型：
--
作者：
Éric Jacopin
本文试图评估在线性逻辑的乘法片段中定理证明器的使用，该线性逻辑已被证明可以模拟合取带式规划9]。证明搜索过程是正确的，完整的，只生成线性证明（即不是树）。可以从证明中提取的计划要么是完全有序的，要么是部分有序的。该程序进行了测试，对带状规划和结果。然而，由于线性逻辑是一种将公式视为数据类型的资源敏感逻辑，因此在线性逻辑中不可能部分描述最终情况;并且在这里呈现的片段中不可能共享后置条件。然后，有人认为，这些限制最终使线性逻辑的片段，尽管其正式的框架，有点无用的实际规划的目的。
This paper attempts to evaluate the use of a theorem prover in the multiplicative fragment of linear logic which has been shown to simulate conjunctive Strips-like planning 9]. A proof search procedure is presented that is correct, complete and only generates linear proofs (i.e. not trees). Plans that can be extracted from proofs are either totally or partially ordered. The procedure is tested against Strips-like planners and results are given. However, since linear logic is a resource-sensitive logic viewing formulas as data types, partial description of the nal situation are impossible in linear logic; and shared postconditions are impossible in the fragment presented here. It is then argued that these restrictions eventually makes the presented fragment of linear logic, despite its formal framework, somewhat useless for practical planning purposes.