Page 3 of 4
Normal form and reductio ad absurdum
The difficult of using resolution is solved almost immediately by a theorem in logic which says that any statement in Boolean logic can be reduced to a form like:
(A OR B) AND (NOT C OR D) AND (E OR NOT F OR G)
This is called conjunctive normal form and there is a simple algorithm that will convert any statement to it. If you have a premise like:
(A OR B) AND (NOT C OR D) AND (E OR NOT F OR G)
then for this to be true as a whole each of the substatements in brackets also have to be true on their own (because they are connected by ANDs).
As this is true you can split the premise up and write:
1. (A OR B) 2. (NOT C OR D) 3. (E OR NOT F OR G)
and these are clearly in the form that we need to be able to apply resolution.
A list of premises that consist of individual statements each only involving OR and NOT is often referred to as being in clause form.
We can speed up the entire process of searching for a solution simply by adopting a slightly different goal for our proof.
The method that results is called reductio ad absurdum.
If the statement that you are trying to prove, P say, is true then adding its negation, that is NOT P, to the premises then will eventually result in the resolution method producing a null statement.
The reason is simply that if P is true then it will eventually be produced by resolving statements together. This results in both P and NOT P being available for resolution so producing the null statement.
The Final Strategy
Now at last we have a workable and simple method that allows a computer to prove things using logic. All the machine has to do is:
 Convert all of the statements that are known to be true, i.e. the premises,a into clause form.
 Negate the statement P that you want to prove (i.e. write NOT in front of it), convert it into clause form and add the result to the premise
 Use resolution to derive new truths until the null clause is produced so proving that P was indeed true.
Of course it may be that P was false in which case the program as described would loop forever.
Fortunately there are ways of modifying the program so that it knows that it has tried all possibilities and stops.
Notice that in either case the you can only prove that P is true or false relative to the premises that you started with.
More importantly if the program says that P is false all this really tells you is that it cannot be proved using the information given. It may still be true but you need more starting information to prove that it is so.
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 rewrite 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.
<ASIN:0136042597>
<ASIN:1840468416>
<ASIN:1558604677>
<ASIN:0763773379>
<ASIN:0136070477>
