% prove(G) is satisfied if "?- G." is provable

prove(true) :- !.    % true is the body of facts
prove( (G1, G2) ) :- !, prove(G1), prove(G2). % both parts must be provable
prove(L) :-
        clause(L,G), % search for unifiable rule
        prove(G).    % proof the body

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

% meta-interpreter with computation of resolution steps / length of proofs
% lprove(G,N) is satisfied if G provoiable with N resolution steps

lprove(true,0) :- !.    % true is the body of facts
lprove( (G1, G2), N) :- !,
        lprove(G1,N1),
        lprove(G2,N2),
        N is N1 + N2.
lprove(L,N) :-
        clause(L,G), % search for unifiable rule
        lprove(G,M), % proof the body
        N is M+1.