AIL C3 命题逻辑

由于$\LaTeX$ 的符号限制，本章笔记中使用 $\equiv$ 代替 $|\!=\!|$ ，以避免输入符号过程过于冗杂。

请注意不要将本章笔记中的 $\equiv$ 与一阶逻辑中的 $\equiv$ 混淆。

命题和联结词

• 命题：有真假值的句子/ 陈述句。

  反问句被接受为命题，因为它可以被转化为陈述句。

• （真值）联结词：作用于命题之间，描述命题间关系从而得到新命题。可分为一元联结词和二元联结词。

• 简单命题：不包含联结词的命题。

• 复合命题：包含连结词的命题。

  自然联结词包括： 如果……那么……，……而……，没有……等。由于一元联结词的存在，复合命题可以仅包含一个简单命题。

• 命题的真值： 命题的真假。1表示命题为真，0表示命题为假。

联结词

否定

$A$	并非$A$
1	1
0	0

合取

$A$	$B$	$A$ 并且 $B$
1	1	1
0	1	0
1	0	0
0	0	0

合取支：由合取词联结的两个命题。

析取

$A$	$B$	$A$ 或者 $B$
1	1	1
0	1	1
1	0	1
0	0	0

析取支：由析取支联结的两个命题。

• 相容选言：两个析取支可以同时为真。
• 不相容选言：两个析取支不可同时为真，含义上等价为 $A$ 或者 $B$ 并且 并非 $A$ 并且并非$B$，再自然语言中往往表达为"要么……要么……"。

蕴涵

$A$	$B$	如果 $A$ 那么 $B$ / 只有 $B$ 那么 $A$
1	1	1
1	0	0
0	1	1
0	0	1

蕴涵词表示一个充分条件假言命题中的“如果……那么……”。

• 前件：蕴涵词联结的条件。
• 后件：蕴涵词联结的结论。

由真值表可知，只有当前件为真并且后件为假时该假言命题为真。这种性质的蕴涵也称为实质蕴涵。实质蕴涵 撇开了前后件间在具体内容上的一切联系，而仅仅注意前后件的真假与整个命题的真假间的关系，即纯粹的逻辑上的真假关系。

• 在这种情况下，将$p \rightarrow q$ 读作 “$p$实质蕴涵$q$” 可能比读作 “如果p那么q” 更加合适。

• 蕴含怪论 / 蕴涵悖论：一个假命题可以蕴涵任何命题，一个真命题可以被任意命题蕴涵，与人们的直观不相符合。当人们把蕴涵符号解读为“如果……，那么……”时，难以从直观上认同它们的逻辑真理性。

  严格蕴涵: 和实质蕴涵是两种不同的蕴涵关系。$A\prec B$ 被定义为$\lnot\diamond(A\wedge\lnot B)$，即“A真且B假”是不可能的”；也可以被等价地定义为$\Box(A\rightarrow B)$，即“A实质蕴涵B”是必然的。

等值

A	B	$A$ 当且仅当 $B$
1	1	1
1	0	0
0	1	0
0	0	1

只有当前件和后件的真值相同时该命题为真。

联结词、命题和公式

联结词	命题	公式
否定	负命题	否定式
合取	联言命题	合取式
析取	选言命题	析取式
蕴涵	充分条件假言命题	蕴涵式
等值	充分必要条件假言命题/等值命题	等值式

命题语言

命题语言 $\mathcal{L}^{p}$ 包括：

• 表示原子命题的命题符号：$p,q,r$。特别地，$\bot$ 表示永假命题，$\top$表示永真命题。
• 表示联结词的联结符号：$\lnot ,\wedge ,\vee, \rightarrow, \leftrightarrow$
• 标点符号：左右括号$(,)$。

表达式与公式

表达式： 有限的符号串。则命题公式/ 公式可被形式化定义如下：

1. 命题符号是公式，称为原子公式。
2. 若$\phi,\psi$ 是公式，则(\neg\phi)， (\phi \and \psi),(\phi \or \psi),(\phi \rightarrow \psi),(\phi \leftrightarrow \psi)是公式。
3. 有限次使用(1)(2)得到的是公式。

使用BNF表达式，

\phi ::= p|(\neg\phi)|(\phi \and \phi)|(\phi \or \phi)|(\phi \rightarrow \phi)|(\phi \leftrightarrow \phi)

其中$p$表示任意原子公式，$\phi$表示任意已经构建的公式。

Bacus Normal Form,BNF

类似一种数学游戏：从一个符号起始标志开始，给出替换前面符号的规则。BNF语法定义的书写规范 / 生产式规则形式如下：

$$symbol := alternative_1 | alternative_2 \cdots$$

每条规则申明$:= / ::=$左侧的符号必须被右侧的某一个可选项代替。替换项用 $|$ 分割。替换项通常有两个符号和终结符构成。终结符没有书写规范，是书写过程的终止。

符号通常被叫做非终止符，也有人叫非终端。

依照定义对命题按照联结词进行分类，则任意命题公式有且只有以下形式：

• 原子公式：形如$p$
• 否定式：形如$( \lnot p)$
• 合取式：形如$( p \wedge q)$
• 析取式：形如$( p \vee q)$
• 蕴涵式：形如$( p \rightarrow q)$
• 等值式：形如$( p \leftrightarrow q)$

括号的省略

1. 公式最外层的括号可以省略。
2. 不违反联结词结合力强弱（联结词优先级）的括号可以省略。

语义

公式本身没有真假。

真假赋值

真假赋值： 以所有命题符号为定义域，真假值$\{0,1\}$为值域的函数。用$v(p)$或者$p^{v}$表示真假赋值$v$给公式$p$指派的值。

给定原子公式的真假赋值，其他公式的真值由联结符号的含义确定：

1. $p^v \in \{0,1\}$
2. $( \lnot p)^v = \begin{cases}1,\ p^v = 0\\0,\ p^v = 1\end{cases}$
3. $( p\wedge q)^v = \begin{cases}1,\ p^v = q^v = 1\\0,\ otherwise\end{cases}$
4. $( p\vee q)^v = \begin{cases}0,\ p^v = q^v = 0\\1,\ otherwise\end{cases}$
5. $( p\rightarrow q)^v = \begin{cases}1,\ p^v = 0\ or\ q^v = 1\\0,\ otherwise\end{cases}$
6. $( p\leftrightarrow q)^v = \begin{cases}1,\ p^v = q^v\\0,\ otherwise\end{cases}$
7. $\top^v = 1$
8. $\bot^v = 0$

给定一组集合$\Phi$，则$\Phi^v = 1$表示$\forall \phi \in \Phi,\phi^v = 1$。

公式的分类

对于一个含有$n$个原子公式的复合公式有 $2^n$种真假赋值，根据这些真假赋值的公式真值结果可将命题分为三类：

• 重言式：公式在任何真假赋值下均为真。
• 矛盾式：公式在任何真假赋值下均为假。
• 可满足式：存在一个在真假赋值，公式在该真假赋值下为真且存在一个在真假赋值，公式在该真假赋值下为假。

使用真值表明晰地说明各真假赋值情况下的真值并做出判断。

可满足性

由此定义公式的可满足性。给定命题公式$\phi$，$\phi$ 是可满足的如果

$$\exist v,\phi^v = 1$$

逻辑推论

给定一组命题公式集合$\Phi$ 和一个命题公式$\phi$，$\phi$ 是$\Phi$ 的逻辑推论 当且仅当

$$\forall v, \Phi^v = 1 \rightarrow \phi^v = 1$$

记作$\Phi \models \phi$。

• 当 $\Phi^v = 0$ 时，$\phi^v$的真假值不做要求，即可以为真，也可以为假。即我们不关注$\Phi^v = 0$时的真假。
• 逻辑推论$\Phi \models \phi$是否成立只与$\Phi$ 中公式和$\phi$ 的形式有关，而和其中表示命题的具体内容 / 真假赋值无关。

特别地，$\models \phi$ 当且仅当

$$\forall v, \phi^v = 1$$

由此定义命题$\phi$的有效性。

有效性

给定命题公式$\phi$，$\phi$ 是有效的如果

$$\models \phi$$

Lemma 1

假定$\Phi$ 是有穷集合，$\{\phi_1,\phi_2,\cdots,\phi_n\}\models\phi$ 当且仅当

$$\models \phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n\rightarrow\phi$$

PROOF

$$\begin{align} &\{\phi_1,\phi_2,\cdots,\phi_n\}\models \phi\\ &\Leftrightarrow\forall v,(\phi_1^v = 1) \wedge (\phi_2^v = 1)\cdots\wedge (\phi_n^v = 1) \rightarrow \phi^v = 1\\ &\Leftrightarrow\forall v,(\phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n)^v = 1 \rightarrow \phi^v=1\\ &\Leftrightarrow\forall v,(\phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n \rightarrow \phi)^v=1\\ &\Leftrightarrow \models \phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n\rightarrow\phi \end{align}$$

Lemma 2

给定命题公式$\phi$，

• $\phi$是可满足的 当且仅当 $\lnot \phi$不是有效的；
• $\phi$ 是有效 的 当且仅当 $\lnot \phi$ 不是可满足的。

即可以通过检验一个公式的可满足性来判断这个公式的有效性。

PROOF

$$\begin{align} &\exist v, \phi^v = 1\\ &\Leftrightarrow\lnot(\forall v, (\lnot\phi)^v = 1)\\ &\Leftrightarrow\lnot(\models \lnot\phi) \end{align}$$

$$\begin{align} &\models \phi\\ &\Leftrightarrow\forall v, \phi^v = 1\\ &\Leftrightarrow\lnot\lnot(\forall v, \phi^v = 1)\\ &\Leftrightarrow\lnot(\exist v, (\lnot\phi)^v = 1) \end{align}$$

Lemma 3

给定一组命题公式集合$\Phi$ 和一个命题公式$\phi$，$\Phi \models \phi$ ，当且仅当

$$\Phi \cup \{\lnot \phi\} \models \bot$$

即$\Phi \cup \{\lnot \phi\}$是不可满足的。

PROOF 1

$$\begin{align} &\Phi = \{\phi_1,\phi_2,\cdots,\phi_n\} \models \phi\\ &\Leftrightarrow \models \phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n\rightarrow\phi\\ &\Leftrightarrow \models \lnot(\phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n)\vee\phi\\ &\Leftrightarrow \forall v,(\lnot(\phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n)\vee\phi)^v = 1\\ &\Leftrightarrow \lnot(\exist v, ((\phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n)\wedge\lnot\phi)^v = 1)\\ &\Leftrightarrow \forall v, (\phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n)\wedge\lnot\phi)^v = 0\\ &\Leftrightarrow \models \phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n)\wedge\lnot\phi = 0\\ &\Leftrightarrow \models \phi_1\wedge\phi_2\wedge\cdots\wedge\phi_n)\wedge\lnot\phi \rightarrow \bot\\ &\Leftrightarrow \Phi \cup\{\lnot\phi\}\models \bot \end{align}$$

PROOF 2

• 先证$\Phi \models \phi \Rightarrow \Phi \cup \{\lnot \phi\} \models \bot$:

  由$\Phi\models \phi$，即有$\forall v: \Phi^v = 1,\phi^v = 1$。假设此时$\lnot \phi^v = 1$，则$\phi^v = 0$，和前述矛盾。故不存在一种赋值使得$\left\{\Phi\cup \left\{\lnot \phi \right\}\right\}^v = 1$。

• 再证$\Phi \cup \{\lnot \phi\} \models \bot\Rightarrow \Phi \models \phi$：

  由$\Phi \cup \{\lnot \phi\} \models \bot$，即有$\forall v, \left\{\Phi\cup \left\{\lnot \phi \right\}\right\}^v = 0$，即有$\forall v,\exist \psi:(\psi \in \Phi)\vee(\psi = \lnot\phi),\psi^v = 0$。

  • 若$\psi \in \Phi$，则$\forall v,\Phi^v = 0$，则有$\Phi\models \phi$；
  • 若$\psi = \lnot \phi$，则$\forall v,\phi^v = 1$，则有$\Phi \models \phi$。

语义等价

给定命题公式$\phi,\psi$，$\phi,\psi$语义等价 当且仅当

$$\phi \models \psi \wedge \psi \models \phi$$

记作$\phi |\!\!\!=\!\!\!| \psi$ 。

由于$\LaTeX$ 的符号限制，本章笔记中使用 $\equiv$ 代替 $|\!=\!|$ ，以避免输入符号过程过于冗杂。

一些常见的语义等价关系包括：

• $\lnot\lnot\phi \equiv \phi$
• $\phi \leftrightarrow \psi \equiv (\psi \rightarrow \phi) \wedge (\phi \rightarrow \psi)$
• $\phi \rightarrow \psi \equiv \lnot \phi \vee \psi$
• $\lnot(\psi \wedge \phi) \equiv \lnot\phi \wedge \lnot \psi$
• $\lnot(\psi \vee \phi) \equiv \lnot\phi \vee \lnot \psi$
• $(\psi \wedge \phi)\vee\rho \equiv (\psi \vee \rho)\wedge(\phi\vee\rho)$
• $(\psi \vee \phi)\wedge\rho \equiv (\psi \wedge \rho)\vee(\phi\wedge\rho)$

Lemma 4 等值替换

给定 $\phi \equiv \psi$，且 $\phi$ 是 $\rho$ 的一部分。则

$$\rho \equiv \rho'$$

若将$\rho$中的$\phi$ 替换为 $\psi$ 得到 $\rho'$。

等价关系

集合$X$上的二元关系$R\subseteq X\times X$ 是等价关系，当且仅当 $R$满足

• 自反性：$(a,a) \in R$；
• 对称性：$(a,b) \in R \Leftrightarrow (b,a) \in R$；
• 传递性：$(a,b) \in R,\ if\ \exist c \in X,(a,c) \in R \wedge (c,b) \in R$，

$\forall a,b \in X$。

关于$R$下 $a$ 的等价类，记作 $[a] = \{x \in X | (x, a) \in R\}$。

易知语义等价关系满足自反性、对称性和传递性，是一种等价关系。

范式 Normal Form

每个命题公式都有唯一的*形式*，但通过语义等价关系可以被变换为其他形式，变换形式后的公式与原公式属于同一等价类。-

合取范式

称$\phi$ 为 $\psi$ 的合取范式，如果 $\phi \equiv \psi$，且

$$\phi = D_1 \wedge D_2 \wedge \cdots \wedge D_n$$

其中

• $D_i$ 是 $\phi$ 的子句，形如 $L_1 \vee L_2 \vee \cdots \vee L_n$。
• $L_i$ 是 子句的文字 literal，为原子公式或原子公式的否定。

析取范式

称$\phi$ 为 $\psi$ 的析取范式，如果 $\phi \equiv \psi$，且

$$\phi = D_1 \vee D_2 \vee \cdots \vee D_n$$

其中

• $D_i$ 是 $\phi$ 的子句，形如 $L_1 \wedge L_2 \wedge \cdots \wedge L_n$。
• $L_i$ 是 子句的文字 literal，为原子公式或原子公式的否定。

子句不可以有否定。故$\lnot\lnot q$ 既不是合取范式，也不是析取范式；$q\vee p$既是合取范式，又是析取范式。

• 任何命题公式与它的合取/析取范式等价。

形式推演

为了建立一个过程来判读一个有效推理是否成立，我们需要建立一个基于规则的推理系统，称该规则为推理规则。

推理规则：在推理系统内，从一组前提出发，被不断应用可以得到结论的规则。

实现形式推演系统需要考虑规则的选择和应用问题，这与所涉及公式的形式有关。规则越多，公式形式越多样，形式推演各步骤进行规则选择的难度就越大。因此为了提高系统的可实现性，可以

• 减少公式的形式。
• 减少规则的数量。

MP规则：蕴含消去

$$\phi,\phi \rightarrow \psi \models \psi$$

形式可推演

给定一组前提集合$\Phi = \{\phi_1,\phi_2,\cdots,\phi_n\}$ 和一个结论$\psi$，其中 $\phi_i$和$\psi$都是公式。从前提$\Phi$到这个结论$\psi$是形式可推演的，如果存在一个证明

$$\begin{align} &1\ \quad &\psi_1\\ &2\ \quad &\psi_2\\ &\ &\cdots\\ &m\ \quad &\psi_m \end{align}$$

使得 $\psi_m = ψ$。其中，$\psi_i (i = 1, 2, 3,\cdots,m)$ 要么属于 $\Phi$，要么依据$\{\psi_1, \cdots , \psi_{i−1}\}$ 中的公式通过应用一条推理规则得到。

记为$\Phi \vdash \psi$。

推理系统的性质

设 $\vdash_R$ 是由一组形式推演规则集合$R$构成的推理系统，称为自然演绎系统。对于任意公式集合 $\Phi$和公式 $\psi$，

• 推理系统 $\vdash_R$是可靠的，当且仅当 如果$\Phi \vdash_R \psi$，则$\Phi \models \psi$。
• 推理系统 $\vdash_R$是完备的，当且仅当 如果$\Phi \models \psi$，则$\Phi \vdash_R \psi$。

因此，如果一个推理系统是可靠的，那么从一组真命题出发，通过形式推演得到的结论也是真的，确保了推理系统的正确性；如果一个推理系统是完备的，那么从一组真命题出发，可以推出这组真命题所蕴涵的所有结论，确保了推理系统的推理能力。

Exp: 消解原理

消解推演系统

在进行形式推演前，把相关公式转化为合取范式。

子句公式

• 在一个子句中，命题符号的重复出现和文字的顺序不影响子句真值。
• 在一个合取范式中，子句的重复出现和子句的顺序不影响范式真值。

因此，可以把一个子句看成是一个文字集合，理解为文字的析取；一个合取范式看成子句集合，理解为子句的合取，即为子句公式。 记

• 文字集合/子句：$[L_1, L_2,\cdots , L_n]$，等价于$L_1\vee L_2\vee\cdots \vee L_n$，其中$L_i$是文字；
• 子句集合/公式：$\{D_1,D_2,\cdots , D_m\}$，等价于$D_1 \wedge D_2 \wedge \cdots \wedge D_m\}$，其中$D_i$是子句。

特别指出，$[\ ]$表示空子句，理解为$\bot$ ；$\{\ \}$表示空公式，理解为 $\top$。且 $1 = \{\ \} \neq \{[\ ]\} = 0$。

消解规则

以子句公式为前提，给定两个子句$D_1,D_2$ ，则可从$D_1\cup \{L\}$ 和$D_1\cup \{\overline{L}\}$ 推出子句$D_1 \cup D_2$。其中，$D_1,D_2$ 可为空集$[\ ]$。即

$$D_1\cup \{L\},D_1\cup \{\overline{L}\} \vdash_R D_1 \cup D_2$$

称$D_1\cup D_2$ 为$D_1,D_2$关于$L$的消解式。

$\overline{L}$​ 是 $L$​的补 : 对于任意原子公式$p$，

$$\forall p, \overline{p} = \lnot p,\overline{\lnot p} = p$$

系统性质

$\sqrt{}$可靠性

Lemma 5

$$D_1\cup \{L\},D_1\cup \{\overline{L}\} \models D_1 \cup D_2$$

PROOF

$$\forall v: (D_1\cup \{L\})^v = 1,(D_2\cup \{\overline{L}\})^v = 1$$

假设 $(D_1 \cup D_2)^v = 0$。则

$$D_1^v = 0,D_2^v = 0$$

则

$$L^v = 1,\overline{L}^v = 1$$

即有$(L \vee \overline{L})^v = 1$ ，与$(L \vee \overline{L})^v = \bot^v = 0$ 矛盾。故原式成立。

下证明消解系统的可靠性：

$$若 \Phi \vdash_{Res} = D,\ 则 \Phi \models D$$

PROOF

1. 基始步骤：$\forall D_i \in \Phi$，显然有$\Phi \models D_i$。
2. 归纳步骤：如果 $\Phi \models D_i$ 且 $\Phi \models D_j$，$D_k$ 是 $D_i$ 和 $D_j$ 的消解式，其中$i, j, k \in \{1, 2, \cdots , n\}$ 由lemma 5，$\Phi \models D_k$。

$\times$完备性

PROOF Counter Example

设$\Phi = \{[\lnot p]\},D = [\lnot p,p]$。显然$\Phi \models D$，但无法构造一个从$\Phi$出发的消解推演$D_1,D_2,\cdots, D_n$ 使得$D_n = D$。

Summary

• 消解推理系统是可靠的，但不是完备的。
• 当$D = [\ ]$，消解推演既是可靠的，又是完备的。即消解系统是否证完备的。

Lemma 6 否证完备

从一组有穷的前提集$\Phi$出发，如果不存在 $\bot$ 的 证明，那么$\Phi$是可满足的。

PROOF

上述定理等价为如果一个消解证明没有新子句可以获得，但$\bot$还没被推出，此时整个公式集合（包括前提）都是可满足的。为表方便定义消解闭包：给定子句集合$S$，则$R(S)$是$S$的消解闭包，若$R(S)$满足：

1. 如果$c\in S$，则$c \in R(S)$；
2. 如果$c_1， c_2 \in R(S)$， 且 $c$ 是 $c_1$ 和$c_2$的消解，则$c\in R(S)$。

则上述定义等价为：若 $\bot \notin R(\Phi)$，则$\Phi$是可满足的。

现对$R(\Phi)$中出现的命题符号数量 $n$做归纳证明。

1. 基始步骤： $n = 0$， 即没有任何公式符号。据定义$\{\quad \}$ 是可满足的。

2. 归纳步骤：假设对于$n = 1,2,\cdots,k$，上述断言均成立。则$n = k + 1$时，假设子句集合$\Phi$ 满足 $\bot \notin R(\Phi)$，选择任一命题符号记为$p$，将$R(\Phi)$划分为不相交的三个子集$S_p,S_{\lnot p},S_0$：

   • $S_p$ : $\Phi$中包含 $p$ 的所有子句的集合。
   • $S_{\lnot p}$ : $\Phi$中包含 $\lnot p$ 的所有子句的集合。
   • $S_0$ : $\Phi$中既不包含 $p$ ，又不包含 $\lnot p$ 的所有子句的集合。易知$S_0$ 包含至多$k$ 个命题符号且 $\bot \notin S_0$，根据假设有 $S_0$ 是可满足的: $\exist v,S_0^v = 1$。

   对$p$在$v$下的赋值做分类讨论：

   • $\forall D = p \vee D' \in S_p,\ v(D') = 1$： 此时$S_p^v = 1$，即$S_p$是可满足的。令$p^v = 0$，则$\forall D = \lnot p \vee D' \in S_{\lnot p},\ v(D) = 1$，即$S_{\lnot p}$是可满足的。即$R(\Phi)$是可满足的。
   • $\exist D_0 = p \vee D' \in S_p,\ v(D') = 0$：令$p^v = 1$，则$\forall D = p \vee D' \in S_{p},\ v(D) = 1$，即$S_p$是可满足的。对于$S_{\lnot p}$，若为空集，则$R(\Phi)$已为可满足的；若非空集，则$\forall D = \lnot p \vee D'’ \in S_{\lnot p}$，使其与$p\vee D'$ 消解，得到 $D' \vee D''$，且$D' \vee D''$不含$p,\lnot p$,故必定在$S_0$中。由$S_0$是可满足的，故$(D'\vee D'')^v = 1$。即$R(\Phi)$是可满足的。

   也即：$n = k + 1$，上述断言成立。

综上，若 $\bot \notin R(\Phi)$，则$\Phi$是可满足的。

Lemma 7 消解算法的复杂性 ,

$$\exist c > 1:\forall n,\exist p: \forall v,p^v = 0,最小消解否证包含 c^n步骤。$$

其中 $n$为$p$包含的命题符号数量。

霍恩Horn子句逻辑

前述消解系统是难解的。一个系统的计算复杂性与表达能力有关，故可通过降低系统的表达能力降低计算复杂性。对于消解系统来说，霍恩公式是一种降低计算复杂性的方法。

霍恩子句

定义

霍恩子句是形如$L_1 \vee \cdots \vee L_n$的子句，其中子句至多包含一个正文字。

• 肯定/确定霍恩子句：子句刚好包含一个肯定文字时。
• 否定霍恩子句：子句不包含肯定文字时。

可将一般的子句转化为蕴含公式：

$$p_1\vee p_2\vee\cdots\vee p_m\vee\lnot q_1 \vee \lnot q_2\vee\cdots\vee\lnot q_n \equiv (q_1\wedge q_2\wedge\cdots q_n) \rightarrow (p_1\vee p_2\vee\cdots\lnot p_m)$$

约定蕴涵前件的文字之间恒为合取，蕴涵后件的文字之间恒为析取，并按照逻辑编程的惯例，上式也常写作

$$p_1,p_2,\cdots,p_m \leftarrow q_1,q_2,\cdots,q_n$$

其中$m,n \in \mathbb{N}$。称上式为一个规则，$p_1,p_2,\cdots,p_m$ 为头，$q_1,q_2,\cdots,q_n$ 称为身体。

RECALL可废止规则的每条规则包括：

• 规则头 - 论证结论
• 规则身体 - 论证前提
• 规则符号 - 推理关系

形式

则霍恩子句限制$m = {0,1}$，以得到确定的结果。故霍恩子句共有四种形式：

• $p \leftarrow q_1,\cdots,q_m$
• $p \leftarrow$
• $\leftarrow q_1,\cdots,q_m$
• $\Box$ （空子句）

在本课程中 $\Box,[\ ],\bot$是等价的，只是在不同的的语境中使用。

类似地，从程序设计的角度出发，

• 称形如 $p\leftarrow q_1,\cdots, q_m$ 的霍恩子句为一个过程 ：
  • 称 $p$ 称为过程名；
  • 称 $\{q_1,\cdots, q_m\}$ 称为过程体
  • 解释 $q_i$ 为过程调用。
• 称形如 $p \leftarrow$的霍恩子句为一个事实 ；
• 称形如$\leftarrow q_1,\cdots,q_m$ 的霍恩子句为一个目标。目标全部由过程调用组成，常用来表示一个询问。
• 称 $\Box$ 为停机语句，表示程序执行（成功）终止。

霍恩子句逻辑

霍恩子句逻辑是由霍恩子句组成的系统。它是命题演算系统的子系统。

霍恩子句逻辑程序是指这样一些被称为过程、目标和事实的霍恩子句的集合。

• 给定一个霍恩子句逻辑程序，它由目标中的一个过程调用与一事实或与一过程的过程名匹配启动。
• 当过程调用与一事实匹配，该过程调用成功。
• 再由目标中另一过程调用重新启动程序，直至目标中全部过程调用成功或者某一 过程调用失败。(不能与事实或过程名匹配）
• 当过程调用与一过程名匹配，程序需调用该过程的过程体，该过程体中的过程调用与原目标中余下的过程调用合并形成新目标，并重新启动程序，寻求匹配。

SAT solver

SAT Solver 是实现可满足性的推理引擎：给定一个公式，建构一个真假赋值使得这个公式为真。

RECALL消解原理 处理逻辑演绎。给定一个知识库，检查一个命题是否可以被这个知识库所蕴涵。

DPLL算法

给定一个子句集合 $\Phi$，$\Phi$ 所包含的所有命题符号集合记作 $\Sigma$。DPLL算法 递归调用一个函数 $DPLL(\Phi)$ ：

$$\rm DPLL(\Phi)\ Returns\begin{cases}1, \exist v,\Phi^v = 1\\ 0, otherwise\end{cases}$$

递归规则

1. 如果$\Phi = \phi$ (空集)，返回可满足。
2. 如果 $[\ ] \in \Phi$， 返回不可满足。
3. 单位传播规则：如果 $\Phi$ 包含单位子句$C$，则给$C$中的命题符号赋值使得 $C^v = 1$并在该赋值下把$\Phi$简化为$\Phi'$，调用 $DPLL(\Phi')$。
4. 分裂规则：从$\Sigma$中选择一个没有被赋值的命题符号 $p$并赋值$p^v = 1$，并在该赋值下把$\Phi$简化为 $\Phi'$，调用 $DPLL(\Phi')$。

• 如果该调用返可满足，则返回可满足。
• 否则，赋值$p^v = 0$，并在该赋值下把$\Phi$简化为 $\Phi''$，并调用 $DPLL(\Phi'')$。

从计算复杂性的角度看，SAT,DPLL是NP完全的：在最坏的情况下，其计算复杂性为指数时间。

霍恩子句下的DPLL

1. DPLL 算法在霍恩子句上总能产生霍恩子句。

2. 在 DPLL 中，若第一次系列应用单位传播规则没有导致结束，那么产生的霍恩子句集合不含单位子句。

3. 一组既不含单位子句也不含空语句的霍恩子句是可满足的。

   所有子句都至少有一个负文字，给所有未赋值命题符号赋真值 0 即可满足公式。

4. 依据***3.***可知，每次应用分裂规则时，当前的公式是可满足的 / 错误可以立即被发现。

因此，对于包含 $n$ 个命题符号的 (二叉) 搜索树，最多只有 $n$ 个节点应用了分裂规则。即搜索树的大小是 $n$ 的多项式，故霍恩子句下的DPLL运行时间是多项式的。