The following is a simple meta-interpreter, as seen in many guides/textbooks.
prove(true) :- !.
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- clause(H,B), prove(B),
write(H), write(" <- "), writeln(B).
The following is a simple program to test the meta-interpreter with.
% parent facts
parent(john, jane).
parent(john, james).
parent(sally, jane).
parent(martha, sally).
parent(deirdre, martha).
% ancestor recursive definition
ancestor(X,Y) :- parent(X,Y), !.
ancestor(X,Y) :- parent(X,A), ancestor(A,Y).
The meta-interpreter works for programs that are simple facts. It also works for simple deduction. However it fails when the program uses a cut.
?- prove(ancestor(martha, jane)).
parent(martha,sally) <- true
parent(sally,jane) <- true
No permission to access private_procedure `!/0'
In:
[6] clause(!,_692)
[5] prove(!) at line 20
[3] prove(ancestor(sally,jane)) at line 20
[1] prove(ancestor(martha,jane)) at line 20
Question: Is there a simple way to handle cuts in the programs that the meta-interpreter is trying to run?
I know how to extend the meta-interpreter to handle additional syntax, eg the following adds the ability handle \+
thanks to the answer here: negation \+ and vanilla meta-interpreter
prove(true) :- !.
prove((A,B)):- !, prove(A), prove(B).
prove(\+ A) :- !, \+ prove(A). %%% handling \+
prove(H) :- clause(H,B), prove(B),
write(H), write(" <- "), writeln(B).