命题逻辑

命题逻辑把完整陈述视为不可再分析的布尔变量，只研究“整句话的真假如何组合”。它不观察对象、量词或谓词内部结构，因此表达力有限，却拥有简单完备的真值表语义和可判定推理；公式的语法树与赋值递归决定真值，真值表也由此提供有限、机械的语义检查方法。

$P\vee \mathrm{\neg }P$ 是重言式；$P\wedge \mathrm{\neg }P$ 不可满足。命题逻辑不能表达“所有对象”或“存在某个对象”，这些量化结构需要一阶逻辑。

公式

在赋值 $P=\mathrm{\top },Q=\mathrm{\perp },R=\mathrm{\top }$ 下为真，而在 $P=\mathrm{\top },Q=\mathrm{\perp },R=\mathrm{\perp }$ 下为假。命题逻辑只把 $P,Q,R$ 当作整体真假值，不分析它们内部谈论的对象。因而它能机械检查有限布尔组合，却不能在固定有限公式中表达“每个自然数都有后继”这类量化结构；这需要一阶逻辑公理库一阶逻辑First-order logic · Predicate logic在命题逻辑上加入对象、关系、函数与量词的形式语言和模型语义。。

真值表公理库真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。判定永真与等价，合取范式公理库合取范式Conjunctive normal form · CNF由若干析取子句之合取构成且与原公式逻辑等价的标准形。连接 SAT、布尔电路与数字电路验证；程序条件表达式的推理也建立在这一层上。自然演绎、相继式演算和 可靠性与完备性公理库命题逻辑可靠性与完备性定理Soundness and completeness of propositional logic命题演算中的可证性与对所有赋值成立的语义蕴涵恰好一致。共同建立语法—语义闭环。

有界模型检查公理库有界模型检查Bounded model checking · BMC · SAT-based bounded model checking将前 k 步转移展开为 SAT 公式寻找有界反例，并明确无解结果何时不能升级为全局证明。把有限步转移与坏状态编码成命题公式，PDR/IC3公理库Property-Directed Reachability / IC3Property-directed reachability · PDR · IC3以 SAT 查询阻塞坏状态前驱、学习逐层归纳子句，最终得到反例或安全归纳不变式。则从 SAT 反例中学习归纳子句。二者使用命题逻辑作为求解接口，但要验证的对象仍是状态系统，性质是否成立也仍量化其全部相关执行。