Robinson第一定理，即归结原理，在数理逻辑和自动定理证明中（GOFAI涉及的主题），归结（resolution）是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。
基本介绍
- 中文名：Robinson第一定理
- 外文名：J.A. Robinson's resolution Principle
- 别称：归结原理
- 提出者：J.A. Robinson
命题逻辑中的归结
归结规则
在命题逻辑中的归结规则是一个单一的有效的推理规则，从两个子句生成它们所蕴含的一个新的子句。归结规则接受包含互补的文字的两个子句 - 子句是文字的析取式，并生成带有除了互补的文字的所有文字的一个新子句。形式上，这里的
和
是互补的文字：
归结规则生成的子句叫做两个输入子句的归结（resolvent）。
当两个子句包含多于一对的互补文字的时候，归结规则可以（独立的）套用到每个这种文字对上。但是，只有要消去（resolve）的文字对可以去除：所有其他文字对仍保留在归结后的子句中。
一种归结技术
当外加上完备的查找算法的时候，归结规则生成一个可靠的和完备的算法来决定命题公式的可满足性，并且经过扩展，决定句子在一组公理下的有效性。
这种归结技术使用反证法，并基于在命题逻辑中的任何句子都能转换成等价的合取範式句子的事实。步骤如下：
- 在知识库中所有句子和要证明的句子（猜测（conjecture）)的否定都合取连结。
- 结果的句子变换成合取範式（处理成一组子句）。
- 把归结规则套用到包含互补的文字的所有可能的子句对，通过除去重複的文字来简化结果的句子。如果句子包含互补的文字，则（作为重言式）丢弃它。如果没有，并且它在子句的集合中仍然不存在，则增加上它，并考虑做进一步的归结推理。
- 如果在套用归结规则之后推导出空子句，则全部的公式是不可满足的（或者说矛盾的），所以可以做出最初的猜测从这些公理中推出的结论。
- 在另一方面，如果不能推导出空子句，并且不能套用归结规则推导更多的新子句，则这个猜测不是最初的知识库的定理。
这个算法的一个实例是最初的Davis-Putnam算法，它后来被精製成去除了对归结出的子句的显式表示的需求的DPLL算法。
一阶逻辑中的归结
一阶逻辑归结把传统的逻辑推理的直言三段论浓缩成了一个单一的规则。
要理解归结是如何工作的，考虑词项逻辑三段论的下列例子：
- 所有希腊人都是欧洲人，
- 荷马是希腊人，
- 所以，荷马是欧洲人。
或者，更一般性的：
- ∀X, P（X）→ Q（X），
- P（a），
- 所以, Q（a）。
要使用归结技术重造推理，首先子句们必须转换成合取範式。在这种形式下，所有的量化都成为隐含的：在变数（X, Y...）上的全称量词理所当然的被省略了，而存在量化的变数被替换成Skolem函式。
- ¬P（X）∨ Q（X），
- P（a），
- 所以, Q（a）。
所以，问题是归结技术如何从前两个子句推导出最后一个子句?规则是简单的：
- 找到包含相同谓词的两个子句，这个谓词在一个子句中是否定的而在另一个子句中是肯定的。
- 在两个谓词上进行合一。（如果合一失败，则你做了错误的谓词选择，回到前面的步骤再次尝试。）
- 如果在被合一的谓词中受到约束的任何未绑定的变数也出现这两个子句中的其他谓词中，则同样的把它们替换（replace）成它们的绑定值（项）。
- 丢弃被合一的谓词，併合并两个子句中的余下的谓词到一个新子句中，并用"∨"运算元连线起来。
要套用这个规则到上述例子，我们找到谓词P以否定形式出现在第一个子句中
- ¬P（X）。
并以非否定形式出现在第二个子句中
- P（a）。
X是一个未绑定变数，而a是一个绑定变数（原子）。合一两个子句生成代换（substitution）
- X:= a。
丢弃合一了的谓词，并把这个代换套用到余下的谓词中（在本例中就是Q（X）)，生成结论：
- Q（a）。
举个其他例子，考虑三段论形式
- 所有克里特岛人都是岛上居民，
- 所有岛上居民都是说谎者，
- 所以，所有克里特岛人都是说谎者。
或者更一般性的,
- ∀X P (X) → Q（X），
- ∀X Q (X) → R（X），
- 所以, ∀X P (X) → R（X）。
在合取範式中，前提变成了：
- ¬P（X）∨ Q（X），
- ¬Q（Y）∨ R（Y）。
（注意在第二个子句中的变数被重命名来使在不同子句中的变数清晰的区分开来。）
现在，合一第一个子句中的Q（X）和第二个子句中¬Q（Y）意味着X和Y变成了同一个变数。把这个变数代换到余下的子句中，合併它们给出结论：
- ¬P（X）∨ R（X）。
归结规则（带有额外的因数分解）同样的包容传统逻辑的所有其他的演绎形式。