不含有任何连线词的谓词公式叫原子公式，简称原子，而原子或原子的否定统称文字。子句就是由一些文字组成的析取式。由子句构成的集合称为子句集。将没有变元出现的子句集分别称作基子句集。

定义1 不含有任何连线词的谓词公式叫原子公式，简称原子，而原子或原子的否定统称文字。

定义2 子句就是由一些文字组成的析取式。

定义3 不包含任何文字的子句称为空子句，记为 。

定义4 由子句构成的集合称为子句集。

定义5 设谓词公式G的子句集为S，则按下述方法构造的个体变元域H称为公式G或子句集S的Herbrand域，简称H域。

(1)令H₀是S中所出现的常量的集合。若S中没有常量出现，就任取一个常量 ，规定 。

(2)令 {S中所有的形如 的元素)，其中 是出现于

G中的任一函式符号，而 是 中的元素。i=0，1，2，…。

定义6下列集合称为子句集S的原子集：

A={所有形如 的元素}

其中， 是出现在S中的任一谓词符号，而 则是S的H域上的任意元素。

定义7 将没有变元出现的原子、文字、子句和子句集分别称作基原子、基文字、基子句和基子句集。

定义8 当子句集S中的某个子句C中的所有变元符号均以其H域中的元素替换时，所得到的基子句称作C的一个基例。

定义9(可满足性、不可满足性)对于一个变元自由的一阶语言公式G，如果至少存在一个D论域上的一个解释，在此解释下G为真，则称G是可满足的，即；反之，如果对于任何解释G均为假，则称G是不可满足的，即。

对于一个变元自由的一阶语言公式集，即，如果至少存在一个D的解释，在此解释下，的每个以D为论域的公式均为真，则称为可满足的；如果D的所有解释都有假公式，则称是不可满足的。

定理1 设有谓词公式G，而其相应的子句集为S，则G是不可满足的充分必要条件是S是不可满足的。

要再次强调：公式G与其子句集S并不等值，只是在不可满足意义下等价。

的子句集

当 时，若设P的子句集为 ， 的子句集为 ，则一般

情况下， 并不等于 ，而是要比 複杂得多。但是，在不可满足的意义下，子句集 与 是一致的，即 不可满足 不可满足。

定义10 如果子句集S的原子集为A，则对A中各元素的真假值的一个具体设定都是S的一个H解释。

可以证明，在给定域D上的任一个解释 ，总能在H域上构造一个解释与之对应，使得如果D域上的解释能满足子句集S，则在H域的解释也能满足S(即若，就有)。

定理2 设是子句集S在域D上的一个解释，则存在对应于的H域解释，使得若有，就必有。

定理3 子句集S不可满足的充要条件是S对H域上的一切解释都为假。

证明： 充分性：若S在一般域D上是不可满足的，必然在H域上是不可满足的，从而对H域上的一切解释都为假。

必要性：若S在任一H解释下均为假，必然会使S在D域上的每一个解释为假。否则，如果存在一个解释使S为真，那幺依据定理2可知，一定可以在H域找到相对应的一个解释使S为真。这与S在所有H解释下均为假矛盾。

定理4 子句集S不可满足的充要条件是存在一个有限的不可满足的基例集S’。

该常理称为Herbrand定理。