Mathematicians are redundant

Armed a program that proves theorems by resolution, an easy one to write, I can at last put the entire mathematical profession out of a job!

All I have to do is translate the basic theorems of mathematics into clause form, enter a likely candidate for a new theorem and wait for my program to win me the Fields medal (the mathematician's equivalent of the Nobel prize).

The flaw in this plan is that you cannot translate mathematics into Boolean logic - it is far to restrictive. It does capture some of the elements of human reasoning but it misses more than it hits. For example, you can make a statement such as:

John is a father -> John is male

but how can you write something that captures that fact that anyone who is a father is also male?

The answer is to be found in first order predicate calculus which does have enough power to deal with mathematics.

This is an extension of simple propositional calculus to include variables and logical functions i.e. functions that are either true or false.

In the jargon predicates are logical functions hence the term 'predicate calculus'.  To represent the idea 'fathers are male' as a fact in predicate calculus you would write something like:

X is father -> X is male

In this case the statement is true for all possible values of X. In the jargon X is 'universally quantified'. This is often indicated by writing an upside down A in front of the statement (due to typographical difficulties the A will be used right side up in this article!)

For example,

A X   X is father -> X is male

would be read "For all X, X is a father implies X is male".

The only alternative to the universal quantifier A, is E, the existential quantifier (I warned earlier you that the jargon was fun!)

This is used in the same way as A but it is read "There exists". (Once again the usual convention is to write E mirror reversed but again due to typography we will use a standard E.)

For example:

AX EY  X is person -> Y is father of X

would be read "For all X there exists a Y such that X is a person implies that Y is the father of X.

Once you get the hang of A and E it is easy to write all sorts of complicated things.

However in practice the quantifiers prove to be a problem so these days a different method based on functions is used to indicate that something applies only to a specific X, Y or Z.

For example, you can just as well write:

AX  X is a person -> F(X)

where F(X) a function that returns the name of the father of X.

That is F(X) is the Y that is mentioned in the first version of the statement. It turns out that it is possible to re-write any statement so that an E is unnecessary simply by introducing functions that provide the particular object needed.

This process is referred to as Skolemisation and the functions are called Skolem functions but it seems almost commonsense in spite of the fancy titles.

As this is possible we might as well adopt the convention that all variables are universally quantified as a default because any that aren't would occur as functions. 

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:

father_of(tom,dick)     

    means Dick is Tom's father

father_of(dick,harry)    

   means Harry is Dick's father

and so on. You could then add a clause like

grand_father(X,Y) :- 
      father_of(X,Z),father_of(Z,Y)

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! (But it is probably only a matter of time.)

However mathematicians are using theorem provers as assistants at they work and there is a general feeling that this is the way mathematics is going. In the future math will be a joint human machine endeavor.

There is also the view that AI doesn't need logic anymore. The reason is that biologically inspired artificial neural networks are so successful that there doesn't seem room for any other approach. If you are about to go into AI research neural networks are where the action is not logic. This is a slightly distorted picture because logic captures a much higher level of human intelligence. You can think of it as the high level expression of all those neuronal calculations. What this means is that there are some areas, such as planning and reasoning, where logical methods are more direct. Don't give up on automated logic just yet.

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. To cover these areas new forms of logic are being developed.

Database The Prolog Way      

Fuzzy Logic And Uncertainty In AI       

Picat 1.0 - Is Logic Programming Making A Comeback?       

The Triumph Of Deep Learning

The Paradox of Artificial Intelligence

<ASIN:0136070477>

<ASIN:0446678759>

<ASIN:026201243X>

<ASIN:1432749366>

<ASIN:0135717795>

<ASIN:0321545893>

<ASIN:0136042597>

<ASIN:048624864X>