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

消解

在本節中，我們將為命題邏輯開發一種演算。到目前為止，我們有一個語言，即一組公式，我們已經研究了語義和公式或子句集的一些性質。現在，我們將引入一條推理規則，即消解規則，它允許從給定的子句推匯出新的子句。

定義 10

一個子句 $R$ 是子句 $C_{1}$ 和 $C_{2}$ 的消解式，如果存在文字 $L\in C_{1}$ 和 ${\overline {L}}\in C_{2}$ ，並且

R=(C_{1}-\{L\})\cup (C_{2}-\{{\overline {L}}\})

其中 ${\overline {L}}={\begin{cases}\;\;\,\lnot A\;{\text{ if }}L=A\\\;\;\,A\;{\text{ if }}L=\lnot A\end{cases}}$

注意，存在一種特殊情況，如果我們從兩個文字構造消解式，即 $L$ 和 ${\overline {L}}$ 可以被消解併產生空集。這個空的消解式用特殊符號 $\square$ 表示。
$\square$ 表示一個不可滿足的公式。我們定義一個包含空子句的子句集為不可滿足的，

接下來，我們將研究消解規則和整個演算的性質。以下引理說明了消解規則單次應用的正確性。

定理 7

如果 $S$ 是一組子句，而 $R$ 是 $C_{1},C_{2}\in S$ 的一個消解式，那麼 $S\equiv S\cup \{R\}$

證明：令 ${\mathcal {A}}$ 是 $S$ 的一個賦值；因此它也是 $S\equiv S\cup \{R\}$ 的一個賦值。假設 ${\mathcal {A}}\models S$ ：因此，對於 $S$ 中的所有子句 $C$ ，我們都有 ${\mathcal {A}}\models C$ 。 $C_{1}$ 和 $C_{2}$ 的消解式 $R$ 看起來像

R=(C_{1}-\{L\})\cup (C_{2}-\{{\overline {L}}\})

其中 $L\in C_{1}$ 且 ${\overline {L}}\in C_{2}$ 。現在有兩個情況

${\mathcal {A}}\models L$ : 從 ${\mathcal {A}}\models C_{2}$ 和 ${\mathcal {A}}\not \models {\overline {L}}$ 中，我們可以得出 ${\mathcal {A}}\models (C_{2}-\{{\overline {L}}\})$ 因此 ${\mathcal {A}}\models R$ .
${\mathcal {A}}\not \models L$ : 從 ${\mathcal {A}}\models C_{1}$ 中我們可以得出 ${\mathcal {A}}\models (C_{1}-\{L\})$ 因此 ${\mathcal {A}}\models R$ 。引理的相反方向是顯而易見的。

定義 11

令 $S$ 是子句集，並且

Res(S)=S\cup \{R\mid R{\text{ is a resolvent of two clauses in }}S\}

那麼

$Res^{0}(S)=S$
$Res^{n+1}(S)=Res(Res^{n}(S)),n\geq 0$
$Res^{*}(S)=\bigcup _{n\geq 0}Res^{n}(S)$

如果我們將迭代 Res 運算子的過程理解為從給定集合中推匯出新子句的過程，特別是推匯出可能為空的子句，我們必須問，在哪些情況下我們能得到空子句，反之，如果我們得到空子句，這意味著什麼。以下兩個定理將研究這些性質。

定理 8（正確性）

令 $S$ 為一組子句。如果 $\square \in Res^{*}(S)$ ，則 $S$ 不可滿足。

證明：從 $\square \in Res^{*}(S)$ 中我們可以得出結論， $\square$ 是透過兩個子句 $C_{1}=\{L\}$ 和 $C_{2}=\{{\overline {L}}\}$ 採用歸結推理得出的。因此，存在一個 $\exists n\geq 0$ 使得 $\square \in Res^{n}(S)$ 並且 $C_{1},C_{2}\in Res^{n}(S)$ ，因此 $Res^{n}(S)$ 不可滿足。從定理（歸結推理引理）中我們可以得出結論， $Res^{n}(S)\equiv S$ ，因此 $S$ 不可滿足。

定理 9（完備性）

令 $S$ 為一組有限子句。如果 $S$ 不可滿足，則 $\square \in Res^{*}(S)$ .

證明： 對公式集中原子公式數量 $n$ 進行歸納。當 $n=0$ 時，我們有 $S=\{\square \}$ ，因此 $\square \in S\subseteq Res^{*}(S)$ 。

假設 $n$ 固定，並且對於每個包含 $n$ 個原子公式的不可滿足子句集 $S$ ，都有 $\square \in Res^{*}(S)$ 。

假設有一個包含原子公式 $A_{1},\cdots ,A_{n},A_{n+1}$ 的子句集 $S$ 。接下來我們將構造兩個子句集 $S_{f}$ 和 $S_{t}$

$S_{f}$ 是透過從 $S$ 中刪除每個子句中所有 $A_{n+1}$ 以及包含 $\lnot A_{n+1}$ 的所有子句而得到的。這種變換顯然對應於用 $false$ 解釋原子公式 $A_{n+1}$ ，
$S_{t}$ 是從類似的變換中得出的，其中 $\lnot A_{n+1}$ 的出現和包含 $A_{n+1}$ 的子句都被刪除了，因此 $A_{n+1}$ 被解釋為 $true$ .

讓我們證明， $S_{f}$ 和 $S_{t}$ 都是不可滿足的：假設原子公式 $\{A_{1},\cdots ,A_{n}\}$ 的一個賦值 ${\mathcal {A}}$ 是 $S_{f}$ 的模型。因此，賦值 ${\mathcal {A}}'(B)={\begin{cases}\;\;\,{\mathcal {A}}(B)\;{\text{ if }}B\in \{A_{1},\cdots ,A_{n}\}\\\;\;\,false{\text{ if }}B=A_{n+1}\end{cases}}$ 是 $S$ 的模型，這導致了矛盾。類似的構造表明 $S_{t}$ 也是不可滿足的。因此，我們可以使用歸納假設得出結論： $\square \in Res^{*}(S_{t})$ 和 $\square \in Res^{*}(S_{f})$ 。因此，存在一個子句序列

C_{1},\cdots ,C_{m}=\square

使得 $\forall 1\leq i\leq m$ 成立 $C_{i}\in S_{f}$ 或 $C_{i}$ 是兩個子句 $C_{a}$ 和 $C_{b}$ 的消解式，其中 $a,b<i$ 。對於 $S_{t}$ 也有類似的序列。

C_{1}',\cdots ,C_{t}'=\square

現在我們將重新引入之前刪除的文字 $A_{n+1}$ 和 $\lnot A_{n+1}$ 到這兩個序列中。

子句 $C_{i}$ 是從 $S$ 中原始子句刪除 $A_{n+1}$ 而得到的，再次被修改為 $C_{i}\cup \{A_{n}+1\}$ 。這將導致一個序列 ${\overline {C_{1}}},\cdots ,{\overline {C_{m}}}$

其中 ${\overline {C_{m}}}$ 要麼是 $\square$ ，要麼是 $A_{n+1}$ 。

在第二個序列中，我們引入 $\lnot A_{n+1}$ ，使得 ${\overline {C_{t}'}}$ 要麼是 $\square$ ，要麼是 $\lnot A_{n+1}$ 。

在以上任何情況下，我們都得到 $\square \in Res^{*}(S)$ ，最多經過一次使用 ${\overline {C_{m}}}$ 和 ${\overline {C_{t}'}}$ 的消解步驟。

基於正確性和完備性定理，我們給出了一個決定命題公式可滿足性的過程。

決定命題公式的可滿足性

給定一個命題公式 $F$ 。

將 $F$ 轉換為等價的 CNF $S$ 。
計算 $Res^{n}(S)$ $Res^{n}(S)$ ，對於 $n=0,1,2,\cdots$ $n=0,1,2,\cdots$
- 如果 $\square \in Res^{n}(S)$ 則 **停止：不可滿足**。
- 如果 $Res^{n}(S)=Res^{n+1}(S)$ 則 **停止：可滿足**。