Page 4 of 4
Unification and Prolog
Given predicate calculus you really can oust the mathematicians and install a computer instead. Apart that is from the small problem that our theorem proving by resolution has no way of dealing with variables and functions in statements.
Fortunately there is a simple generalisation of the resolution method that does apply to predicate calculus which was invented by Alan Robinson in the 1960's and which ultimately gave rise to the language Prolog.
The changes are:
- all statements have to be converted to 'Horn clauses' which are clauses with at most one NOT.
- variables in clauses have to be assigned values in an attempt to find pairs that can be resolved together. This assigning of values is called the Unification algorithm.
Although unification sounds complicated it is just a matter of trying to make two clauses look similar by setting variables to the same values.
For example, the following statements:
1. NOT(X is a person) OR
F(X) is father of X
(i.e. X is a person -> F(X)
is father of X)
2. NOT(Y is father of X) OR
X is child of Y
(i.e. Y is father of X -> X
is child of Y)
could be unified by setting Y to F(X) and then resolving the two clauses to give:
3. NOT(X is a person) OR
X is a child of F(X)
or X is a person -> X
is child of F(X)
which is of course a reasonable deduction.
We can still use the trick of adding the negation of the clause that we are trying to prove to the premises and trying to derive the null clause and so proof in predicate calculus can also be automated.
The link between all of this and Prolog is that the language is based on predicate calculus and it uses unification and resolution to prove whatever goals you set it.
The only real difference between what we have been looking at so far and Prolog is a matter of notation. Prolog uses :- for ->, a comma for AND and a semi-colon for OR. The clauses also have to be written in the form of predicates or logical functions.
For example, the clause:
Y is father of X -> X is child of Y
would be written in Prolog as:
father_of(X,Y) :- child_of(Y,X)
where father_of(X,Y) is a function that is either true or false depending on the values of X and Y. Using predicates also avoids the having to use Skolem functions. For example, the idea contained in:
X is a person -> F(X) is father of X
would be translated into Prolog as a listing of values of X and Y for which the predicate father_of(X,Y) was true:
means Dick is Tom's father
means Harry is Dick's father
and so on. You could then add a clause like
which says that the grandfather of X is Y if the father of X is Z and the father of Z is Y.
Prolog will automatically scan the list of father_of clauses to find a suitable value of Z for any values that are given to X and Y and if none can be found then the predicate grand_father(X,Y) isn't true for the current values of X and Y.
The current state of thought
If by this point you are feeling a little boggled by predicates, unification, resolution and so on, then it is worth saying that many users of Prolog never manage to understand its relationship to logic.
This is a shame because after all Prolog does stand for PROgramming in LOGic. Prolog is one just one example of a theorem prover. There are others and some of them are better at the task. However Prolog is a good compromise between power and efficiency but don't be surprised if the language develops to include more powerful features of logic.
Currently theorem provers have successfully proved theorems in mathematics that beforehand were unsolved problems. None of these have been earth shattering and so far no computer has been awarded the Fields medal!
The range of problems that can be tackled using predicate calculus is amazing but it still doesn't really capture the nature of human thought. You can look at this either as a reflection of the fact that human thought is sloppier than logic or that it is more sophisticated than logic. I suppose it all depends on whether you think computers are better than humans.