2.6 Herbrand定理 　　Herbrand定理是归结原理的理论基础，归结原理的正确性是通过Herbrand定理来证明的。同时归结原理是Herbrand定理的具体实现，利用Herbrand定理对公式的证明是通过归结法来进行的。本届简单地描述了Herbrand定理的基本思想和相关预备知识，最后给出Herbrand定理的一般形式。 　　公式G永真：对于G的所有解释，G都为真。 　　公式G永假（矛盾）： 没有一个解释使G为真。 2.6.1 Herbrand 定理概述 　　问题：一阶逻辑公式的永真性（永假性）的判定是否能在有限步内完成？ 　　1936年图灵(Turing)和邱吉(Church)互相独立地证明了： 　　"没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步内判定它是永真（或永假）。对于非永真（或永假）的公式就不一定能在有限步内得到结论。判定的过程将可能是不停止的。"