An Inference Rule for Hypothesis Generation
An Inference Rule for Hypothesis Generation
复制标题
假设生成的推理规则
DOI：
--
复制
发表时间：
1991
期刊：
影响因子：
--
通讯作者：
L. F. D. Cerro
中科院分区：
文献类型：
--
作者：
R. Demolombe;L. F. D. Cerro
自动推理有许多新的应用领域，我们必须应用溯因推理。在这些应用中，我们必须产生具有某些适当性质的给定理论的结果。特别是，我们考虑的情况下，我们必须生成的条款包含一个给定的文字L的实例。在这样的子句中对其他文字的否定是允许导出L的假设。
在本文中，我们提出了一个推理规则，称为L-推理，这是为了推导出这些条款，和L-策略。L-推理规则是一种输入超分辨。本文的主要结果是证明了L-推理规则的可靠性和完备性。与L-推理规则相关联的L-策略是通过删除重言式和所包含的分句而达到的水平饱和。我们证明L策略也是完全的。
There are many new application fields for automated deduction where we have to apply abductive reasoning. In these applications we have to generate consequences of a given theory having some appropriate properties. In particular we consider the case where we have to generate the clauses containing instances of a given literal L. The negation of the other literals in such clauses are hypothesis allowing to derive L.
In this paper we present an inference rule, called L-inference, which was designed in order to derive those clauses, and a L-strategy. The L-inference rule is a sort of Input Hyper-resolution. The main result of the paper is the proof of the soundness and completeness of the L-inference rule. The L-strategy associated to the L-inference rule, is a saturation by level with deletion of the tautologies and of the subsumed clauses. We show that the L-strategy is also complete.