Algebraic Laws in Prolog

Algebra.pl

% Introduce reflexive equality
refl(X, X).

% Introduce symmetrical equality
sym(X, Y) :- 
	refl(X, Y),
	refl(Y, X).

% Identity of addition by zero
add_zero(N) :- 
	N1 is N + 0,
	refl(N, N1).

% Identity of multiplication by one
mul_one(N) :-
	N1 is N * 1,
	refl(N, N1).

% Commutativity of addition
commute_add(N, M) :-
	N1 is N + M,
	M1 is M + N,
	refl(M1, N1).

% Commutativity of multiplication
commute_mul(N, M) :-
	N1 is N * M,
	M1 is M * N,
	refl(N1, M1).

% Associativity of addition
assoc_add(M, N, O) :-
	R is M + N + O,
	L is N + O + M,
	refl(R, L).

% Associativity of multiplication
assoc_mul(M, N, O) :-
	R is M * N * O,
	L is N * O * M,
	refl(R, L).

% Distributive property
distribute(X, Y, Z) :-
	LI is Y + Z,
	L is X * LI,
	R1 is X * Y,
	R2 is X * Z,
	R is R1 + R2,
	refl(R, L).

% Inverse property of addition
inverse_add(X) :-
	I is -1 * X,
	E is X + I,
	refl(E, 0).

% Inverse property of multiplication
inverse_mul(X) :-
	X =\= 0,
	I is 1 / X,
	E is I * X,
	refl(E, 1).

% Transitive property
transitive(X, Y, Z) :-
	refl(X, Y),
	refl(Y, Z),
	refl(X, Z).

% Transitivity of addition
transitive_add(X, Y, K) :-
	refl(X, Y),
	X1 is X + K,
	Y1 is Y + K,
	refl(X1, Y1).

% Transitivity of multiplication
transitive_mul(X, Y, K) :-
	refl(X, Y),
	X1 is X * K,
	Y1 is Y * K,
	refl(X1, Y1).