计算机科学家逻辑/命题逻辑/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$