Tractable Reasoning in First-Order Knowledge Bases with Disjunctive Information
Tractable Reasoning in First-Order Knowledge Bases with Disjunctive Information
复制标题
具有析取信息的一阶知识库中的易处理推理
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
H. Levesque
中科院分区：
文献类型：
--
作者：
Yongmei Liu;H. Levesque
这项工作提出了一种新的方法来建立处理表达性一阶知识库的推理服务的易处理性。它包括定义一个比经典逻辑弱的逻辑，它具有两个性质：第一，蕴涵问题可以简化为少量特征模型的模型检查问题；其次，对于具有有限数量变量的公式，模型检查问题本身很容易处理。我们展示了这种方法在 Liu、Lakemeyer 和 Levesque 之前提出的处理分离信息的推理服务中的实际应用。他们表明，他们的推理在命题情况下是易于处理的，在一阶情况下是可判定的。在这里，我们应用该方法并证明，如果知识库和查询都使用有限数量的变量，则在一阶情况下推理也是易于处理的。
This work proposes a new methodology for establishing the tractability of a reasoning service that deals with expressive first-order knowledge bases. It consists of defining a logic that is weaker than classical logic and that has two properties: first, the entailment problem can be reduced to the model checking problem for a small number of characteristic models; and second, the model checking problem itself is tractable for formulas with a bounded number of variables. We show this methodology in action for the reasoning service previously proposed by Liu, Lakemeyer and Levesque for dealing with disjunctive information. They show that their reasoning is tractable in the propositional case and decidable in the first-order case. Here we apply the methodology and prove that the reasoning is also tractable in the first-order case if the knowledge base and the query both use a bounded number of variables.