Computation in Predicate Logic

Prolog is a programming language based on predicate logic.

• A Prolog program attempts to prove a goal, such as brother(Barney,x), from a set of facts and rules.

• In the process of proving the goal to be true, using substitution and the other rules of inference, Prolog substitutes values for the variables in the goal, thereby "computing" an answer.

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

• Prolog uses unification to determine when two clauses can be made equivalent by a substitution of variables.

• The unification procedure is used to instantiate the variables in a goal clause based on the facts and rules in the database.

Horn Clauses

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

• Statements are constructed from terms.

• Each statement (clause) has (at most) one term on the left hand side of an implication symbol ( :- ).

• Each statement has a conjunction of zero or more terms on the right hand side.

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

• A fact is a clause with an empty right hand side.

• A question (or goal) is a clause with an empty left hand side.

• A rule is a clause with terms on both sides.

Terms

There are three kinds of terms in Prolog:

• A constant is an atom or a number. An atom is a quoted character string or a string of letters, digits, and underscores that starts with a lower-case letter. A number resembles the real or integer constants used in most programming languages.

• A variable is a string of letters, digits, and underscores that starts with an upper-case letter. There are no type declarations; types are discovered implicitly by the interpreter.

• A structure represents an atomic proposition of predicate calculus, and has the form "atom(parameter list)".

Facts and Rules

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

• Facts are axioms; relations between terms that are assumed to be true.

• Rules are theorems that allow new inferences to be made.

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

• The implication is from right to left!

• The scope of a variable is the clause in which it appears.

• Variables whose first appearance is on the left hand side of the clause have implicit universal quantifiers.

• Variables whose first appearance is on the right hand side of the clause have implicit existential quantifiers.

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