計算機科學家邏輯/謂詞邏輯/Herbrand 理論

Herbrand 理論

到目前為止，我們考慮了謂詞邏輯中公式的任意解釋。特別是，我們有時使用數字作為解釋域和函式，比如加法或後繼。在下文中，我們將集中討論一種特殊情況，Herbrand 解釋，並將討論它們與一般情況的關係。

定義 11

令 $S$ 為一組子句。S 的 Herbrand 域 $U_{H}$ 由以下給出：

• 出現在 $S$ 中的所有常量都在 $U_{H}$ 中（如果 $S$ 中沒有出現常量，我們假設一個單個常量，比如 $a$ 存在於 $U_{H}$ 中）。
• 對於每個 n 元函式符號 $f$ 出現在 $S$ 中，以及每個 $t_{1},\cdots ,t_{n}\in U_{H}$，$f(t_{1},\cdots ,t_{n})\in U_{H}$。

示例：給定子句集 $S_{1}=\{P(a),\lnot P(x)\lor P(f(x))\}$，我們構建 Herbrand 域

$U_{H}=\{a,f(a),f(f(a)),f(f(f(a))),\cdots \}$

對於子句集 $S_{2}=\{P(x)\lor Q(x),R(z)\}$，我們得到Herbrand全集 $U_{H}=\{a\}$。

定義 12

設 $S$ 是一個子句集。解釋 ${\mathcal {I}}=(U_{\mathcal {I}},A_{\mathcal {I}})$ 是一個Herbrand解釋，當且僅當

• $U_{\mathcal {I}}=U_{H}$
• 對於每一個 $n$元函式符號（$n\geq 0$） $f$ 和 $t_{1},\cdots ,t_{n}\in U_{H}$$f^{\mathcal {I}}(t_{1},\cdots ,t_{n})=f(t_{1},\cdots ,t_{n})$
  

注意，對謂詞符號的賦值關係沒有限制（當然，它們必須是Herbrand全集 $U_{H}$ 上的關係）。

為了討論謂詞符號的解釋，我們需要Herbrand基的概念。

定義 13

一個地原子或一個地項是一個不包含變數的原子或項。對於一組子句 $S$，它的 Herbrand 基是地原子集 $p(t_{1},\ldots ,t_{n})$，其中 $p$ 是來自 $S$ 的一個 $n$-元謂詞符號，並且 $t_{1},\ldots ,t_{n}\in U_{H}$。

我們將透過簡單地給出集合 $I=\{m_{1},m_{2},\cdots ,m_{n},\cdots \}$ 來表示將關係分配給謂詞符號，其中每個元素都是一個文字，其原子來自 Herbrand 基。

例子

• $S=\{p(x)\lor q(x),r(f(y))\}$
• $U_{H}=\{a,f(a),f(f(a)),\ldots \}$
• $I=\{p(a),q(a),r(a),p(f(a)),q(f(a)),r(f(a)),\cdots \}$

定義 14

設 ${\mathcal {I}}=(U_{\mathcal {I}},A_{\mathcal {I}})$ 是一個子句集 $S$ 的解釋; 與 ${\mathcal {I}}$ 相對應的 Herbrand 解釋 ${\mathcal {I}}^{*}$ 是一個滿足以下條件的 Herbrand 解釋: 設 $t_{1},\ldots ,t_{n}$ 是 $S$ 的 Herbrand 域 $U_{H}$ 中的元素。透過解釋 ${\mathcal {I}}$ 每個 $t_{i}$ 都對映到一個 $d_{i}\in U_{\mathcal {I}}$。如果 $p^{\mathcal {I}}(d_{1},\ldots ,d_{n})=true(false)$，那麼 $p(t_{1},\ldots ,t_{n})$ 必須在 ${\mathcal {I}}^{*}$ 中被賦值為 $true(false)$。

現在讓我們陳述一個簡單而顯而易見的引理，它將幫助我們關注後續的 Herbrand 解釋。

引理 4

如果 ${\mathcal {I}}$ 是子句集的模型，那麼與之相對應的每個 Herbrand 解釋 ${\mathcal {I}}^{*}$ 都是 $S$ 的模型。

定理 4

一組子句 $S$ 是不可滿足的，當且僅當 $S$ 沒有 Herbrand 模型。

證明：如果 $S$ 是不可滿足的，顯然 $S$ 沒有 Herbrand 模型。
假設 $S$ 沒有 Herbrand 模型，並且 $S$ 是可滿足的。那麼，存在 ${\mathcal {I}}$ 是 $S$ 的模型，根據引理 4，相應的 Herbrand 解釋 ${\mathcal {I}}^{*}$ 是 $S$ 的模型，這與假設矛盾。