rule(0+X,X). rule(X+0,X). rule(1*X,X). rule(X*1,X). rule(1*X,X). rule(0*_,0). rule(_*0,0). rule(sum(_,0),0). rule((X+Y)*Z, (X*Z)+(Y*Z)). rule(X*(Y+Z), X*Y + X*Z). rule(X+(Y+Z), X+Y+Z). rule(X*(Y*Z), X*Y*Z). rule(X+Y, Y+X) :- X @< Y. rule(X*Y, Y*X) :- X @< Y. rule(X+Y+Z, X+Z+Y) :- Y @< Z. rule(X*Y*Z, X*Z*Y) :- Y @< Z. rule(X+X, X*2). rule(d(V,X + Y), d(V,X) + d(V,Y)). rule(d(V,X*Y), d(V,X) * Y + X * d(V,Y)). rule(d(V,V), 1). rule(d(V,N), 0) :- number(N); atom(N), V \= N. rule(d(V,sum(I,T)), sum(I,d(V,T))). rule(d(V,X),D * d(V,A)) :- X =.. [F,A], atomic_concat(F,'`',FD), D =.. [FD,d(V,A)]. applyrules(P,X,TX) :- call(P,X,T), !, applyrules(P,T,TX), !. applyrules(_,X,X). treplacelist(_,[],[]) :- !. treplacelist(P,[H|T], [HR|TR]) :- treplace(P,H,HR), treplacelist(P,T,TR), !. treplace(X,TX) :- treplace(rule,X,TX). treplace(P,X,TX) :- applyrules(P, X, XR), XR =.. [F|L], treplacelist(P, L,LR), XRR =.. [F|LR], applyrules(P, XRR, XRRR), !, (XRR \= XRRR, !, treplace(P,XRRR,TX); XRRR = TX). subst(V,S,V,S) :- !. subst(_,_,[],[]) :- !. subst(V,S,[H|T],[HS|TS]) :- !, subst(V,S,H,HS), subst(V,S,T,TS), !. subst(V,S,T,TS) :- !, T =.. [TF|Args], subst(V,S,Args,Sargs), TS =.. [TF|Sargs], !. printLtx(T) :- treplace(printrule,T,T1), !, print('$$'), write_term(T1,[]), print('$$'), nl. printrule(d(V,T), R) :- atomic_list_concat(['\\frac{d}{d', V, '}'], P), R =.. [P,T]. printrule(sum(V,T), R) :- atomic_list_concat(['\\sum_{', V, '}'], P), R =.. [P,T]. printrule(ind(V,T), R) :- T=.. [F|A], atomic_list_concat(['{', F, '}_{', V, '}'], P), R =.. [P|A]. printEval(T) :- print(T), nl, treplace(T,TR), print(TR), nl, printLtx(T=TR), nl, nl. /* treplace is the term replacer, printLtx prints a LaTeX representation of a term, e.g. for use with MathJax. d(V,T) means the derivation of term T after variable V. subst is term substitution> subst(Term,SubstitutedBy,InTerm,Result) */