計算機科學家邏輯/命題邏輯/解析圖

解析圖

在本節中，我們介紹一種演算，即解析圖，它作為消解法的替代方案。雖然這種演算是在獨立於消解法的情況下發展起來的，但事實證明它有一些有趣的共同特徵。最明顯的區別是解析圖直接作用於公式，不需要將公式轉換成子句正規化。

解析圖 - 簡史

解析圖演算的發展始於 1950 年代。首先要提到的是 Beth (1955)、Hintikka (1955) 和 Schütte (1956)。他們的目標主要是開發沒有元語言結構的演算。後來在 1960 年代，這種演算中推導樹和節點的想法，以及在這樣的樹中用公式標記節點，成名於 Smullyan 在 1968 年引入的解析圖的概念。然後，Kanger (1957)、Prawitz (1960)、Wang (1960)、Davis (1960) 和 Maslov (1968) 引入瞭解析圖演算機械化的想法。

後來，解析圖的概念被修改和完善，以便在自動推論中使用，例如 Loveland 在 1968 年（模型消除）、Kowalski 和 Kuehner 在 1971 年（SL-消解）以及 Bibel 在 1975 年、Andrews 在 1976 年（連線或配對方法）。如今，有許多基於這項工作的高效能定理證明器。

演算

解析圖演算的優點之一是它可以在不將公式轉換為子句正規化的情況下定義。
示例 給定一組公式 $\{\lnot P\land \lnot (Q\lor R),\lnot (Q\land \lnot R)\}$。我們的目標是構建一棵樹，其分支包含用公式標記的節點。

為此，重要的是根據公式的引導連線詞來分析公式。Smullyan 觀察到，如果非字面量公式被分組到相同型別的公式中，可以節省一些工作：$\alpha$ 用於表示連線型別的公式，$\beta$ 用於表示命題情況下的析取型別的公式。請注意，在上面的例子中，$\lnot (Q\land \lnot R)$ 必須被視為析取型別的公式，因為前面有一個否定符，它位於連結符之前。公式與其型別之間的對應關係總結在表 1 中。字母 $\alpha$ 和 $\beta$ 用於表示（僅表示）相應型別的公式。現在讓我們定義解析圖演算的基本資料結構以及相應的擴充套件規則。

定義 13

一個邏輯 $L$ 的 tableau 是一個有限分支樹，其節點是來自 $L$ 的公式。tableau $T$ 中的一條分支是 $T$ 中的一條最大路徑。當沒有混淆時，分支通常與其節點（公式）的集合等同。給定一個來自 $L$ 的公式集 $\Phi$，$\Phi$ 的 tableau 是透過（可能是無限的）一系列應用以下規則構建的。

1. 由單個節點 $true$ 組成的樹是 $\Phi$ 的 tableau（初始化規則）。
2. 令 $T$ 是 $\Phi$ 的一個 tableau，$B$ 是 $T$ 中的一條分支，$\psi$ 是 $B\cup \Phi$ 中的一個公式。如果樹 $T'$ 是透過擴充套件 $B$ 透過表格 2 中具有前提 $\psi$ 的 tableau 規則模式的例項一樣多的新線性子樹構建的，並且新子樹的節點是規則例項的擴充套件中的公式，那麼 $T'$ 是 $\Phi$ 的一個 tableau（擴充套件規則）。

我們示例中的一個 tableau 如圖 2 所示。

定義 14

在一個分析表 $T$ 中，對於一個句子集合 $\Phi$，一個分支 $B$ 是封閉的當且僅當 $B\cup \Phi$ 包含一對互補公式 $\phi ,\lnot \phi$，或 $false$；否則，它是開放的。如果分析表的所有分支都是封閉的，那麼分析表是封閉的。對於一個公式集合 $\Phi$（其不可滿足性），一個分析表證明是一個針對 $\Phi$ 的封閉分析表 $T$。

問題 31（命題邏輯）

給出以下公式的嚴格分析表證明

1. $\lnot ((A\downarrow B)\downarrow (A\lor B))$
2. $((A\to B)\land (B\to C))\to (\lnot (\lnot C\land A))$

$\Box$

子句正規化分析表

現在讓我們改進計算方法，專門針對子句集的情況，這些子句集表示以CNF形式的公式。請注意，在合取正規化的情況下，我們只有文字，它們透過 $\lor$-連線詞連線。因此每個子句都是 $\beta$-型別的。在圖 3 中，給出了一個子句集的分析表。來自給定子句集的子句形成了初始分析表；然後只有 $\beta$-規則可用於進一步擴充套件分析表。

在以下子句正規化分析表的正式定義中，我們從一個初始分析表開始，該分析表是透過從給定的子句集S中獲取任意子句形成的。對於進一步擴充套件分析表，可以使用來自S的子句的 $\beta$-規則應用。哪個子句是允許的由一個 *連結條件* 控制。

定義 15

一組子句 $S$ 的子句（正規化）真值表是 $S$ 的真值表，其節點是 $S$ 中的文字，並且透過以下規則（可能是無限的）序列來構建。

1. 以 $true$ 為根，並以 $L_{1},\cdots ,L_{n}$ 為直接後繼的樹是 $S$ 的真值表，其中 $C=L_{1},\cdots ,L_{n}\in S$ （初始化規則）。
2. 令 $T$ 是 $S$ 的真值表，$B$ 是 $T$ 的一個分支，並且 $C=L_{1},\cdots ,L_{n}\in S$，使得連結條件（見下文）滿足。如果樹 $T'$ 是透過 $n$ 個子樹 $L_{i}$ 擴充套件 $B$ 而構建的，那麼 $T'$ 是 $S$ 的真值表（擴充套件規則）。

以下列出了三種可能的連結條件

1. 無條件。
2. 弱連線條件：存在一個字面量 $L\in B$ 以及 ${\overline {L}}\in C$.
3. 強連線條件：令 $L$ 為 $B$ 的葉節點，則存在 ${\overline {L}}\in C$.

實際上我們已經定義了三種不同的演算

• 在沒有連線條件的情況下，它被稱為子句正規化真值表。
• 在有弱連線條件的情況下，我們稱之為連線演算，而
• 在有強連線條件的情況下，它被稱為模型消去。

子句正規化真值表的示例在圖 3 中給出。連線演算真值表的示例是

最後，模型消去真值表由以下給出

定理 11

子句正規化真值表是完備的。
注意強連線條件不允許合流

證明過程。如果沒有連線條件（即空條件），那麼很容易得到一個合流版本。對於弱連線條件的情況，這不是很明顯。為了得到命題子句的判定過程，我們需要一個額外的條件

定義 16

子句集 $S$ 的真值表的分支 $B$ 被稱為正則的，如果沒有任何字面量出現超過一次。

定理 12

具有正則性和連線條件的子句正規化真值表為命題邏輯提供了一個判定過程。

問題（診斷）

考慮這個有兩個輸入線和一個輸出線的電子電路

假設，如所示，兩條輸入線都為“1”，而輸出線為“1”，這與預期輸出值“0”相矛盾。

1. 首先，對電路進行形式化，即對三個元件和兩個連線的功能進行形式化，忽略元件無法正常工作的可能性（即不要使用abnormal -字面量）。
2. 考慮向輸入線提供值對“0-0”、“1-0”和“1-1”。對於這些值對中的每一個，使用（1）中的結果，透過解析真值表計算預期的輸出值。你如何從真值表中讀出結果？
3. 使用你的形式化和解析真值表來證明輸出值“1”在輸入為“1-1”的情況下與預期行為相矛盾。你如何從真值表中讀出結果？
4. 現在透過abnormal -字面量修改（1）中元件的形式化，如課堂上所示。使用解析真值表計算輸入為“1-1”且輸出為“1”的所有可能的診斷。你如何從真值表中讀出結果？