范式

语义等价、满足性和有效性

真值表一致并不能表明我们的逻辑语义就是等价的，比如我们有 蕴含关系， 这和 $\neg p \lor q$ 是不等价的

定义

对于命题逻辑公式 $\phi$ 和 $\psi$, 我们称二者语义等价，当且仅当 $\phi\models \psi \land \psi \models \phi$ 成立，记为 $\phi \equiv \psi$. 进一步, 如果 $\models \phi$ 成立，我们称 $\phi$ 是有效的

引理

命题逻辑公式 $\phi_1\cdots\phi_n\models \psi$成立，当且仅当 $\models\phi_1\to(\phi_2\cdots\to(\phi_n \to \psi))$
这个引理用于将命题变成完全不包含 $\to$ 的形式 （使用 $\neg p\lor q\equiv p\to q$ tautology)
通过将 $\to$ 变成一般逻辑公式，使得正确与否很好确定，我们称之为范式 (normal form)

范式 Normal Form

合取范式 conjunctive normal form (CNF)

公式

$C:: = D | D\land C$

公式 $C$ 是若干子句的合取
合取范式在检验有效性的方面有非常强的作用，我们可以快速查看每个部分的成立

析取引理

文字析取 $L_1\lor L_2\lor L_3\cdots L_n$ 是有效的 当且仅当存在 $1\le i,j\le m$ 使得 $L_i$ 是 $\neg L_j$
相类似的，对于合取逻辑，我们检验有效性就看是不是有互为相反逻辑的同时存在于合取式中

可满足性 satisfiable

对一个命题逻辑公式 $\phi$ 我们有赋值使得其为 $T$ 则我们称 $\phi$ 是可满足的

可满足性和有效性

命题 $\phi$, 我们有 $\phi$ 是可满足的 当且仅当 $\neg \phi$ 不是有效的 (注意这里的赋值是相同的)

如何构建合取范式

1. 列出真值表
2. 找到赋值为 False 的项，对每一项前提 premise 取非之后用 $\lor$ 连接
   1. 这里其实用到了摩根定律
3. 将上述的逻辑命题合取连接

合取范式和有效性

一个公式是有效的当且仅当他的等价公式是有调得，我们把判断任何一个 $\phi$ 是否有效的问题简化为它的等价公式 $\psi$ 是否有效上面去，其中 $\psi$ 是 CNF, 这样就很好判断了
但是对一个命题，其等价合理范式并不是只有一个，所以我们需要找到最小成本，也就是获得合取的个数或者语法分析树的高度之类的定量判定
这里我们要考虑的是 确定性 deterministic 算法(算法名也叫 CNF)，即对于一个已知输入 $\phi$, 总能给出同样输出 CNF
对此，我们首先要保证:

1. CNF 是能终止的
2. 对于每一个输入，CNF 输出一个等价公式
3. 所有由 CNF 计算的输出都是 CNF 形式

预处理

首先我们需要将逻辑公式中的 $\psi \to\eta$ 的蕴含用 $\neg \psi \lor \eta$ 替代.
这个程序 我们称为 IMPL_FREE 蕴含释放，这个程序必须是递归的，因为 $\psi, \eta$ 本身可能就是蕴含关系

否定范式

我们并不知道能不能有效的从 $\phi$ 的 CNF 推导到 $\neg \phi$ 的 CNF
首先我们称 只否定原子的公式为 否定范式 NNF (negation normal form), 原就是得摩根公式
也就是说预处理的结果表达式大概就是 NNF(IMPL_FREE(\phi)

递归思路

• 如果 $\phi = \phi_1 \land \phi_2$, 我们对每一个 $\phi_i$ 递归的调用 CNF 得到输出 $\bigwedge \eta_i$
• 如果 $\phi = \phi_1\lor \phi_2$, 我们对每一个 $\phi_i$ 递归使用 CNF, 但是不能直接返回 $\bigvee \eta_i$, 因为这不是 CNF

分配律算法

这是一个独立算法 DISTR, 用于将命题进行逻辑分配到原子命题
为什么要分配？
因为分配律能将合取的析取变成析取的合取，也就是能让我们拥有合取范式

霍恩子句 Horn Clause

定义

霍恩公式满足:

P::\quad = \quad \bot\quad |\quad \top\quad | \quad p$$ $$A::\quad = \quad P \quad | \quad P \quad\land\quad A$$ $$C:: \quad = \quad A \quad \to \quad P

$H::\quad = \quad C \quad | \quad C\quad \land\quad H$

其中 $C$ 表示一个霍恩子句，$H$ 就表示一个霍恩公式，即多个霍恩子句的合取

霍恩公式算法要求

• 对于可满足性的功能正确
• 循环次数是一定有限的

SAT 求解机

霍恩公式的标记算法是对所有使公式为真的赋值进行标记来作为约束，那么我们应该将其对命题“真"的赋值转变为对子式的真假赋值
SAT Solver 是一个对于布尔可满足性问题的算法

线性求解机