:- dynamic append/3, loop/0, quickSort/2, quickSort_dl/3, splitLGE/4. % zum Testen append([],Ys,Ys). append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs). loop. loop :- loop. quickSort(L,S) :- quickSort_dl(L,S,[]). quickSort_dl([],L,L). quickSort_dl([E|R],M,N) :- splitLGE(E,R,L,GE), quickSort_dl(L,M,[E|GESorted]), quickSort_dl(GE,GESorted,N). splitLGE(_,[],[],[]). splitLGE(X,[Y|Ys],[Y|L],GE) :- Y < X, splitLGE(X,Ys,L,GE). splitLGE(X,[Y|Ys],L,[Y|GE]) :- Y >= X, splitLGE(X,Ys,L,GE). % einfacher Interpreter prove(true) :- !. prove((A,B)) :- !, prove(A), prove(B). prove(A) :- clause(A,R), prove(R). % beschränkter Interpreter bounded(G,N) :- bounded(G,N,_). bounded(G,N,K) :- N >= 0, bprove(G,N,K). bprove(true,_,0) :- !. bprove((A,B),N,K) :- !, bounded(A,N,K1), N2 is N - K1, bounded(B,N2,K2), K is K1 + K2. bprove(A,N,K1) :- N1 is N-1, clause(A,R), bounded(R,N1,K), K1 is K + 1. % Beweis berechnen proof(G,P) :- proof(G,P,[]). proof(true,P,P) :- !. proof((A,B),P,R) :- !, proof(A,P,Q), proof(B,Q,R). % für quickSort proof(<(X,Y),[<(X,Y)|P],P) :- !, X < Y. proof(>=(X,Y),[>=(X,Y)|P],P) :- !, X >= Y. proof(A,[:-(A,G)|P],Q) :- clause(A,G), proof(G,P,Q). printProof(G) :- proof(G,P), printClauses(P). printClauses([]). printClauses([:-(A,true)|Cs]) :- !, write(A), write('.'), nl, printClauses(Cs). printClauses([:-(A,B)|Cs]) :- !, write(A), tab(1), write(':-'), tab(1), write(B), write('.'), nl, printClauses(Cs). printClauses([A|Cs]) :- write(A), write('.'), nl, printClauses(Cs).