Prolog 的语法很奇怪,需要一些时间来适应,所以我花了点时间,想用Prolot来表示和验证离散逻辑的16组等价公式。

1. 双重否定律 (Double Negation Law)

A ⇔¬¬A
首先，我们来看看双重否定律。在 Prolog 中，我们可以这样验证它：

fun1(A,Z):-
    member(A,[false,true]),
    (((Z1 = not(A),Z2=not(Z1)) , equal(A,Z2)) ->Z=true;Z=false),
    format('A = ~w , Z = ~w~n',[A,Z]),fail.

这个函数检查一个值和它的双重否定是否相等。是不是感觉就像在镜子里看镜子？

2. 幂等律 (Idempotent Laws)

A ⇔ A∨A
A ⇔ A∧A
接下来是幂等律，这听起来像是一种超级能力，但实际上它很简单：

fun2_1(A,Z):-
    member(A,[false,true]),
    (((Z1=(A;A)),equal(A,Z1))->Z=true;Z=false),
    format('A = ~w , Z = ~w~n',[A,Z]),fail.

fun2_2(A,Z):-
    member(A,[false,true]),
    (((Z1=(A,A)),equal(A,Z1))->Z=true;Z=false),
    format('A = ~w , Z = ~w~n',[A,Z]),fail.

就像说“给我再多的杨幂，不如只给我一个杨幂就够了"。

3. 交换律 (Commutative Laws)

A∨B ⇔ B∨A
A∧B ⇔ B∧A
交换律告诉我们，顺序不重要，就像在决定先穿袜子还是裤子一样：

fun3_1(A,B,Z):-
    member(A,[false,true]),
    member(B,[false,true]),
    ((Z1=(A;B),Z2=(B;A),equal(Z1,Z2))->Z=true;Z=false),
    format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.
  
  fun3_2(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Z1=(A,B),Z2=(B,A),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.

4. 结合律 (Associative Laws)

(A∨B)∨C ⇔ (A∨(B∨C)
(A∧B)∧C ⇔ (A∧(B∧C)
结合律就像是一位擅长变魔术的艺术家。就像是在告诉我们：“不管你怎么组合这些逻辑片段，结果都像是经过了魔术师的手，神奇地保持不变！”

fun4_1(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Z1=((A;B);C),Z2=((A;(B;C)),equal(Z1,Z2)))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.

fun4_2(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Z1=((A,B),C),Z2=((A,(B,C)),equal(Z1,Z2)))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.

5. 分配律 (Distributive Laws)

A∨(B∧C) ⇔ (A∨B)∧(A∨C)
A∧(B∨C) ⇔ (A∧B)∨(A∧C)
分配律像是在进行一场精彩的逻辑舞蹈。它轻松地在不同逻辑结构之间跳跃

fun5_1(A,B,C,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
 	member(C,[false,true]),
	(((Z1=(A;(B,C))),(Z2=((A;B),(A;C))),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w , C = ~w , Z = ~w~n',[A,B,C,Z]),fail.

fun5_2(A,B,C,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
 	member(C,[false,true]),
	(((Z1=(A,(B;C))),(Z2=((A,B);(A,C))),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w , C = ~w , Z = ~w~n',[A,B,C,Z]),fail.

6. 德摩根律 (De Morgan Laws)

¬(A∨B) ⇔ ¬A∧¬B
¬(A∧B) ⇔ ¬A∨¬B
德摩根律就像是逻辑世界的一面镜子。当你通过这面镜子看逻辑表达式时，一切都被反转了，但令人惊奇的是，结果依然成立！

fun6_1(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Y1=(A;B),Z1=(\+Y1),Z2=(\+A,\+B),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.
fun6_2(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Y1=(A,B),Z1=(\+Y1),Z2=(\+A;\+B),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.

7. 吸收根律 (Absorption Laws)

A∨(A∧B) ⇔ A
A∧(A∨B) ⇔ A
吸收根律就像是一个厨师，能将一桌丰盛的菜肴减少到最基本的几样，但味道依然美妙

fun8_1(A,Z):-
	member(A,[false,true]),
	(((Z1=(A;true)),equal(Z1,true))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

fun8_2(A,Z):-
	member(A,[false,true]),
	(((Z1=(A,false)),equal(Z1,false))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

8. 9. 零律和同一律 (Domination Laws & Identity Laws)

A∧1 ⇔ A
A∨0 ⇔ A
零律和同一律就像则是Prolog中的基本常量，它们是逻辑世界中的稳定点，始终如一

fun8_1(A,Z):-
	member(A,[false,true]),
	(((Z1=(A;true)),equal(Z1,true))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

fun8_2(A,Z):-
	member(A,[false,true]),
	(((Z1=(A,false)),equal(Z1,false))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.
	fun9_1(A,Z):-
	member(A,[false,true]),
	(((Z1=(A,true)),equal(Z1,A))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

fun9_1(A,Z):-
	member(A,[false,true]),
	(((Z1=(A,true)),equal(Z1,A))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

fun9_2(A,Z):-
	member(A,[false,true]),
	(((Z1=(A;false)),equal(Z1,false))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

10. 11. 排中律与矛盾律 (Law of the Excluded Middle Laws & Law of Contradiction )

A∨¬A ⇔ 1
A∧¬A ⇔ 0
排中律与矛盾律这两个法则展示了逻辑的极端情况，一方面是充分性，另一方面是不可能性。

fun10(A,Z):-
	member(A,[false,true]),
	(((Z1=(A;\+A)),equal(Z1,true))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

fun11(A,Z):-
	member(A,[false,true]),
	(((Z1=(A,\+A)),equal(Z1,false))->Z=true;Z=false),
	format('A = ~w , Z = ~w~n',[A,Z]),fail.

12. 13. 蕴涵律和等价律 (Implication Laws & Eqivalence Laws)

A→B ⇔ ¬A∨B
A↔B ⇔ (A→B )∧(B→A)
蕴涵律和等价律是理解逻辑关系的核心

fun12(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Z1=(A->B;true),Z2=(\+A;B),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.
	
fun13(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Z1=equal(A,B),Z2=(contain(A,B),contain(B,A)),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.

14. 15. 假言易位律与等价否定律 (Contraposition Laws and Negation of Equivalence Laws)

A→B ⇔ ¬B→¬A
A↔B ⇔ ¬A↔¬B
假言易位律与等价否定律展示了逻辑表达式的巧妙转换，就像是逻辑世界的变形术，展示了多种面貌

fun14(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Z1=contain(A,B),Y1=(\+B),Y2=(\+A),Z2=(contain(Y1,Y2)),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.
	
fun15(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Z1=equal(A,B),Y1=(\+A),Y2=(\+B),Z2=(equal(Y1,Y2)),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.

16. 归谬律 (Reductio ad Absurdum)

(A→B) ∧(A→¬B) ⇔ ¬A
归谬律是Prolog中逻辑推理的终极检验，它揭示了逻辑中的悖论和矛盾

fun16(A,B,Z):-
	member(A,[false,true]),
	member(B,[false,true]),
	((Y1=(\+B),Z1=(contain(A,B),contain(A,Y1)),Z2=(\+A),equal(Z1,Z2))->Z=true;Z=false),
	format('A = ~w , B = ~w, Z = ~w~n',[A,B,Z]),fail.