Prolog is a programming language based on predicate logic.
How does Prolog know which facts and which rules to use in the proof?
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.
There are three kinds of terms in Prolog:
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.
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.
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