等值式：如果A?B是重言式那么稱A与B等值的，记为A?B并称A?B为等值式
（1）双重否定律A?￢￢A
（2）幂等律A∨A?A，A∧A?A
（3）交换律A∨B?B∨AA∧B?B∧A
（4）结合律（A∨B）∨C?A∨（B∨C），（A∧B）∧C?A∧（B∧C）
（5）分配率A∨（B∧C）?（A∨B）∧（A∨C）A∧（B∨C）?（A∧B）∨（A∧C）
（6）德摩根律￢（A∨B）?￢A∧￢B，￢（A∧B）?￢A∨￢B
（7）吸收律A∨（A∧B）?AA∧（A∨B）?A
（8）零律A∨1?1，A∧0?0
（9）同一律A∨0?AA∧1?A
（10）排中律A∨￢A?1
（11）矛盾律A∧￢A?0
（12）蕴涵等值式A→B?￢（A∨B）
（13）等价等值式A?B?（A→B）∧（B→A）
（14）假言异位A→B?￢B→￢A
（15）等价否定等值式A?B?￢A?￢B
（16）归谬论（A→B）∧（A→￢B）?￢A
等值演算求主析取范式算：由已知的等值式推算出新的等值式的过程
置换规则：如果A?B，那么Φ（A）?Φ（B）
重言式与矛盾式的判别法：A为重言式当且仅当A?1；A为矛盾式，当且仅当A?0
定理：在命题逻辑中任何公式都存在与之等值的主析取范式和主合取范式，并且它们是惟一的
求公式A的主析取范式的方法与步骤：
（1）方法一 等值演算求主析取范式算法：
S1：消去A中联结词→?（若存在）
S2：否萣联结词的内移（￢（A?∨A?）?￢A?∧￢A?，￢（A?∧A?）?￢A?∨￢A?）
或消去（￢￢A??￢￢A?）
S3：使用分配率（A?∧（A?∨A3）?（A?∧A?）∨（A?∧A3））
以上3步将A等值的化成析取范式
S4：将析取范式中不是极小项的简单合取式利用排中律、同一律、分配率化成若干个極小项
S5：将极小项用名称mi表示使用幂等律，最后排序
（2）方法二 真值表法
S2：找出A的成真赋值
S3：写出每个成真赋值对应的极小项（用名称表示）按角标从小到大顺序析取
求公式A的主合取范式的方法与步骤：
（1）方法一 等值演算求主析取范式算法
（2）方法二 真值表法：
S2：写絀A的成假赋值
S3：写出每个成假赋值对应的极大项（用名称表示），按角标从小到大顺序合取
（2）方法三 由A的主析取范式求A的主合取范式
主析取范式的用途（与真值表相同）
（1）求公式的成真赋值和成假赋值
（3）判断两个公式是否等值
真值函数：n元真值函数F：{01}n→{0，1}
任何一个含n个命题变项的命题公式A都惟一的存在一个n元真值函数与之等值。
如果A,B与同一个真值函数等值那么A?B
联结词完备集：{￢，∧∨，→?}，{￢∧，∨}{￢，∧∨，→}{￢，∧}{￢，∨}{￢，→}{↑}，{↓}
消解规则：设C?和C?是两个简单析取式C?含文字l，C?含lc（lc=￢l）从C?中删去l，从C?中删去lc然后将所得的结果析取成一个简单析取式，称这样得到的简单析取式为C?和C?的（以l和lc为消解文字的）消解式或消解结果记为Res（C?，C?）由C?和C?得到Res（C?C?）的规则称为消解规则。
合取范式的消解序列和否证：若简单析取式序列C?C?，…Cn中的每一个Ci（1≤i≤n）都是合取范式S中得一个简单析取式，或者是它之前的某两个简单析取式CjCk（1≤j＜k≤i）的消解结果，则称此序列是甴S导出Cn的消解序列
当Cn=λ（空简单析取式）时，称次序列是S的一个否证
定理：一个合取范式是不可满足的当且仅当它有否证
消解法：利鼡消解规则求解可满足性问题（判断任意给定的合式公式是否是可满足的）的算法
