在离散数学中证明过 Skolem 范式的性质：设谓词逻辑公式 G 的 Skolem 范式为 S，则 G 的不可满足性与 S 的不可满足性等价。因此，若想证明谓词逻辑公式 G 是不可满足的，可以通过证明 S 的不可满足性来实现。相比于公式 G 可以具有任意形式，S 是只包含全称量词的前束范式，并且母式为合取范式（若干个子句的合取）。因此，S 可以看成是一个子句集合，该集合中出现的量词均是被全称量词作用。
这就是下面经常谈论子句集的原因。项、文字、子句等若不含变量，则相应地称为基项、基文字和基子句。
首先介绍子句集 S 的 Herbrand 域。
设 H0 是出现于子句集 S 的常量符号集合，若 S 中无常量符号出现，则H0 由一个常量符号a 组成。对于i=1,2,..., 在Hi-1 中加入fn(t1,...,tn)得到的集合 Hi 称为 S 的 i 级常量集，其中 fn 是出现在 S 中的所有 n元函数符号，项 t1,...,tn 取自 Hi-1。H∞称为 S 的 Herbrand 域。
例 1： S = {P(f(x), a, g(y,z), b)}，于是， H0 = {a, b}
H1 = {a, b, f(a), f(b), g(a, a), g(a, b), g(b, a), g(b,b)}
H2 = {a, b, f(a), f(b), g(a,a), g(a,b), g(b,a), g(b,b), f(f(a)), f(f(b)),
f(g(a,a)), f(g(a,b)), f(g(b,a)), f(g(b,b)), g(a,f(a)), g(a,f(b)), g(a,g(a,a)), g(a,g(a,b)), ...}
只要子句集 S 中包含函数符号，则 S 的 Herbrand 域是无限集。
对于子句集 S 中子句 C，使用 S 的 Herbrand 域中元素代替 C 中变量得到的基子句构成的集合称为 C 的基例集。
定理 1（Herbrand 定理）子句集 S 是不可满足的，当且仅当存在
S 的一个有限不可满足的 S 的基例集 S’。
Herbrand 定理指出了一种证明子句集S 的不可满足性的方法：如果存在一个机械程序，它可以分别用 H1,H2,...中的元素生成 S 中子句的基例集 S1’,....,Sn’，并依次检查 S1’,....,Sn’,...的不可满足性，那么根据 Herbrand 定理，如果 S 是不可满足的，则这个程序一定可以找到一个有限数N，使SN’是不可满足的。
因为每个 Si’可以视为该集合中全部基子句的合取，因此可以使用命题逻辑中的任意方法检查 Si’的不可满足性。Gilmore 是实现这个想法的第一人，他将 Si’化为析取范式，如果其中任意一个短语包含一个互补对（文字与该文字的否定），则可以从析取范式中删除该短
语。最后，如果某个 Si’是空的，则 Si’是不可满足的。Gilmore 方法需要求析取范式，因此面临组合爆炸的情况，为了克服这个缺点，Davis和 Putnam 提出改进方法，即后来的 DPLL 过程[77] 。
即使采用DPLL 来判定命题公式的不可满足性，Herbrand 定理的主要障碍仍然是它要求生成关于子句集 S 的基例集 S1’,S2’ ,，在多
数情况下，这些集合的元素个数是以指数方式增加的。非常有可能发生：子句集 S 的最小的不可满足基例集 Sk’的元素数远超计算机的存储能力，更别提来判定 Sk’的不可满足性了。
为了避免上述情况，J.A.Robinson 于 1965 年文章中提出归结原理[78] ，可以直接判定任意子句集 S（不一定是基子句集）的不可满足性，其的核心思想是合一算法，通过合一算法来主动生成能证明 S不可满足性的实例。