判断有效结论的方法

推理的一般形式

G_{1} \land G_{2} \land \dots ⟹ H_{1} \lor H_{2}

写成竖式会很好看

G_{1} \land G_{2} \land \dots ⟹ H_{1} \lor H_{2}

⟺ \neg H_{1} \land G_{2} \land \dots ⟹ \neg G_{1} \lor H_{2}

结论全部拿上去，要证明结论是假

前提全部拿下来，前提就变成真（但是 True 蕴含的是无穷多的分类情况，加大了证明的难度）

(G_{1} \lor P) \land G_{2} \land \dots ⟹ H_{1} \lor H_{2}

⟺ (G_{1} \land G_{2} \land \dots ⟹ H_{1}) \lor (P \land G_{2} \land \dots ⟹ H_{2})

G_{1} \land G_{2} \land \dots ⟹ H_{1} \land H_{2}

则要证下面两个成立

G_{1} \land G_{2} \land \dots ⟹ H_{1}

G_{1} \land G_{2} \land \dots \land H_{1} ⟹ H_{2}

G_{1} \land G_{2} \land \dots ⟹ H_{1} \to H_{2}

可以把结论的前件拿到前面

G_{1} \land G_{2} \land \dots \land H_{1} ⟹ H_{2}

从前提集合 $Γ$ 推出结论 $H$ 的一个演绎是构造命题公式的一个有限序列： $H_{1}, H_{2}, \dots, H_{n}$ 其中一项是某个前提或者有效结论，并且 $H_{n}$ 就是 $H$ ，则称能从前提演绎出结论来

如果推断过程中推断出最后要证明的结论，或者前提的合取是“假”，则证明结束

[Γ, P ⟹ S] ⟺ [Γ ⟹ P \to S]

P T CP 一般写在最前面，T 的引用放在 T 的后面

PVS 计算机辅助证明

即逆否命题，把结论的否定作为前提条件，证明条件的否定即可

🪴 Cyril