% The simpliest metainterpreter - and it can interpret ITSELF prove(true). prove((A,B)) :- prove(A), prove(B). prove(A) :- built_in(A),A. prove(A) :- clause(A,B), prove(B). built_in(clause(_,_)). % clause(true,true). - it fails because of clause(clause(true,true),L) fails; % or (A,B) -> modify the last clause into % prove(A) :- predicate_property(A,interpreted), % clause(A,B), prove(B). % Add cuts into 1st,2nd ... :- !, ... % Built-in % prove(A) :- predicate_property(A,built-in),!,call(Goal). % it becomes the 3rd clause %%%%%%%%%%%% % Handling cuts prove1(Goal) :- rule(Goal, Before, Cut, After), prove1_body(Before), ifthen(Cut=:=1,!), prove1_body(After). prove1_body([]). prove1_body([Goal|Goals]) :- prove1(Goal), prove1_body(Goals). rule(a(1), [b,c],0,[]). % a(1) :- b,c. rule(a(2), [],0,[]). % a(2). rule(b,[],0,[]). % b. rule(c,[d],1,[f]). % c :- d,!,f. rule(d,[],0,[]). % d. %rule(f,[],0,[]). % f. a(1) :- b,c. a(2). b. c :- d,!,f. d. cc :- (d,!)=..L. %%%%%%%%%%%% % Metainterpreter saving the trace solve(','(A,B),In,Out) :- solve(A,In,Out1),solve(B,Out1,Out). solve(A,In,Out) :- clause(A,B), append(In,[A],Out1), solve(B,Out1,Out). solve(true,In,In). solve(A,In,Out) :- A, append(In,[A],Out). r:- solve(fib(3,F),[],L),write(L), L=[H|B],assert(':-'(H,B)). %%%%%%%%% /* % A Depth-Bounded Interpreter solve(P,X) :- solve(P,25,X), (X \== true, !; true). solve(true,D,true) :- !. solve(A,0,(overflow,[])) :- !. solve((A,B),D,S) :- !, solve(A,D,Sa), ifthenelse(Sa = true, (solve(B,D,Sb), S = Sb), S = Sa). % (Sa = true -> solve(B,D,Sb), S = Sb; S = Sa). solve(A,D,Sa) :- ifthenelse(system(A),(A, Sa = true), % system(A) -> A, Sa = true; ( D1 is D - 1, clause(A,B), solve(B,D1,Sb), (Sb = true -> Sa = true; Sb = (overflow,S) -> Sa = (overflow,[(A :- B)|S]) ). */