Herbrand定理：
　　定理1：
　　子句集S是不可满足的，当且仅当对应于S的完全语义数是棵有限封闭树。
　　定理2：
　　子句集S是不可满足的，当且仅当存在不可满足的S的有限基例集。