$$ (A\lor C)\land(B\lor \neg C)\Leftrightarrow A \lor B $$
消解律の使用范围
消解律中的 $A$, $B$, $C$ 都是文字，不能是式子！！
解证明推理问题
- 把 前提 & 结论否定 化为合取范式
- 用 1. 得到公式进行消解推理
- 如果得到空式 $\lambda$，则证明推理正确
解可满足性问题
- 假定公式不可满足
- 把公式化为合取范式
- 对每个析取项两两消解
- 如果推出空子式 $\lambda$，假定成立，不可满足
- 如果消解为最简后仍无空子式 $\lambda$，假定不成立，可满足