命题逻辑的归结

将逻辑公式转换成合取范式(CNF)的方法:

1.消去{$\mathrm{\neg },\wedge ,\vee$${\lnot},{\wedge},{\vee}$}以外的逻辑联结词。

常见联结词的转换方法:

$A\to B\iff \mathrm{\neg }A\vee B$$A\rightarrow B \Leftrightarrow \lnot A \lor B$ $A\uparrow B\iff \mathrm{\neg }(A\wedge B)$$A\uparrow B \Leftrightarrow \lnot (A \land B)$ $A\downarrow B\iff \mathrm{\neg }(A\vee B)$$A\downarrow B \Leftrightarrow \lnot (A \lor B)$ $A\leftarrow B\iff A\vee \mathrm{\neg }B$$A\leftarrow B \Leftrightarrow A \lor \lnot B$ $A\leftrightarrow B\iff (A\to B)\wedge (B\to A)$$A{\leftrightarrow}B \Leftrightarrow (A\rightarrow B) \land (B\rightarrow A)$ $A\oplus B\iff \mathrm{\neg }(A\to B)\vee \mathrm{\neg }(B\to A)$$A\oplus B \Leftrightarrow \lnot (A\rightarrow B)\lor \lnot (B\rightarrow A)$

2.利用德$\cdot$${\cdot}$摩根律将否定联结词$\mathrm{\neg }$${\lnot}$内移到命题变量之前,消去双重否定。

3.利用分配律化成合取范式。

例: 求$(\mathrm{\neg }p\to \mathrm{\neg }q)\to (p\to q)$$(\lnot p\rightarrow \lnot q)\rightarrow (p\rightarrow q)$的合取范式。

$\mathrm{\neg }p\to \mathrm{\neg }q)\to (p\to q)$$\lnot p\rightarrow \lnot q)\rightarrow (p\rightarrow q)$ $\iff \mathrm{\neg }(\mathrm{\neg }\mathrm{\neg }p\vee \mathrm{\neg }q)\vee (\mathrm{\neg }p\vee q)$$\Leftrightarrow \lnot (\lnot \lnot p\lor\lnot q) \lor (\lnot p \lor q)$ $\iff (\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }p\wedge \mathrm{\neg }\mathrm{\neg }q)\vee (\mathrm{\neg }p\vee q)$$\Leftrightarrow (\lnot \lnot \lnot p\land\lnot \lnot q) \lor (\lnot p \lor q)$ $\iff (\mathrm{\neg }p\wedge q)\vee (\mathrm{\neg }p\vee q)$$\Leftrightarrow (\lnot p \land q) \lor (\lnot p \lor q)$ $\iff (\mathrm{\neg }p\vee \mathrm{\neg }p\vee q)\wedge (q\vee \mathrm{\neg }p\vee q)$$\Leftrightarrow (\lnot p\lor\lnot p \lor q) \land (q \lor\lnot p \lor q)$

例: 求$((p\vee q)\to r)\to p$$((p{\vee}q){\rightarrow}r){\rightarrow}p$的合取范式。

$((p\vee q)\to r)\to p$$((p{\vee}q){\rightarrow}r){\rightarrow}p$ $\iff (\mathrm{\neg }(p\vee q)\vee r)\to p$${\Leftrightarrow}({\lnot}(p{\vee}q){\vee}r){\rightarrow}p$ $\iff \mathrm{\neg }(\mathrm{\neg }(p\vee q)\vee r)\vee p$${\Leftrightarrow}{\lnot}({\lnot}(p{\vee}q){\vee}r){\vee}p$ $\iff ((p\vee q)\wedge \mathrm{\neg }r)\vee p$${\Leftrightarrow}((p{\vee}q){\wedge}{\lnot}r){\vee}p$ $\iff (p\vee q\vee p)\wedge (\mathrm{\neg }r\vee p)$${\Leftrightarrow}(p{\vee}q{\vee}p){\wedge}({\lnot}r{\vee}p)$ $\iff (p\vee q)\wedge (\mathrm{\neg }r\vee p)$${\Leftrightarrow}(p{\vee}q){\wedge}({\lnot}r{\vee}p)$

一个合取范式是永真式,当且仅当它的每个基本和都是永真式。 一个基本和是永真式,当且仅当至少含有一个命题变量及其否定。 一个子句(Clause)是一个文字集合中所有元素的析取。 一个单位子句(Unit Clause)的文字集合仅含一个文字。 一个空子句(Empty Clause )的文字集合是空集。空子句记为$◻$$\Box$. 一个公式可以表示成含有若干个子句的集合的形式, 称为子句标准形(Clause Form)。该公式的真值是子句标准形中所有子句的合取。 子句标准形可以是空集,记为$\varphi$$\phi$​​. 每个公式都可以转换成子句标准形, 因为子句标准形与合取范式是对应的。

例: $(p\vee r)\wedge (\mathrm{\neg }q\vee \mathrm{\neg }p\vee q)\wedge (p\vee \mathrm{\neg }p\vee q\vee p\vee \mathrm{\neg }p)\wedge (r\vee p)$$(p \lor r) \land (\lnot q \lor \lnot p \lor q) \land (p\lor \lnot p \lor q \lor p\lor \lnot p) \land (r \lor p)$ 合并子句中的相同元素,可化简为: $(p\vee r)\wedge (\mathrm{\neg }q\vee \mathrm{\neg }p\vee q)\wedge (p\vee \mathrm{\neg }p\vee q)\wedge (r\vee p)$$(p \lor r) \land (\lnot q \lor \lnot p \lor q) \land (p\lor \lnot p \lor q) \land (r \lor p)$

合并相同的子句,可化简为: $(p\vee r)\wedge (\mathrm{\neg }q\vee \mathrm{\neg }p\vee q)\wedge (p\vee \mathrm{\neg }p\vee q)$$(p \lor r) \land (\lnot q \lor \lnot p \lor q) \land (p\lor \lnot p \lor q)$

对应的子句标准形是: $\{\{p,r\},\{\mathrm{\neg }q,\mathrm{\neg }p,q\},\{p,\mathrm{\neg }p,q\}\}.$$\{\{p, r\}, \{\lnot q,\lnot p, q\}, \{p,\lnot p, q\}\}.$

子句标准形也可以表达成缩写形式: $\{pr,\overline{q}\overline{p}q,p\overline{p}q\}$$\{pr, \bar{q}\bar{p}q, p\bar{p}q\}$

如果一个子句仅包含一对互补的文字$\{p,\mathrm{\neg }p\}$$\{p, {\lnot}p\}$,称该子句是平凡的(Trivial). 平凡子句是永真式, 空子句$◻$$\Box$是永假式。 空子句集$\varphi$$\phi$是永真式。

在子句标准形中, 归结(Resolution)是将包含互补文字的两个子句$C_1$$C_1$ ($x\in C_1$$x\in C_1$)和$C_2$$C_2$ ($\overline{x}\in C_2$$\bar{x}\in C_2$)转化为一个子句的操作。转化后的子句是:

$Res(C_1,C_2)=(C_1-\{x\})\vee (C_2-\{\overline{x}\}).$$Res(C_1,C_2) = (C_1 - \{x\}) \lor (C_2 - \{\bar{x}\}).$

例: $Res(ab\overline{c},bc\overline{e})$$Res(ab\bar{c},bc\bar{e})$ $=((ab\overline{c}-\{\overline{c}\})\vee (bc\overline{e}-\{c\})$$=((ab\bar{c} - \{\bar{c}\})\lor (bc\bar{e} - \{c\})$ $=ab\overline{e}.$$=ab\bar{e}.$

例: $Res(\{x,y\}\vee C_1,\{\overline{x},\overline{y}\}\vee C_2)$$Res(\{x,y\}\lor C_1,\{\bar{x},\bar{y}\}\lor C_2)$ $=\{y,\overline{y}\}\vee C_1\vee C_2$$=\{y,\bar{y}\}\lor C_1 \lor C_2$ $=true.$$=true.$

定理: $Res(C_1,C_2)$$Res(C_1,C_2)$是可满足的,当且仅当子句$C_1$$C_1$和$C_2$$C_2$都是可满足的。 称$Res(C_1,C_2)$$Res(C_1,C_2)$与$C_1\wedge C_2$$C_1{\land}C_2$是等可满足性的(Equisatisfiable), 用≈表示。

$\{p,r\}=\{F,F\}$$\{p,r\}=\{F,F\}$时都为假; $\{p,r\}=\{T,T\}$$\{p,r\}=\{T,T\}$都为真; $\{p,r\}=\{F,T\}$$\{p,r\}=\{F,T\}$都可满足; $\{p,r\}=\{T,F\}$$\{p,r\}=\{T,F\}$都可满足。

归结过程不唯一

$\{(1)p,(2)\overline{p}q,(3)\overline{r},(4)\overline{p}\overline{q}r\}$$\{(1)p, (2)\bar{p}q, (3)\bar{r}, (4)\bar{p}\bar{q}r\}$