归结原理
归结（resolution）原理，在数理逻辑和自动定理证明中（GOFAI涉及的主题），是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。
命题逻辑中的归结
归结规则
在命题逻辑中的归结规则是一个单一的有效的推理规则，从两个子句生成它们所蕴含的一个新的子句。归结规则接受包含互补的文字的两个子句 - 子句是文字的析取式，并生成带有除了互补的文字的所有文字的一个新子句。形式上，这里的 和 是互补的文字：
归结规则生成的子句叫做两个输入子句的归结（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）
归结规则（带有额外的因数分解）同样的包容传统逻辑的所有其他的演绎形式。
Paramodulation
Paramodulation是一种相关技术，用于推理条款集，其中谓词变量是平等的。它可以生成所有 "相等 "的子句，但反身的相同性除外。参数化操作需要一个正的从子句，它必须包含一个平等字面。然后，它搜索一个 "进入 "子句，该子句与平等关系的一方相统一。然后，该子项被等号的另一边所取代。Paramodulation的一般目的是将系统简化为原子，在替换时减少术语的大小。[1]
参考文献
- Robinson, J. Alan. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. 1965, 12 (1): 23–41. doi:10.1145/321250.321253.
- Leitsch, Alexander. The Resolution Calculus. Springer. 1997.
- Gallier, Jean H. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers. 1986 [2018-08-16]. （原始内容存档于2018-08-08）.
- Lee, Chin-Liang Chang, Richard Char-Tung. Symbolic logic and mechanical theorem proving [reprint]. San Diego: Academic Press. 1987. ISBN 0-12-170350-9.
Approaches to non-clausal resolution, i.e. resolution of first-order formulas that need not be in clausal normal form, are presented in:
- D. Wilkins. QUEST — A Non-Clausal Theorem Proving System (学位论文). Univ. of Essex, England. 1973.
- Neil V. Murray. A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. Feb 1979 [2018-08-16]. 2-79. （原始内容存档于2020-06-07）. (Cited from Manna, Waldinger, 1980 as: "A Proof Procedure for Non-Clausal First-Order Logic", 1978)
- Zohar Manna, Richard Waldinger. A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems. Jan 1980, 2: 90–121 [2018-08-16]. doi:10.1145/357084.357090. （原始内容存档于2017-09-27）. A preprint appearead in Dec 1978 as SRI Technical Note 177 （页面存档备份，存于互联网档案馆）
- N. V. Murray. Completely Non-Clausal Theorem Proving. Artificial Intelligence. 1982, 18: 67–85. doi:10.1016/0004-3702(82)90011-x.
- Schmerl, U.R. Resolution on Formula-Trees. Acta Informatica. 1988, 25: 425–438. doi:10.1007/bf02737109. Summary （页面存档备份，存于互联网档案馆）
外部链接
- Resolution Principle （页面存档备份，存于互联网档案馆）
- Resolution （页面存档备份，存于互联网档案馆）
- ^ Nieuwenhuis, Robert; Rubio, Alberto. Paramodulation-Based Theorem Proving. Handbook of Automated Reasoning (PDF). [2022-03-21]. （原始内容 (PDF)存档于2021-12-31）.