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

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

定义

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

引理

命题逻辑公式 ϕ1⋯ϕn⊨ψ\phi_1\cdots\phi_n\models \psi成立，当且仅当 ⊨ϕ1→(ϕ2⋯→(ϕn→ψ))\models\phi_1\to(\phi_2\cdots\to(\phi_n \to \psi))
这个引理用于将命题变成完全不包含 →\to 的形式 （使用 ¬p∨q≡p→q\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, 用于将命题进行逻辑分配到原子命题 为什么要分配？ 因为分配律能将合取的析取变成析取的合取，也就是能让我们拥有合取范式