Robinson第一定理
逻辑学术语
Robinson第一定理,即归结原理,在数理逻辑自动定理证明中(GOFAI涉及的主题),归结(resolution)是对于命题逻辑一阶逻辑中的句子的推理规则,它导致了一种反证法定理证明技术。
命题逻辑中的归结
归结规则
在命题逻辑中的归结规则是一个单一的有效的推理规则,从两个子句生成它们所蕴含的一个新的子句。归结规则接受包含互补的文字的两个子句 - 子句是文字的析取式,并生成带有除了互补的文字的所有文字的一个新子句。形式上,这里的和是互补的文字:
归结规则生成的子句叫做两个输入子句的归结(resolvent)。
当两个子句包含多于一对的互补文字的时候,归结规则可以(独立的)应用到每个这种文字对上。但是,只有要消去(resolve)的文字对可以去除:所有其他文字对仍保留在归结后的子句中。
一种归结技术
当外加上完备的查找算法的时候,归结规则生成一个可靠的和完备的算法来决定命题公式的可满足性,并且经过扩展,决定句子在一组公理下的有效性。
这种归结技术使用反证法,并基于在命题逻辑中的任何句子都能转换成等价的合取范式句子的事实。步骤如下:
这个算法的一个实例是最初的Davis-Putnam算法,它后来被精制成去除了对归结出的子句的显式表示的需求的DPLL算法
一阶逻辑中的归结
一阶逻辑归结把传统的逻辑推理直言三段论浓缩成了一个单一的规则。
要理解归结是如何工作的,考虑词项逻辑三段论的下列例子:
或者,更一般性的:
要使用归结技术重造推理,首先子句们必须转换成合取范式。在这种形式下,所有的量化都成为隐含的:在变量(X, Y...)上的全称量词理所当然的被省略了,而存在量化的变量被替换成Skolem函数。
所以,问题是归结技术如何从前两个子句推导出最后一个子句?规则是简单的:
要应用这个规则到上述例子,我们找到谓词P以否定形式出现在第一个子句中
并以非否定形式出现在第二个子句中
X是一个未绑定变量,而a是一个绑定变量(原子)。合一两个子句生成代换(substitution)
丢弃合一了的谓词,并把这个代换应用到余下的谓词中(在本例中就是Q(X)),生成结论:
举个其他例子,考虑三段论形式
或者更一般性的,
在合取范式中,前提变成了:
(注意在第二个子句中的变量被重命名来使在不同子句中的变量清晰的区分开来。)
现在,合一第一个子句中的Q(X)和第二个子句中¬Q(Y)意味着X和Y变成了同一个变量。把这个变量代换到余下的子句中,合并它们给出结论:
归结规则(带有额外的因数分解)同样的包容传统逻辑的所有其他的演绎形式。
参考资料
最新修订时间:2023-02-07 16:55
目录
概述
命题逻辑中的归结
参考资料