2.6.1.1 Herbrand 定理思想
　　要证明一个公式是永假的，采用反证法的思想（归结原理），就是要寻找一个已给的公式是真的解释。然而，如果所给定的公式的确是永假的，就没有这样的解释存在，并且算法在有限步内停止。