| 定理的意义在于将一阶逻辑证明问题转化成了有限的命题逻辑问题。由此定理保证，可以放心的用机器来实现自动推理了。（归结原理） 注意：Herbrand定理给出了一阶逻辑的半可判定算法，即仅当被证明定理是成立时，使用该算法可以在有限步得证。而当被证定理并不成立时，使用该算法得不出任何结论。 使用Herbrand定理，来证明定理或S是不可满足的，或是寻找有限的封闭树或是寻找有限的不可满足的基例集。 一个具体实现证明的方法是，对S的H域中的Hi作出基例集Si'，即将Hi中的元素依次带入S中的各个子句便构成Si'，若Si'是不可满足的，必有S是不可满足的，或说相应的定理成立。若被证明的定理成立，必可在有限步内证明某个SN'是不可满足的。 重点： 1． 这里公式G的解释的意义是：公式G的一个解释就是公式G在其论域上的一个实例化。 2． H域实际上是对于论域的一种简化。使得我们在一个能够把握的论域中对逻辑命题进行永假的判断。 3． 以下的概念需要特别注意和区分：f（tn）, 原子集, H解释, 基例 |