计算机科学家逻辑/命题逻辑/消解

消解

在本节中，我们将为命题逻辑开发一种演算。到目前为止，我们有一个语言，即一组公式，我们已经研究了语义和公式或子句集的一些性质。现在，我们将引入一条推理规则，即消解规则，它允许从给定的子句推导出新的子句。

定义 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)$ 则 **停止：可满足**。