千问总结：
第三节：重言式及其判定方法
1. 重言式、矛盾式与偶真式
- 重言式：对于任意命题变项的真值指派，其值始终为真的真值形式。
- 矛盾式：对于任意命题变项的真值指派，其值始终为假的真值形式。
- 偶真式：存在某些真值指派下值为真，另一些真值指派下值为假的真值形式。
2. 性质与关系
- 重言式与矛盾式的关系：一个真值形式是重言式，当且仅当其否定式为矛盾式。
- 非重言式：一个真值形式不是重言式，当且仅当存在至少一组真值指派使其取值为假。
- 非矛盾式：一个真值形式不是矛盾式，当且仅当存在至少一组真值指派使其取值为真。
- 偶真式判定：一个真值形式是偶真式，当且仅当它既非重言式也非矛盾式。
3. 重言式代入定理
- 若A是重言式，包含n个命题变项p1, p2, ..., pn，用公式C1, C2, ..., Cn分别替换A中每个变项的每次出现得到的公式B，B也是重言式。
代入要求：
- 仅代入命题变项：仅能替换真值形式中的命题变项，不能替换其他复合公式。
- 处处代入：在被代入变项出现的每一个位置上，用同一个公式替换该变项。
- 同时代入：对n个变项做代入时，必须同时用相同的公式替换每个变项。
4. 判定重言式的方法
真值表方法
- 列出所有可能的真值组合：针对公式中所有不同的命题变项，列出所有可能的真值组合。
- 逐层计算子公式直至公式本身的真值：按照公式的生成顺序，由简单到复杂列出子公式，根据真值联结词的真值表，逐步计算出各子公式及公式本身的真值。
- 根据真值判断公式类型：若公式恒取值为真，为重言式；恒取值为假，为矛盾式；有时取值为真、有时取值为假，为偶真式。
归谬赋值法
- 假设公式为假：设定待判定公式取值为假。
- 逆推赋值寻找矛盾：按照联结词的真值表，由公式主联结词的假值逆推出子公式的真值，直至命题变项的真值，检查赋值过程中是否存在矛盾。若出现矛盾，说明公式不可能为假，必定是重言式。
树形图方法
- 构造倒置树形图：假设待判定公式为假（即其否定为真），按照画图规则构建倒置树形图。
- 判断封闭性与终结性：每个树枝末端为命题变项或其否定，且树形图已不再能进行等值变换时，树形图视为终结。若树形图中每个树枝均为封闭（即包含某个公式与其否定），则原公式为重言式。
本节总结了重言式、矛盾式与偶真式的定义、相互关系、重言式代入定理，以及三种判定重言式的方法（真值表法、归谬赋值法、树形图法）的概念、原理与应用实例。
kimi总结：
重言式及其判定方法
一、重言式定义
- 重言式：对于任何命题变项的真值指派都恒为真的真值形式。
- 矛盾式：对于任何命题变项的真值指派都恒为假的真值形式。
- 偶真式：对于某些命题变项的真值指派为真，而另一些指派为假的真值形式。
二、重言式判定方法
真值表方法
步骤：
- 列出所有不同的命题变项及其可能的真值组合。
- 根据公式结构列出所有子公式。
- 根据真值联结词的真值表计算子公式的真值，直至公式本身的真值。
归谬赋值法
步骤：
- 假设待判定公式为假。
- 逆推子公式的真值，直至命题变项。
- 检查是否存在矛盾赋值。
- 如果出现矛盾，公式为重言式；否则，不是重言式。
树形图方法
规则：
- 构造树形图，每个节点代表一个公式。
- 应用画图规则，直到每个树枝封闭或终结。
判定：
- 如果每个树枝都是封闭的，公式为重言式。
- 如果至少有一个树枝未封闭，公式不是重言式。
三、常用重言式示例
- 同一律：
A → A - 排中律：
A ∨ ¬A - 矛盾律：
¬(A ∧ ¬A) - 条件传递律：
(A → (B → C)) → ((A → B) → (A → C)) - 等值自返律：
A ↔ A
四、逻辑规律的应用
- 重言式在逻辑推理中作为推理的有效性和公式恒真的依据。
- 通过归谬赋值法和树形图方法可以验证推理的有效性和公式集的可满足性。
五、复杂情形的处理
- 在归谬赋值法中，可能需要考虑多种赋值选择，只有所有选择都导致矛盾时，才能确定公式为重言式。
- 树形图方法中，需要确保每个树枝都是封闭的，以判断公式为重言式。
prompt：请用markdown结构化输出下文的总结：