真值表

真值表把所有可能世界逐行列完：穷举公式中不同命题变量的布尔赋值，再按语法树逐列机械计算复合公式真值。只要没有遗漏赋值，最后一列就完整刻画公式语义；检查全真、至少一真或两列相同，可分别判断永真、可满足与等价。代价随变量数指数增长，因此它概念完整，却不适合大规模计算。

$p\vee \mathrm{\neg }p$ 的两行都为真；$p\wedge \mathrm{\neg }p$ 的两行都为假。含 $n$ 个实际出现变量的公式需要 $2^n$ 行，而不是按语言中所有潜在变量计数。变量重复出现必须在同一行取相同值。真值表能判定命题公式，但指数行数使它不等于高效 SAT 算法，也不能直接穷举含无限论域量词的一阶语义。

对 $P\to Q$ 的四种赋值，只有 $P$ 真且 $Q$ 假的一行结果为假。比较 $P\to Q$ 与 $\mathrm{\neg }P\vee Q$ 的列可见完全一致。若同一变量重复出现，赋值数仍按不同变量计，而不是按出现次数计；漏掉某行就可能错判永真性。

永真式公理库永真式Tautology · Valid propositional formula在每个真值赋值下均为真的命题公式。、可满足公式公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。与 逻辑等价公理库逻辑等价Logical equivalence两个公式在指定语义类的每个结构与赋值下具有相同真值。都可由真值表定义性检验。它还用于构造 CNF/DNF、检查电路和讲解联结词语义，既给出命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。可判定性的直接证明，也是布尔函数的完整表示。Karnaugh 图、BDD 与 SAT 求解器则试图避免完整穷举，同时保留同一套布尔语义。