計算機科學家邏輯/命題邏輯/Horn 子句

Horn 子句

在本節中，我們將介紹一類特殊的公式，它們對邏輯程式設計特別感興趣。此外，事實證明，這些公式允許對可滿足性進行有效的測試。

定義 9

如果公式是 CNF 且每個析取最多包含一個正文字，則該公式為 Horn 公式。Horn 子句是最多包含一個正文字的子句。

$F=(A\lor \lnot B)$       $\land$   $(\lnot C\lor \lnot A\lor D)$

$\land (\lnot A\lor \lnot B)$       $\land$   $D\land \lnot E$

$F\equiv (B\to A)$            $\land$   $(C\land A\to D)$

$\land (A\land B\to false)$    $\land$   $(true\to D)\land (E\to false)$

其中 $true$ 是重言式，而 $false$ 是不可滿足的公式。

用子句形式可以寫成

$\{\{A,\lnot B\},\{\lnot C,\lnot A,D\},\{\lnot A,\lnot B\},\{D\},\{\lnot E\}\}$

在邏輯程式設計的語境下，這寫成

$\{A\gets B$

  $D\gets A,C$

$\gets A,B$

$\gets E$

   $D\gets$      $\}$

對於 Horn 公式，存在一種有效的演算法來測試公式 $F$ 的可滿足性。

判定 Horn 公式的可滿足性

1. 如果存在一種形式的子公式 $true\to A$，則標記 $F$ 中 $A$ 的每個出現。
   
2. 應用以下規則，直到沒有規則適用為止
   
   • 如果 $A_{1}\land \cdots \land A_{n}\to B$ 是一個子公式，並且 $A_{1}\cdots A_{n}$ 都已標記，而 $B$ 未標記，則標記 $F$ 中 $B$ 的每個出現。
     
   • 如果 $A_{1}\land \cdots \land A_{n}\to false$ 是一個子公式，並且 $A_{1}\cdots A_{n}$ 都已標記，則 **停止：不可滿足**
     

3. **停止：可滿足** 賦值 ${\mathcal {A}}(A)=true$ 當且僅當 $A$ 已標記，是一個模型。
   

定理 6

上述演算法是正確的，並在 $n$ 步之後停止，其中 $n$ 是公式中原子數量。

作為直接結果，我們看到，如果一個 Horn 公式沒有形式為 $A_{1}\land \cdots \land A_{n}\to false$ 的子公式，則它是可滿足的。

Horn 公式允許唯一的最小模型，即 ${\mathcal {A}}$ 是 $F$ 的唯一最小模型，如果對於每個模型 ${\mathcal {A}}'$ 和 F 中的每個原子 B 成立：如果 ${\mathcal {A}}(B)=true$，那麼 ${\mathcal {A}}'(B)=true$。注意，這種唯一的最小模型性質不適用於非 Horn 公式：例如，$A\lor B$ 顯然是非 Horn 的。 ${\mathcal {A}}_{1}(A)=true,{\mathcal {A}}_{1}(B)=false$ 是一個最小模型，並且 ${\mathcal {A}}_{2}(A)=false,{\mathcal {A}}_{2}(B)=true$ 也是，因此我們有兩個最小模型。

問題

問題 20（命題邏輯）

令 $F$ 為一個命題邏輯公式，$S$ 為 $F$ 中出現的原子公式的子集。令 $T_{S}(F)$ 為將 $F$ 中所有出現的原子公式 $A\in S$ 替換為 $\lnot A$ 所得的公式。例如：$T_{\{A\}}(A\land B)=\lnot A\land B$。證明或反駁：存在一個 $S$ 使得

1. $F=A{\stackrel {\cdot }{\vee }}B$ 或
2. $F=A{\stackrel {\cdot }{\vee }}B{\stackrel {\cdot }{\vee }}C$，使得 $T_{S}(F)$ 等價於一個 Horn 公式 $H$（即 $T_{S}(F)\equiv H$）。
   

$\Box$

問題 21（命題邏輯）

將標記演算法應用於以下公式 F。

哪個是最小模型？

$(A\lor \lnot D\lor \lnot E)\land (B\lor \lnot C)\land (\lnot B\lor \lnot D)\land D\land (\lnot D\lor E)$

1. $F=(\lnot A\lor \lnot B\lor \lnot C)\land \lnot D\land (\lnot E\lor A)\land E\land B\land (\lnot F\lor C)\land F$
2. $F=(A\lor \lnot D\lor \lnot E)\land (B\lor \lnot C)\land (\lnot B\lor \lnot D)\land D\land (\lnot D\lor E)$

$\Box$

問題 22（命題邏輯）

判斷哪些 CNF 是 Horn 公式，並將它們轉換為蘊含式的合取形式

1. $(A\lor B\lor C)\land (A\lor \lnot C)\land (\lnot A\lor B)\land \lnot B$
2. $(S\lor \lnot P\lor Q)\land (S\lor \lnot P\lor \lnot R)$
3. $(A\lor \lnot A)$
4. $A\land (\lnot A\lor B)\land (\lnot B\lor \lnot C\lor D)\land (\lnot E)\land (\lnot A\lor \lnot C)\land D$

$\Box$