計算機科學家邏輯/謂詞邏輯/語義樹

語義樹

在本節中，我們將介紹語義樹的概念，它可以用來證明解析的完備性。為此，我們假設讀者熟悉樹、二叉樹和樹路徑的概念。

定義 15

一組子句 $S$ 的語義樹是一棵二叉樹 $T$ ，其根為 $N_{0}$ ，使得邊用文字標記，文字由 $S$ 的 Herbrand 基中的元素構成，使得

如果 $N$ 是一個內部節點，它的兩條出邊用互補文字 $A$ 和 $\lnot A$ 標記。
在 $T$ 中，到達節點 $N$ 的每條路徑中，都不會包含 $I(N)$ 中的互補文字，其中 $I(N)$ 是路徑邊上的文字集。

定義 16

如果每條路徑都包含 Herbrand 基中的每個原子（正或負），則語義樹稱為完整的。

示例： $S=\{p(x),q(f(x))\}$ ，其 Herbrand 基為

\{p(a),q(a),p(f(a)),q(f(a)),p(f(f(a))),\ldots \}

請注意，對於語義樹 $T$ 和節點 $N$ ，集合 $I(N)$ 可以被看作是對基本原子進行真值賦值，就像在 Herbrand 解釋中一樣。因此，我們稱 $I(N)$ 為部分解釋。一個完整的語義樹對應於對解釋的窮盡“列舉”。

定義 17

語義樹 $T$ 的一個節點 $N$ 是一個失敗節點，如果 $I(N)$ 使 $S$ 中的一個子句的某個基本例項為假，但對於 $N$ 的每個祖先節點 $N'$ ， $I(N')$ 不會使 $S$ 中的任何子句的基本例項為假。
如果語義樹 $T$ 中的每條路徑都包含一個失敗節點，那麼該樹稱為閉合樹。
如果閉合語義樹中的節點 $N$ 的兩個直接子節點都是失敗節點，則稱該節點為推斷節點。

示例： $S=\{p(x),\lnot p(x)\lor q(f(x)),\lnot q(f(a))\}$ ，其中 Herbrand 基是

\{p(a),q(a),p(f(a)),q(f(a)),p(f(f(a))),\ldots \}

令 $T$ 為一個完整的語義樹，那麼我們稱 $T'$ 為相應的閉合樹，如果它可以透過在失敗節點處剪下所有分支從 $T$ 中獲得。

定理 5（Herbrand 定理 - 版本 1）

一組子句 $S$ 是不可滿足的，當且僅當對於 $S$ 的每個完整語義樹，都存在一個相應的有限封閉語義樹。

證明： 假設 $S$ 是不可滿足的，並且 $T$ 是 $S$ 的一個完整語義樹。對於每條路徑 $P$ ，我們都有標籤集 $I_{B}$ ，這是一個解釋，因為樹是完整的。因此， $I_{B}$ 使子句 $C\in S$ 的一個地面例項 $C'$ 為假，因為 $S$ 是不可滿足的。由於 $C'$ 中只有有限多個文字，因此必須存在一個失敗節點 $N_{B}$ ，它距離根節點有限距離。由於每條路徑都有這樣的失敗節點，因此存在一個相應的封閉語義樹 $T'$ ，它是有限的。

對於相反方向，假設對於每個完整語義樹 $T$ ，都存在一個相應的有限封閉樹 $T'$ 。那麼，每條路徑都包含一個失敗節點，因此，每個解釋都使 $S$ 為假；因此 $S$ 是不可滿足的。

定理 6（赫布蘭德定理 - 版本 2）

一組子句 $S$ 是不可滿足的，當且僅當存在一個有限不可滿足的集合 $S'$ ，該集合包含 $S$ 中子句的地面例項。

證明： 假設 $S$ 是不可滿足的，並且 $T$ 是 $S$ 的一個完備語義樹。根據 Herbrand 定理版本 1，存在 $S$ 的一個有限閉合語義樹 $T'$ 。設 $S'$ 是在 $T'$ 的所有失敗節點上被證偽的子句的基例項集。 $S'$ 是有限的，並且被所有解釋所證偽，因此是不可滿足的。我們透過逆否命題證明相反的方向。