最后更新: 2025-01-21 20:53 ● 参与者查看: 12 次纠错分享参与项目词条搜索

消解规则

定理2．8 $C_1 \wedge C_2 \approx \operatorname{Res}\left(C_1, C_2\right)$
证记 $C=\operatorname{Res}\left(C_1, C_2\right)=C_1{ }^{\prime} \vee C_2{ }^{\prime}$ ，其中 $l$ 和 $l^c$ 为消解文字，$C_1=l \vee C_1{ }^{\prime}$ ， $C_2=l^c \vee C_2{ }^{\prime}$ ，且 $C _1{ }^{\prime}$ 和 $C _{ 2 }{ }^{\prime}$ 不含 $I$ 和 $l ^c$ 。

假设 $C_1 \wedge C_2$ 是可满足的，$\alpha$ 是它的满足赋值，不妨设 $\alpha(l)=1$ ． $C_2$ 必含有文字 $l^{\prime} \neq l, l^c$ 且 $\alpha\left(l^{\prime}\right)=1 . C$ 中含有 $l^{\prime}$ ，故 $\alpha$ 满足 $C$ ．

反之，假设 $C$ 是可满足的，$\alpha$ 是它的满足赋值．$C$ 必有 $l^{\prime}$ 使得 $\alpha\left(l^{\prime}\right)=1$ ，不妨设 $C_1{ }^{\prime}$ 含 $l^{\prime}$ ，于是 $\alpha$ 满足 $C_1$ 。把扩张到 $l\left(\right.$ 和 $\left.l^c\right)$ 上：
若 $l=p$ ，则令 $\alpha(p)=0$ ；若 $l^c=p$ ，则令 $\alpha(p)=1$ ．恒有 $\alpha\left(l^c\right)=1$ ，从而 $\alpha$满足 $C_2$ ．得证 $C _1 \wedge C _2$ 是可满足的．

注意：$C_1 \wedge C_2$ 与 $\operatorname{Res}\left(C_1, C_2\right)$ 有相同的可满足性，但不一定等值．

定义2．10 设 $S$ 是一个合取范式，$C_1, C_2, \ldots, C_n$ 是一个简单析取式序列。如果对每一个 $i(1 \leq i \leq n), C_i$ 是 $S$ 的一个简单析取式或者是 $\operatorname{Res}\left(C_j, C_k\right)(1 \leq j<k<i)$ ，则称此序列是由 $S$ 导出 $C_{ n }$ 的消解序列。当 $C _{ n }=\lambda$ 时，称此序列是 $S$ 的一个否证。

定理2．9 一个合取范式是不可满足的当且仅当它有否证。

例11 用消解规则证明 $S=(\neg p \vee q) \wedge(p \vee q \vee \neg s) \wedge(q \vee s) \wedge \neg q$ 是不可满足的。
证 $C_1=\neg p \vee q, C_2=p \vee q \vee \neg s, C_3=\operatorname{Res}\left(C_1, C_2\right)=q \vee \neg s, C_4=q \vee s$ ， $C_5=\operatorname{Res}\left(C_3, C_4\right)=q, C_6=\neg q, C_7=\operatorname{Res}\left(C_5, C_6\right)=\lambda$ ，这是 $S$ 的否证．

上一篇：复合联结词

下一篇：消解算法

本文对您是否有用？有用 (0) 无用 (0)