% 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).

:- dynamic app/3.
app([]    ,Ys,Ys).
app([X|Xs],Ys,[X|Zs]) :- app(Xs,Ys,Zs).

% Meta interpreter for Prolog with computation of number of resolution steps.
lprove(true,0) :- !. % body of facts
lprove( (A,B), N) :- !,
        lprove(A,NA), % prove first conjunct
        lprove(B,NB), % prove second conjunct
        N is NA + NB.
lprove(L, N) :-
        clause(L,B), % find appropriate clause for L
        lprove(B,NB),
        N is NB + 1.

