逻辑等价

逻辑等价要求两个表达式在每个允许赋值或结构中真值相同，而不是仅在某个例子上碰巧同真或同假。固定语言与允许的结构类后，它在该语言的公式集合上形成等价关系理路等价关系Equivalence relation满足自反、对称和传递性的关系。：逐点同值保证自反、对称和传递。它把语法不同但语义不可区分的公式归入同一类，可由双向蕴涵表达，并支持在更大公式中作保持真值的替换。

找到共同的真值条件 ​

材料蕴涵给出 $P\to Q\equiv \mathrm{\neg }P\vee Q$。因此

第一步先把外层蕴含改成 $\mathrm{\neg }P\vee (Q\to R)$，再把内层改成 $\mathrm{\neg }Q\vee R$；析取的结合律允许省掉分组。另一边先得到 $\mathrm{\neg }(P\wedge Q)\vee R$，再由 De Morgan 律变成相同的式子。两边都恰好在 $P,Q$ 真而 $R$ 假时失败，所以这些变换覆盖全部赋值。若要否定等价，一行反例就够：取 $P$ 真、$Q$ 假，则 $P\to Q$ 为假，而 $Q\to P$ 为真。$P\vee Q$ 与异或也不等价，因为二者在 $P,Q$ 同真时给出不同结果。

理论相对等价不等于逻辑有效等价 ​

整数结构中 $x+x=0$ 与 $x=0$ 对每个赋值等价，但在二元域中前式对所有元素都真，后式只对零为真。因此不能脱离允许的结构类，声称二者逻辑等价。加入合适的理论公理可以排除反例结构，这正是 $T\models \phi \leftrightarrow \psi$ 中 $T$ 的作用。

等可满足只保留有无解 ​

公式 $P$ 与 $P\vee Q$ 都可满足，却在 $P$ 假、$Q$ 真时真值不同。所以同样“存在一个真赋值”远弱于“每个赋值都同真同假”。Tseitin 编码引入辅助变量时，通常得到的是投影意义上的对应：原变量的赋值满足原公式，当且仅当它能扩展成满足编码的赋值；不能把辅助变量任意赋值后仍要求两式逐点等价。

等价替换可以放进更大的经典逻辑公式中，因为联结词由子公式的真值确定。不过含量词的语法变换还要遵守变量作用域条件。例如把 $\mathrm{\exists }x(P(x)\wedge Q)$ 改成 $(\mathrm{\exists }xP(x))\wedge Q$，需要 $x$ 不自由出现在 $Q$ 中，否则会把原先同一个见证拆成不同参数。具体取 $Q$ 为 $x=0$、$P(x)$ 为 $x=1$，论域为整数。原式 $\mathrm{\exists }x(x=1\wedge x=0)$ 为假；变换后的 $(\mathrm{\exists }xx=1)\wedge x=0$ 中末尾的 $x$ 已成为自由变量，在赋值 $x=0$ 下却为真。

真值表理路真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。能穷举判定命题公式的等价性；合取范式理路合取范式Conjunctive normal form · CNF由文字的析取形成子句，再对这些子句取合取所得的命题公式形状。与析取范式理路析取范式Disjunctive normal form · DNF由文字的合取形成项，再对这些项取析取得到的命题公式形状。给出常用的等价表达形式，但一般范式写法并不唯一。数字电路优化需要保留每个输入的输出，SAT 编码则有时只需保留解的存在性或可恢复性，采用哪种变换取决于任务。