// Abstract ------------------------------------------------------------------------------------------------------------------------------

This sample is capable of solving some mathematical problems (derivative, expression simplifying). It is based on Steven Tanimoto's LISP program "LEIBNIZ" (from his book "The Elements of Artificial Intelligence Using Common Lisp").

// Examples ------------------------------------------------------------------------------------------------------------------------------

?- #leibniz([d,[add,[pow,x,2],[mul,2,x]],x],:s)
-> ( [add, [mul, 2, x], 2] ) := 1.00 (0.013) 1
?- #leibniz([d,[add,[mul,x,7],[mul,8,x]],x],:s)
-> ( 15 ) := 1.00 (0.008) 1
 
// Code ----------------------------------------------------------------------------------------------------------------------------------

diff.rules { // differentiation rules

    ([d,:v?[is.atom],:v],1)^                                        :- true;
    ([d,:c?[is.atom],:v],0)^                                        :- true;

    ([d,[add,:e1,:e2],:v],[add,:d1,:d2])^                           :- #diff.rules([d,:e1,:v],:d1),
                                                                       #diff.rules([d,:e2,:v],:d2);
    ([d,[mul,:e1,:e2],:v],[add,[mul,:e2,:d1],[mul,:e1,:d2]])^       :- #diff.rules([d,:e1,:v],:d1),
                                                                       #diff.rules([d,:e2,:v],:d2);
    ([d,[pow,:e1,:n],:v],[mul,:n,[mul,[pow,:e1,[sub,:n,1]],:d1]])^  :- #diff.rules([d,:e1,:v],:d1);

    // transform what should be a statement in a prototype so that the order is preserved as fizz will
    // evaluate statements before prototypes.
    ([d,:e1,:v],[d,:e1,:v])                                         :- true;

}

simp.rules { // simplification rules

    (:n?[is.number],:n)^        :- true;
    (:s?[is.symbol],:s)^        :- true;
    ([pow,0,_],0)^              :- true;
    ([pow,_,0],1)^              :- true;
    ([pow,:x,1],:xs)^           :- #simp.rules(:x,:xs);
    ([mul,:x,1],:xs)^           :- #simp.rules(:x,:xs);
    ([mul,1,:x],:xs)^           :- #simp.rules(:x,:xs);
    ([add,:x,0],:xs)^           :- #simp.rules(:x,:xs);
    ([add,0,:x],:xs)^           :- #simp.rules(:x,:xs);
    ([mul,:x,0],0)^             :- true;
    ([mul,0,:x],0)^             :- true;

    ([add,:x?[is.number],:y?[is.number]],:z)^ :- add(:x,:y,:z);
    ([mul,:x?[is.number],:y?[is.number]],:z)^ :- mul(:x,:y,:z);
    ([div,:x?[is.number],:y?[is.number]],:z)^ :- div(:x,:y,:z);
    ([sub,:x?[is.number],:y?[is.number]],:z)^ :- sub(:x,:y,:z);
    ([pow,:x?[is.number],:y?[is.number]],:z)^ :- mao.pow(:x,:y,:z);

    // the following prototype uses the set.if.not and break.not primitives to prematurely end the inference
    // when it is detected that there isn't going to be anymore simplification of the expressions bound to the
    // variables :s1 and :s2 (thus avoiding a forever loop).
    ([:o?[is.symbol],:e1,:e2],:r) :- #simp.rules(:e1,:s1), #simp.rules(:e2,:s2),
                                     neq(:e1,:s1,:c1), neq(:e2,:s2,:c2), boo.or(:c1,:c2,:c),
                                     set.if.not([:o,:s1,:s2],:r,:c), break.not(:c),
                                     #simp.rules([:o,:s1,:s2],:r);

}

leibniz { // main of the sample, we apply differentiation then simplification

    (:e,:s) :- #diff.rules(:e,:d), #simp.rules(:d,:s);

}

// ---------------------------------------------------------------------------------------------------------------------------------------

[Home] [Email] [Twitter] [LinkedIn]