定義
不含有任何連線詞的謂詞公式叫 原子公式,簡稱 原子,將沒有變元出現的原子稱作 基原子(即“ 基礎原子”)。
相關概念
定義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的子句集為 , 的子句集為 ,則一般情況下, 並不等於 ,而是要比 複雜得多。但是,在不可滿足的意義下,子句集 與 是一致的,即 不可滿足 不可滿足 。
海伯倫理論
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定理 。