 <p>Math expressions can be very complex, I presume you are referring to arithmetic instead. The normal form (I hope my wording is appropriate) is 'sum of monomials'.</p> <p>Anyway, it's not an easy task to solve generally, and there is an ambiguity in your request: 2 expressions can be syntactically different (i.e. their syntax tree differ) but still have the same value. Obviously this is due to operations that leave unchanged the value, like adding/subtracting 0.</p> <p>From your description, I presume that you are interested in 'evaluated' identity. Then you could normalize both expressions, before comparing for equality.</p> <p>To evaluate syntactical identity, I would remove all parenthesis, 'distributing' factors over addends. The expression become a list of multiplicative terms. Essentially, we get a list of list, that can be sorted without changing the 'value'.</p> <p>After the expression has been flattened, all multiplicative constants must be accumulated. </p> <p>a simplified example:</p> <p><code>a+(b+c)*5</code> will be <code>[[1,a],[b,5],[c,5]]</code> while <code>a+5*(c+b)</code> will be <code>[[1,a],[5,c],[5,b]]</code></p> <p><strong>edit</strong> after some improvement, here is a <em>very</em> essential normalization procedure:</p> <pre><code>:- [library(apply)]. arith_equivalence(E1, E2) :- normalize(E1, N), normalize(E2, N). normalize(E, N) :- distribute(E, D), sortex(D, N). distribute(A, [[1, A]]) :- atom(A). distribute(N, [[1, N]]) :- number(N). distribute(X * Y, L) :- distribute(X, Xn), distribute(Y, Yn), % distribute over factors findall(Mono, (member(Xm, Xn), member(Ym, Yn), append(Xm, Ym, Mono)), L). distribute(X + Y, L) :- distribute(X, Xn), distribute(Y, Yn), append(Xn, Yn, L). sortex(L, R) :- maplist(msort, L, T), maplist(accum, T, A), sumeqfac(A, Z), exclude(zero, Z, S), msort(S, R). accum(T2, [Total|Symbols]) :- include(number, T2, Numbers), foldl(mul, Numbers, 1, Total), exclude(number, T2, Symbols). sumeqfac([[N|F]|Fs], S) :- select([M|F], Fs, Rs), X is N+M, !, sumeqfac([[X|F]|Rs], S). sumeqfac([F|Fs], [F|Rs]) :- sumeqfac(Fs, Rs). sumeqfac([], []). zero([0|_]). mul(X, Y, Z) :- Z is X * Y. </code></pre> <p>Some test:</p> <pre><code>?- arith_equivalence(a+(b+c), (a+c)+b). true . ?- arith_equivalence(a+b*c+0*77, c*b+a*1). true . ?- arith_equivalence(a+a+a, a*3). true . </code></pre> <p>I've used some SWI-Prolog builtin, like include/3, exclude/3, foldl/5, and <a href="http://www.swi-prolog.org/pldoc/doc_for?object=msort/2" rel="nofollow">msort</a>/2 to avoid losing duplicates.</p> <p>These are basic <a href="http://www.swi-prolog.org/pldoc/doc_for?object=section%282,%27A.2%27,swi%28%27/doc/Manual/apply.html%27%29%29" rel="nofollow">list manipulation</a> builtins, easily implemented if your system doesn't have them.</p> <p><strong>edit</strong></p> <p>foldl/4 as defined in SWI-Prolog apply.pl:</p> <pre><code>:- meta_predicate foldl(3, +, +, -). foldl(Goal, List, V0, V) :- foldl_(List, Goal, V0, V). foldl_([], _, V, V). foldl_([H|T], Goal, V0, V) :- call(Goal, H, V0, V1), foldl_(T, Goal, V1, V). </code></pre> <p><strong>handling division</strong></p> <p>Division introduces some complexity, but this should be expected. After all, it introduces a full <em>class</em> of numbers: rationals.</p> <p>Here are the modified predicates, but I think that the code will need much more debug. So I allegate also the 'unit test' of what this micro rewrite system can solve. Also note that I didn't introduce the negation by myself. I hope you can work out any required modification.</p> <pre><code>/* File: arith_equivalence.pl Author: Carlo,,, Created: Oct 3 2012 Purpose: answer to http://stackoverflow.com/q/12665359/874024 How to check if two math expressions are the same? I warned that generalizing could be a though task :) See the edit. */ :- module(arith_equivalence, [arith_equivalence/2, normalize/2, distribute/2, sortex/2 ]). :- [library(apply)]. arith_equivalence(E1, E2) :- normalize(E1, N), normalize(E2, N), !. normalize(E, N) :- distribute(E, D), sortex(D, N). distribute(A, [[1, A]]) :- atom(A). distribute(N, [[N]]) :- number(N). distribute(X * Y, L) :- distribute(X, Xn), distribute(Y, Yn), % distribute over factors findall(Mono, (member(Xm, Xn), member(Ym, Yn), append(Xm, Ym, Mono)), L). distribute(X / Y, L) :- normalize(X, Xn), normalize(Y, Yn), divide(Xn, Yn, L). distribute(X + Y, L) :- distribute(X, Xn), distribute(Y, Yn), append(Xn, Yn, L). sortex(L, R) :- maplist(dsort, L, T), maplist(accum, T, A), sumeqfac(A, Z), exclude(zero, Z, S), msort(S, R). dsort(L, S) :- is_list(L) -&gt; msort(L, S) ; L = S. divide([], _, []). divide([N|Nr], D, [R|Rs]) :- ( N = [Nn|Ns], D = [[Dn|Ds]] -&gt; Q is Nn/Dn, % denominator is monomial remove_common(Ns, Ds, Ar, Br), ( Br = [] -&gt; R = [Q|Ar] ; R = [Q|Ar]/[1|Br] ) ; R = [N/D] % no simplification available ), divide(Nr, D, Rs). remove_common(As, [], As, []) :- !. remove_common([], Bs, [], Bs). remove_common([A|As], Bs, Ar, Br) :- select(A, Bs, Bt), !, remove_common(As, Bt, Ar, Br). remove_common([A|As], Bs, [A|Ar], Br) :- remove_common(As, Bs, Ar, Br). accum(T, [Total|Symbols]) :- partition(number, T, Numbers, Symbols), foldl(mul, Numbers, 1, Total), !. accum(T, T). sumeqfac([[N|F]|Fs], S) :- select([M|F], Fs, Rs), X is N+M, !, sumeqfac([[X|F]|Rs], S). sumeqfac([F|Fs], [F|Rs]) :- sumeqfac(Fs, Rs). sumeqfac([], []). zero([0|_]). mul(X, Y, Z) :- Z is X * Y. :- begin_tests(arith_equivalence). test(1) :- arith_equivalence(a+(b+c), (a+c)+b). test(2) :- arith_equivalence(a+b*c+0*77, c*b+a*1). test(3) :- arith_equivalence(a+a+a, a*3). test(4) :- arith_equivalence((1+1)/x, 2/x). test(5) :- arith_equivalence(1/x+1, (1+x)/x). test(6) :- arith_equivalence((x+a)/(x*x), 1/x + a/(x*x)). :- end_tests(arith_equivalence). </code></pre> <p>running the unit test:</p> <pre><code>?- run_tests(arith_equivalence). % PL-Unit: arith_equivalence ...... done % All 6 tests passed true. </code></pre>