% Oliver Kutter kutter@in.tum.de 08/12/02 % Ein bisschen Arithmetik mit natuerlichen Zahlen % - Addition % - Multiplikation % - Subtraktion % - kleiner, groesser, gleich , ungleich % - groesserals, kleinerals, Exponentialfunktion % - Fakultaet und Fibonacci % - Summe ueber alle k mit k = 0..n % Addition fuer natuerliche Zahlen % a - neutrales Element -> 0 % f(a) -> 1 = a + 1 % fuer alle X gilt a + X = X addN(a,X,X). % fuer alle X,Y,Z gilt X +1 + Y = Z +1 -> X + Y = Z addN(f(X),Y,f(Z)):-addN(X,Y,Z). % Multiplikation fuer natuerliche Zahlen % a = 0 -> a X = a multN(a,X,a). % fuer alle X,Y,z gilt % (X+1)Y = Z -> XY = W mit W + Y = Z multN(f(X),Y,Z):-multN(X,Y,W),addN(W,Y,Z). teilt(X,Y,Z):-multN(Y,Z,X). % Subtraktion % fuer alle X,Y,Z gilt X - Y = Z -> Y+Z = X subN(X,Y,Z):-addN(Y,Z,X). % fuer alle X gilt a < X+1 kleiner(a,f(X)). % fuer alle X,Y gilt X+1 < Y+1 -> X < Y kleiner(f(X),f(Y)):-kleiner(X,Y). % groesserals groesser(X,Y):-not(kleiner(X,Y)). % Gleichheit gleich(X,X). % Ungleichheit ungleich(X,Y):-not(gleich(X,Y)). % Groessergleich : fuer alle X,Y gilt X >= Y -> gleich(X,Y) oder groesser(X,Y) groessergleich(X,Y):-gleich(X,Y);groesser(X,Y). % Kleinergleich : fuer alle X,Y gilt X <= Y -> gleich (X,Y) oder kleiner(X,Y) kleinergleich(X,Y):-gleich(X,Y);kleiner(X,Y). % Exponentialfunktion n^m fuer n > 0 % Rekursionsanfang % fuer alle N, n > 0 gilt (N+1)^a -> f(a) = 1 exp(f(N),a,f(a)). % fuer alle N,X gilt N^(M+1) = X -> N^M =Y mit Y * N = X exp(N,f(M),X):-exp(N,M,Y),multN(Y,N,X). % Fakultaet n >= 0 % Rekursionsanfang % Fakueltaet von 0 ist 1 fac(a,f(a)). % fuer alle X,N gilt fac(N+1,X) = fac(N,Y) mit Y * (N+1) = X fac(f(N),X):-fac(N,Y),multN(Y,f(N),X). % Fibonacci von n mit n >= 0 % % Rekursionsanfang fib(0) = 0 fib(1) = 1 fib(a,a). fib(f(a),f(a)). % fuer alle N gilt fib(N+2) = fib(N+1) + fib(N) fib(f(f(N)),X):-fib(f(N),Y),fib(N,Z),addN(Y,Z,X). % Summe ueber k mit k = 0..n % Rekursionsanfang summe(a,a). % Summenbildung % Summe von 0 bis f(N) = X % impliziert Summe von 0 bis N = Y mit Y + f(N) = X summe(f(N),X):-summe(N,Y),addN(Y,f(N),X).