2.2.5 归结原理的改进策略
2.2.5.1 语义归结
子句集S 的子集 T 称为 S 的支撑集，如果 S－T 是可满足的。一个支撑集归结是一个不同时属于 S－T 的两个子句的归结。支撑集归结式 L. Wos, J.A. Robinson 和 D.F.Carson 于 1965 年提出[80] 。这种策略的思想比较直观：在一阶逻辑中证明 A1,...,An 共同蕴涵 B，即证明 (A1...An)B 为恒真公式，归结方法是去证明 A1...AnB 是不可满足的。通常，前提集合{A1,...,An}是可满足的。因此，要找出矛盾
（即空子句），避免在{A1,...,An}中的子句进行归结是明智的。这就是支撑集归结的来源。支撑集归结是完备的。
与支撑集归结的思想相似，语义归结[81] 的核心思想是通过一个解释 I，在解释 I 下输入子句集 S 一定会被划分为非空的两个子集：被满足的子句子集 S1 和被弄假的子句子集 S2。语义归结要求进行归结的两个子句只能来源于不同的子集。语义归结中也对谓词符号进行排序，在应用归结方法时要求只能应用在子句中最大的谓词符号上。当解释I 中只有正文字（或者负文字）时，语义归结又被称为正超归结（或者负超归结）。语义归结和超归结都是完备的。
2.2.5.2 Horn 集上的归结原理
单元归结：归结的两个子句中有一个单文字子句。输入归结：归结的两个子句中有一个子句来自最初给定的子句集合 S。若一个演绎中的每个归结步骤都是单元（输入）归结，则称之为单元（输入）演绎。
存在从子句集S 推出空子句的单元演绎当且仅当存在从子句集S推出空子句的输入演绎。单元归结和输入归结这样好的推理方法，却是不完备的，例如前面的例 1。然而，对于一类特殊子句集，Horn 集是完备的。Horn 集虽然特殊，却用途广泛。
如果一个子句中最多有一个正文字，则称此子句为 Horn 子句；由 Horn 子句构成的子句集，称为 Horn 集。如下一个 Horn 集
{A1A2A3B1,A4A5B2,PQ,A1,A4,P}恰好描写了如下一组知识：
(1) A1
(2) A4
(3) P
(4) A1A2A3B1
(5) A4A5B2
(6) PQ
其中前三条公式描述了事实，后三条公式描述了规则。Horn 集描
述的知识（事实与规则）恰好是知识工程中经常使用的知识表示方法。因此，针对 Horn 集上归结方法有许多研究工作与改进成果。例如，前述提到的单元归结与输入归结是不完备的。即对于普通的不可满足子句集，仅使用单元演绎或者输入演绎最后未必能推导出空子句。但是单元归结与输入归结对 Horn 集是完备的。设 S 是不可满足的 Horn集，于是存在从 S 推出空子句的输入演绎和单元演绎。
2.2.5.3 广义归结
应用归结原理证明谓词公式 G 不可满足时，需要先得到 G 的 Skolem 范式，这种范式的母式是合取范式，首标中只有全称量词。因此，归结方法的输入是来自合取范式中的子句构成的集合，子句中出现的变量均是受全称量词限制。求 Skolem 范式的过程繁琐费时，研究者们试着避开这一环节。
1979 年王湘浩、刘叙华提出了广义归结方法，1982 年发表于《计算机学报》[101] ；同年， N. V. Murray 在国际权威期刊 Artificial Intelligence(AIJ)发表论文，提出一种非子句形式的 NC 归结方法[85] 。 1992 年，刘叙华和孙吉贵研究、比较了广义归结和 NC 归结，证明了：NC 归结对于锁归结、有序归结、语义归结和线性半锁归结都是不完备的，并指出 Murray 论文中的错误。刘叙华在其专著[102] 中指出：不论是由复杂文字组成的子句的归结(T. Bollinger 在 IJCAI-91 上发表的论文[103] )，还是 NC(Non Clausal)归结(1982 年，Murray 在 AI上发表的论文[85] )，都是在广义归结中加上某种简单限制，这些限制既带来一些好处，同时也带来一些坏处。