转载： http://star.aust.edu.cn/~xjfang/AiPrinciple/logical.html
逻辑等价式
| ～～A<=>A | 双重否定 |
| A∧A<=>A | 等幂律 |
| A∨A<=>A | |
| A∧B<=>B∧A | 交换律 |
| A∨B<=>B∨A | |
| (A∧B)∧C<=>A∧(B∧C) | 结合律 |
| (A∨B)∨C<=>A∨(B∨C) | |
| A∧(B∨C)<=>(A∧B)∨(A∧C) | 分配律 |
| A∨(B∧C)<=>(A∨B)∧(A∨C) | |
| A∧(A∨B)<=>A | 吸收律 |
| A∨(A∧B)<=>A | |
| ～(A∧B)<=>～A∨～B | 摩根定律 |
| ～(A∨B)<=>～A∧～B | |
| A→B<=>～A∨B | 蕴含表达式 |
| A<->B<=>(A→B)∧(B→A) | 等价表达式 |
| A∧T<=>A | |
| A∧F<=>F | |
| A∨T<=>T | |
| A∨F<=>A | |
| A∧<=>F | 矛盾律 |
| A∨～A<=>T | 排中律 |
| A→(B→C)<=>A∧B→C | 输出律 |
| (A→B)∧(A→～B)<=>～A | 归谬律 |
| A→B<=>～B→～A | 逆反律 |
 xA<=>A |
A中不含约束变元 |
 xA<=>A |
A中不含约束变元 |
| x(A(x)∧B(x))<=>xA(x)∧xB(x) |
量词分配律 |
| x(A(x)∨B(x))<=>xA(x)∨xB(x) |
|
| ～xA(x)<=>x～A(x) |
量词转换律 |
| ～xA(x)<=>x～A(x) |
|
| xA(x)∧P<=>x(A(x)∧P) |
量词辖域扩张及收缩律(P为不含约束变元x的谓词公式) |
| xA(x)∨P<=>x(A(x)∨P) |
|
| xA(x)∧P<=>x(A(x)∧P) |
|
| xA(x)∨P<=>x(A(x)∨P) |
|
| xyP(x,y)<=>yxP(x,y) |
量词交换律 |
| xyP(x,y)<=>yxP(x,y) |
|
| xA(x)→P<=>x(A(x)→P) |
量词分配律 |
| xA(x)→P<=>x(A(x)→P) |
|
| P→xA(x)<=>x(P→A(x)) |
|
| P→xA(x)<=>x(P→A(x)) |
常用逻辑蕴含式
| A==>A∨B | 附加律 |
| A∧B==>A,A∧B==>B | 简化律 |
| (A→B)∧A===>B | 假言推理 |
| (A→B)∧～B===>～A | 拒取式 |
| (A∨B)∧～A===>B | 析取三段论 |
| (A→B)∧(B→C)===>A→C | 假言三段论 |
| A→B===>(B→C)→(A→C) | |
| (A→B)∧(C→D)===>A∧C→B∧D | |
| (A<->B)∧(B<->C)===>A<->C | |
| A,B===>A∧B | |
| xA(x)===>A(y) |
全称指定规则(Universal specification,简称US) |
| xA(x)===>A(y) |
存在指定规则(Existential specification,简称ES) |
| A(y)===>xA(x) |
全称推广规则(Universal Generalization,简称UG) |
| A(y)===>xA(x) |
存在推广规则(Existential Generalization,简称EG) |
| xA(x)===>xA(x) |
|
| xA(x)∨xB(x)===>x(A(x)∨B(x)) |
|
| x(A(x)∧B(x))===>xA(x)∧xB(x) |
|
| xyP(x,y)===>yxP(x,y) |
|
| yxP(x,y)===>xyP(x,y) |
|
| xyP(x,y)===>xyP(x,y) |