Computation in Predicate Logic

Prolog is a programming language based on predicate logic.

How does Prolog know which facts and which rules to use in the proof?


Horn Clauses

To simplify the resolution process in Prolog, statements must be expressed in a simplified form, called Horn clauses.

Prolog has three kinds of statements, corresponding to the structure of the Horn clause used.


Terms

There are three kinds of terms in Prolog:


Facts and Rules

The Prolog environment maintains a set of facts and rules in its database.

Example facts:

      male(adam).
      female(anne).
      parent(adam,barney).
  

Example rules:

      son(X,Y) :- parent(Y,X) , male(X)
      daughter(X,Y) :- parent(Y,X) , female(X)
  

The first rule is read as follows: for all X and Y, X is the son of Y if there exists X and Y such that Y is the parent of X and X is male.

The second rule is read as follows: for all X and Y, X is the daughter of Y if there exists X and Y such that Y is the parent of X and X is female.


Observations about Prolog Rules


Executing a Prolog Program

To run a Prolog program the user must ask a question (goal) by stating a theorem (asserting a predicate) which the Prolog interpreter tries to prove.

If the predicate contains variables, the interpreter prints the values of the variables used to make the predicate true.

The interpreter uses backward chaining to prove a goal. It begins with the thing it is trying to prove, and works backwards looking for things that would imply it, until it gets to facts.


Example: Greatest Common Divisor

Using Euclid's algorithm, we can compute the GCD of two positive integers in Prolog as follows:

  /* Prolog program to compute GCD */
  | gcd(A, 0, A).
  | gcd(A, B, D) :- (A>B),(B>0),R is A mod B,gcd(B,R,D).
  | gcd(A, B, D) :- (A<B), gcd(B,A,D).
  

The first rule is the base case to terminate the recursive definition.

The second rule ensures that the first argument is the larger of the two and that the second argument is a positive integer, computes the remainder of A/B into R, and recursively matches (finds) the gcd of the smaller argument and R.

The third rule reorders the arguments so the larger argument is first.

Prolog attempts to match the rules in order, and clauses are evaluated left to right. If any clause fails (ie, if A is not greater than B in rule 2), then the rule fails.

Here is the sequence of steps the Prolog proof system would go through given A=5 and B=10:

      ?-gcd(5,10,D)
      (5>10)
      gcd(10,5,D)
      (10>5)
      (5>0)
      R=0
      gcd(5,0,D)
      D=5