一、重言式、矛盾式和偶真式
命题逻辑的公式种类繁多，无穷无尽。我们可以根据公式的真值情况，将其分为重言式、矛盾式和偶真式三类。
重言式是指在一个公式中，不论其中的命题变项取何值，该公式总是为真。也就是说，重言式是命题逻辑中的有效推理形式，如“p→p”和“（p∧p）”等。
矛盾式则是无论命题变项如何取值，该公式总是为假。例如，“p∧p”就是一个矛盾式。
偶真式则是指在某些情况下为真，在另一些情况下为假。如“q↔（s∧t）”就是一个偶真式。
重言式又称为命题逻辑的有效式，而矛盾式和偶真式则合称为非有效式。重言式和偶真式又可以统称为可满足式。
二、重言式的判定
在命题逻辑中，我们需要找出所有的重言式。如果有一个方法可以在有限步骤内确定一个给定的公式是否是重言式，那么我们就有了判定程序。这个判定程序需要满足三个条件：每一步都是由事先规定的规则决定的、可以在有限步骤内结束、能够给出唯一的结论。
接下来，我们将介绍三种判定程序：真值表法、归谬赋值法和树形图法。
1. 真值表法
真值表法的步骤是：首先找出公式中所有的命题变项，并列出它们所有可能的真值组合。然后按照公式的生成顺序，列出所有子公式的真值，直至原公式本身。最后根据真值联结词的真值表，计算出各个子公式和原公式的真值。如果原公式恒为真，则为重言式；如果恒为假，则为矛盾式；如果有时为真有时为假，则为偶真式。
例如，对于公式“（（p→q）∧p）→q”，我们可以通过真值表法来判断它是否是重言式。在真值表中，我们可以列出所有可能的p和q的值，并计算公式的值。如果对于所有的赋值，公式的值都是真，那么它就是重言式。
2. 归谬赋值法
归谬赋值法是真值表法的简化版本。它的基本思路是：如果A是重言式，那么无论给A中的变项指派什么真值，A都必须为真。我们可以假设A不是重言式，然后按照联结词的真值表逆推出子公式的真值，看是否能导致矛盾的赋值。如果能，那么原假设不成立，A必须是重言式。
归谬赋值法的具体做法包括写出待判定的公式、在主联结词下写0、按照联结词的真值表逆推出子公式的真值、检查赋值中是否出现矛盾。如果出现矛盾，则该公式是重言式；否则，该公式可以为假，不是重言式。
3. 树形图法
树形图法是归谬赋值法的另一种表现形式。它的基本思路是：假设待判定公式A为假，然后按照树形图的规则往下画。如果一个树枝上同时含有一个公式和它的否定公式，那么这个树枝就是封闭的。如果树形图中的每一个树枝都是封闭的，那么A就是重言式。树形图不仅可以判定一个公式是否是重言式，还可以判定一个公式是否矛盾。
