轉載： 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) |