子句集

不含有任何連接詞的謂詞公式叫 原子公式，簡稱 原子，而原子或原子的否定統稱 文字。子句就是由一些文字組成的 析取式。由子句構成的集合稱為 子句集。將沒有變元出現的子句集分別稱作 基子句集。

例如，都是子句。用 表示空子句，即不包含任何文字的子句。構成一個子句集S： 。相反，以下命題表達式不是單獨的子句: 。因為它們的最外層都是 連接的，因此前者可以化為A 和B 兩個子句，後者可以化為 和C兩個子句。不能區分在子句集中的子句是獨立的命題，還是一個合取範式(由 連接的表達式)。在本例中，命題 和命題 的子句集都是。

定義1不含有任何連接詞的謂詞公式叫 原子公式，簡稱 原子，而原子或原子的否定統稱 文字。

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

定義3不包含任何文字的子句稱為 空子句，記為。

定義4由子句構成的集合稱為 子句集。

定義5設謂詞公式G的子句集為S，則按下述方法構造的個體變元域H稱為公式G或子句集S的 Herbrand域，簡稱 H域。

(1)令是S中所出現的常量的集合。若S中沒有常量出現，就任取一個常量，規定。

(2)令 {S中所有的形如 的元素)，其中 是出現於G中的任一函數符號，而 是 中的元素。。

定義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的子句集為，的子句集為，則一般

情況下，並不等於，而是要比 複雜得多。但是，在不可滿足的意義下，子句集 與 是一致的，即 不可滿足 不可滿足。

H域上的解釋

定義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定理。