【摘要】：一阶逻辑子句的归结规则简单而言只是第7.5.1节给出的命题归结规则的一个提升版本。例如，通过合一者θ={u/G,v/x}消除互补文字Loves和Loves(u,v)，我们可以对两个子句进行归结[Animal∨Loves] 和 [Loves∨Kills]刚刚给出的规则是二元归结规则，因为它正好对两个文字进行归结。二元归结规则自身不能得到一个完备的推理过程。全归结规则对每个可合一的子句中的文字子集进行归结。合一者必须应用于整个子句。
9.5.2 归结推理规则
一阶逻辑子句的归结规则简单而言只是第7.5.1节给出的命题归结规则的一个提升版本。假设两个子句已经标准化分离，因此它们没有共享变量，那么如果包含互补文字，则它们是可归结的。如果一个命题文字是另一个命题文字的否定式，则这两个命题文字是互补的；如果一个一阶逻辑文字能和另一个一阶逻辑文字的否定式合一，则这两个一阶逻辑文字是互补的。因此，我们可以得到
其中UNIFY(li,¬mj)=θ。例如，通过合一者θ={u/G(x),v/x}消除互补文字Loves(G(x),x)和¬Loves(u,v)，我们可以对两个子句进行归结
[Animal(F(x))∨Loves(G(x), x)] 和 [¬Loves(u, v)∨¬Kills(u, v)]
产生归结式子句
[Animal(F(x))∨¬Kills(G(x), x)]
刚刚给出的规则是二元归结规则，因为它正好对两个文字进行归结。二元归结规则自身不能得到一个完备的推理过程。全归结规则对每个可合一的子句中的文字子集进行归结。另外的一种方法就是把归并——去除冗余文字——扩展到一阶逻辑的情况。命题逻辑的归并是如果两个文字相同，则将这两个文字减少到一个；一阶逻辑的归并是如果两个文字可合一，则将这两个文字减少到一个。合一者必须应用于整个子句。二元归结和归并的结合都是完备的。
免责声明：以上内容源自网络，版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。
