metainterpreter

fact(is_a(a,b)).
fact(is_a(b,c)).
rule((is_aT(A,B) :- is_a(A,B))).
rule((is_aT(A,B) :- is_a(A,Z),is_aT(Z,B))).


prove(Goal,[Goal]) :-
        fact(Goal).
prove(Goal, [Rule|Steps]) :-
        Rule = rule( (Goal :- Body) ),
        Rule,
        prove(Body, Steps).
prove((A,B), Steps) :-
        prove(A,Steps1),
        prove(B,Steps2),
        % append is ugly - should really return a proof tree not list
        append(Steps1,Steps2,Steps).
prove((G;_), Steps) :-
        prove(G,Steps).
prove((_;G), Steps) :-
        prove(G,Steps).

t :-
        prove(is_aT(a,c),Steps),
        writeln(proof=Steps).



    

To test:

$ swipl -l metalog.pl -g t
proof=[rule((is_aT(a,c):-is_a(a,b),is_aT(b,c))),is_a(a,b),rule((is_aT(b,c):-is_a(b,c))),is_a(b,c)]