待解释公式
解释空间探索
通过遍历所有可能的解释,我们可以判断公式的逻辑性质
公式分类判定
永真式 (Tautology)
在所有解释下都为真的公式,代表普遍真理
例: ∀x(P(x) ∨ ¬P(x)) - 排中律
永假式 (Contradiction)
在所有解释下都为假的公式,代表逻辑矛盾
例: ∀x(P(x) ∧ ¬P(x)) - 矛盾律
可满足式 (Satisfiable)
至少存在一个解释使公式为真,代表理想可实现
例: ∃x(奋斗(x) ∧ 成功(x))