Gödel Tutorial


MODULE    Fibonacci.

IMPORT    Integers.


PREDICATE Fib : Integer * Integer.

% Fib(k,n) <-> n is the Fibonacci number F_{k} of rank k.

Fib(0,0).
Fib(1,1).
Fib(k,n) <-
          k > 1 &
          FibIt(k-2,1,1,n).


PREDICATE FibIt : Integer * Integer * Integer * Integer.

% FibIt(k,f,g,n) <-> n  =  F_{k} * f  +  F_{k+1} * g.

FibIt(0,_,g,g).
FibIt(k,f,g,n) <-
          k > 0 &
          g < n &
          FibIt(k-1,g,f+g,n).

  GCD Function 
MODULE      GCD.

IMPORT      Integers.

PREDICATE   Gcd : Integer * Integer * Integer.

Gcd(i,j,d) <-
            CommonDivisor(i,j,d) &
            ~ SOME [e] (CommonDivisor(i,j,e) & e > d).

PREDICATE   CommonDivisor : Integer * Integer * Integer.

CommonDivisor(i,j,d) <-
            IF (i = 0 \/ j = 0)
            THEN
              d = Max(Abs(i),Abs(j))
            ELSE
              1 =< d =< Min(Abs(i),Abs(j)) &
              i Mod d = 0 &
              j Mod d = 0.

Database
  Family Tree 
MODULE        DB.

BASE          Person.

CONSTANT      Fred, Mary, George, James, Jane, Sue : Person.

PREDICATE     Ancestor, Parent, Mother, Father : Person * Person.

Ancestor(x,y) <-
              Parent(x,y).
Ancestor(x,y) <-
              Parent(x,z) &
              Ancestor(z,y).

Parent(x,y) <-
              Mother(x,y).
Parent(x,y) <-
              Father(x,y).

Father(Fred, Mary).
Father(George, James).

Mother(Sue, Mary).
Mother(Jane, Sue).

  Sports Database 
MODULE      Sports.

IMPORT      Sets.

BASE        Person, Sport, PersonSports.

CONSTANT    Mary, Bill, Joe, Fred : Person;
            Cricket, Football, Tennis : Sport.

FUNCTION    Pair : Person * Set(Sport) -> PersonSports.

PREDICATE   Likes : Person * Sport.

Likes(Mary, Cricket).
Likes(Mary, Tennis).
Likes(Bill, Cricket).
Likes(Bill, Tennis).
Likes(Joe, Tennis).
Likes(Joe, Football).

List/Set Processing
MODULE     SetProcessing.

IMPORT     Sets.

PREDICATE  Sum : Set(Integer) * Integer.

Sum(s,y) <-
        x In s &
        Sum1(s\{x},x,y).

PREDICATE  Sum1 : Set(Integer) * Integer * Integer.

Sum1({},x,x).
Sum1(s,x,x+w) <-
        z In s &
        Sum1(s\{z},z,w).

PREDICATE  Max : Set(Integer) * Integer.

Max(s,y) <-
        x In s &
        Max1(s\{x},x,y).

PREDICATE  Max1 : Set(Integer) * Integer * Integer.

Max1({},x,x).
Max1(s,x,y) <-
        z In s &
        IF z>x THEN Max1(s\{z},z,y) ELSE Max1(s\{z},x,y).