第二章 归结推理方法

　　2.3.4 Herbrand 定理
　　回顾针对一阶谓词描述下的
　　　　∧∧→B
的证明问题，我们已经作了足够的准备。首先将这个证明问题化成
　　　　G＝∧∧∧～B
的不可满足问题，进而将G化成 SKOLEM 标准形建立了相应的子句集S，并将一般论域D上的讨论简化成H域上的讨论，最后还引入了语义树。现在就可阐明 Herbrand 给出的两个定理了。
定理 定理
  　2.3.4(1)子句集S是不可满足的，当且仅当对应于S的完全语义树都是一棵有限的封闭语义树。
证明 证明
  　设S是不可满足的。
　先作出S的完全树T。
　令B是T的任一分枝，IB是对应B分枝上S的一个解释。依S的不可满足性，IB必使S的某子句的某基例为假。这样，B上必有结点N，而N是T的失败结点。
　需说明的是失败结点N必离T的根结点只有有限步。这是由于IB中文字个数是可数的，而S中子句个数有限，每个子句所含有的文字也有限。
　又由于语义树T是个二叉树，每个结点仅有有限的两个子结点。这样从T的根结点计起，直到所有分枝上的失败结点所构成的封闭树必是有限的。
　反过来，已知S有限的封闭语义树。
　设I是S的任一解释，I必落在T的某分枝B上，知B上必有失败结点如N。而I(N)已使S的某个子句的某基例C'为假了。
　但是I(N)I，自然有I使C'为假。由I是S的任一解释，故S是不可满足的。
　定理证毕。
定理 定理 2.3.4(2)
  　S是不可满足的，当且仅当存在不可满足的S的有限基例集。
证明 证明
  　设S是不可满足的。
　从而依定理2.3.4(1)，S的完全语义树T必是一棵有限的封闭语义树。设T共有n个失败结点N1,…,Nn，而且I(Ni)使S的某子句Ci的基例Ci′为假。
　令　S'={C1',…,Cn'}
　需证明S'是不可满足的。对S'的任一解释I'必有S的某个解释I，使得II'。由于S是不可满足的，I必使S的某子句的某基例Cj'为假，但是I中使Cj'为假的文字均包含于I'中，于是I'也使Cj'为假，从而S'是不可满足的。
　反过来，知S'是不可满足的有限基例集。
　设I是S的任一解释，必有S'的解释I'使II'。然而I'已使S'的某个Cj'为假，于是I也使Cj'为假，从而使S为假。故S是不可满足的。
　定理得证。

　　应该指出 Herbrand 定理给出了一阶逻辑的半可判定算法。其中的"半"字指的是有条件下的判定算法，即仅当被证定理是成立的，使用该算法方可得证。而当被证定理并不成立时，使用该算法得不出任何结果。说是算法，那指的是有限步内是可实现的。因为无论从有限的封闭树观点，还是从不可满足的有限基例集观点都是可判定的，因为这已是有限的命题逻辑问题了。
　　使用 Herbrand 定理，来证明定理或S是不可满足的，或是寻找有限的封闭树或是寻找有限的不可满足的基例集。
　　一个具体实现证明的方法是，对S的H域中的Hi做出基例集Si'，即将Hi中的元素依次代入S中的各子句便构成了Si'，若Si'是不可满足的必有S是不可满足的，或说相应的定理成立。若被证定理成立，必可在有限步内证明某个S'N是不可满足的。
　　1960年 Gilmore 编制了生成Si'的程序，进而将Si'化成析取范式，当每个析取项都含有互补对时便知Si'是不可满足的。然而化成析取范式并不是好方法，如下规则可简化计算过程（由于Herbrand 定理已将证明问题化成了命题逻辑问题，所以只需在命题逻辑范围来简化）。
　　重言式子句可删除规则
　　S中的重言式子句，不会为S的不可满足提供任何信息，应该删除。
　　如　　S＝{P∨～P,,}
　　那么S的逻辑含义是(P∨～P)∧∧=∧，从而删去重言式P∨～P，不影响S的真值。
　　单文字删除规则
　　如S＝{L ,L∨,～L∨,,}
　　其中C3,C4不含L和～L。先作S'再作S",
　　S'：{～L∨,,}是从S中删除含L的子句而得。
　　S"：{,,}是从S'中删除文字～L而得。
　　那么　若S'为空集，便知S是可满足的。
　　 　　 若S'非空，便知S与S" 同时是不可满足的。
　　这个结论是不难证明的。如S'为空集，那么S形如{L，L∨，～L∨}， 即每个子句都含文字L。若取L=T，必有S为T，所以S是可满足的。如果S'不是空集，若S是不可满足的而S"是可满足的，就有解释I"使
　　　　S"|I"=T　即　∧∧|I" =T
那么令 I= I"∪{L，…}，这时必有S|I=T，这与S不可满足是矛盾的。反过来设S"是不可满足的而S是可满足的，有I使
　　　　S|I=T
其中I必含L，而且(～L∨)∧∧|I=T，从而 ∧∧|I=T，这与S"不可满足性相矛盾。
　　纯文字删除规则
　　当文字L出现于S中，而～L不出现于S中，便说L为S的纯文字。若从S中删除含L的子句得S'，而为空集，那么S是可满足的。而当S'非空，那么S'与S同时是不可满足的。
　　分离规则
　　若　S＝(L∨A1)∧…∧(L∨Am)∧(～L∨B1)∧…∧(～L∨Bn)∧R
　　其中R是不含L和～L的子句集。
　　令　　S'＝{A1,…,Am,R}
　　　　　S"＝{B1,…,Bn,R}
　　则S不可满足当且仅当S'和S" 同时是不可满足的。
　　这几条删除规则的使用，将会简化S不可满足的证明过程。纯文字和分离规则可同单文字规则一样得到证明。