% Meta interpreter for Prolog: prove(A) beweisbar falls "?- A." beweisbar

prove(true) :- !. % body of facts
prove( (A,B) ) :- !,
        prove(A), % prove first conjunct
        prove(B). % prove second conjunct
prove(L) :-
        clause(L,B), % find appropriate clause for L
        prove(B).

% Example program:
p(a).
p(b).

q(b).

% Meta interpreter with tracing:

tprove(true) :- !. % body of facts
tprove( (A,B) ) :- !,
        tprove(A), % prove first conjunct
        tprove(B). % prove second conjunct
tprove(L) :-
        callfail(L),
        clause(L,B), % find appropriate clause for L
        tprove(B),
        exitredo(L).

callfail(L) :- write('Call: '), write(L), nl.
callfail(L) :- write('Fail: '), write(L), nl, fail.

exitredo(L) :- write('Exit: '), write(L), nl.
exitredo(L) :- write('Redo: '), write(L), nl, fail.


