逻辑等价

逻辑等价要求两个表达式在每个允许赋值或结构中真值相同，而不是仅在某个例子上碰巧同真或同假。它把语法不同但语义不可区分的公式归入同一类，可由双向蕴涵表达，并支持在更大公式中作保持真值的替换。

$P\Rightarrow Q\equiv \mathrm{\neg }P\vee Q$，且 $\mathrm{\neg }(P\wedge Q)\equiv \mathrm{\neg }P\vee \mathrm{\neg }Q$。$P\Rightarrow Q$ 与 $Q\Rightarrow P$ 不等价；在某一行真值表上相同不足以证明逻辑等价。

利用材料蕴涵可验证

左式化为 $\mathrm{\neg }P\vee \mathrm{\neg }Q\vee R$，右式也化为同一公式。逻辑等价要求所有赋值下真值一致；例如 $P\vee Q$ 与异或在多数赋值上相同，却在 $P=Q=\mathrm{\top }$ 时不同，因此不等价。等价替换保持真值，但不表示两个公式具有相同语法树或同样短的证明。

等价变换用于化简公式、逆否证明、逻辑电路和查询规范化。语法相同、可证明等价与语义等价是不同层次。只保持可满足性的 equisatisfiability 更弱：Tseitin 转换后的 CNF 可与原公式同可满足，却因引入新变量而不是同一语言中的逻辑等价替换。

真值表公理库真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。决定命题公式等价，合取范式公理库合取范式Conjunctive normal form · CNF由若干析取子句之合取构成且与原公式逻辑等价的标准形。与析取范式公理库析取范式Disjunctive normal form · DNF由若干合取项之析取构成且与原公式逻辑等价的标准形。则选择等价类中的规范代表。证明化简、数字电路优化和 SAT 预处理都依赖保持逻辑等价或至少保持可满足性。