根据上一小节中我们对人类推理特点做出的分析，要想用计算机模拟人类的推理过程， 可行的方案就是采用反向演绎的推理方法。
反向演绎从待证目标出发，因此能够避免在推理的每一步都产生大量的无用事实，但在规则量很大时，仍然需要逐一计算规则的匹配，非常缓慢低效。
该问题在 1965 年，由 Robinson 提出归结原理后得以解决。归结原理也因此成为自动定理证明的理论基础。其本质与反向演绎类似，同样从待证目标出发，只是，归结原理采用的是反证法。
归结原理用于自动推理
• 归结原理如何用于自动推理呢？答案是，用反证法。为了解释这个过程，我们先看几条前提假设。
– （1）证明一个命题 P 成立，等价于证明其逆命题 ¬P 不成立。
– （2）一个已知为真的事实集，其内部不包含矛盾。
– （3）如果将一个命题加入事实集，并且导致事实集出现矛盾，则原命题不成立。
– （4） 常见的矛盾形式，是 ：P ∧ ¬P =>□ 一旦事实集中出现空符号□，则认为事实集中存在矛盾。
归结原理用于自动推理
• 有了上面几条假设，我们可以设想，从目标的待证命题出发：
– 将待证命题 P 取逆命题，
– 将逆命题 ¬P 作为“事实”加入已知为真的事实集中，
– 如果我们在这样的事实集中推导出 □，则该事实集存在矛盾，
– 则证明逆命题 ¬P 不成立，命题 P 成立
• 如何推导出□呢？这里利用了归结原理。
– 归结原理是在一个事实集中导出矛盾的 快方式，每归结一步，事实集都在简化而不是变复杂。这就有利于□的推导。
– 另外，归结原理的目标单一，只要在事实集中推导出□，问题就解决，而与具体证明问题无关，因此是一个通用方法。
归结推理的自动化问题
• 至此我们初步建立起用归结原理实现定理证明的完整框架，包括：
–用标准谓词子句形式建立知识库
–用反证法，从待证目标开展推理
–用归结原理，尝试寻找知识库中的□
• 但这个过程还不是自动化的。还缺少一个环节：
–如何在知识库选择正文字、负文字进行消解。
–目前由人工来选择，且不同的选择方式，会导致推理效率存在差异。
–如果有某种方法可以自动化文字选择过程，则整个证明就可以自动化了。
