分类:数理逻辑

数理逻辑把命题、推理规则和可满足性作为研究对象。公式的写法属于语法，公式在某种解释下是否成立属于语义；辨明两者，才能准确说明一个推导系统证明了什么。

• 表达与推理：数学命题 → 演绎推理与三段论 → 反证法。
• 命题逻辑中的自动推理：可满足性 → 合取范式 → 归结原理。

可先列出少量变量的真值，再把命题化为适合计算的形式。将公式改写为合取范式时，要留意是在保留逻辑等价还是只保留可满足性；这些差别会影响后续结论。