How to prove it

The trouble with meeting Boolean logic in connection with computers is that there is a tendency to overlook its role in proof or logical reasoning.

Boolean logic provides the basic framework for examining how truth values combine in compound statements but it doesn't provide a strategy for proving one thing from another.

For example, the modus ponens law includes the word 'implies' and before we can consider proof in Boolean algebra we have to find a translation of implies in terms of AND, OR and NOT.

It is customary to use the notation A->B for A implies B and we can draw up a truth table for the compound statement A->B 

Notice that this table might not be quite what you are expecting of 'implies'.

The key to understanding it is to notice that A->B only says that B is true if A is true. If A is false then A->B says nothing about the truth of B. By studying the truth table you might discover that

A -> B = NOT A OR B

This simple relationship is the key to most of the recent advances in AI and basis of the language Prolog. What it allows us to do is automate the modus ponens and the chain rule and so add logical reasoning to the dimmest of computers.

Automated Reasoning

Before looking at how we can automate logical reasoning it is worth proving something using traditional methods.

For example, if you have the premises

1. (A AND B) -> ((C OR D) -> (E AND F))
2. (E AND F) -> (NOT F OR G)
3. A AND B

then to prove

(C AND D) -> NOT F OR G

you would have to use modus ponens on 1 and 3 to give

4. (C AND D) -> (E AND F)

using the chain rule on 2 and 4 gives

5. (C AND D) -> (NOT F OR G)

which completes the proof. 

This seems easy enough but how can a computer be made to produce the same proof?

How was it determined that the modus ponens rule should be used and then the chain rule?

Like nearly all proofs this one covers up the trial and error and sometimes slightly inspired route that the human took to arrive at the answer.

This is not a method that we can program on a computer.

Resolution

The first observation that helps to  automate logical reasoning is that both modus ponens and the chain rule can be written in a single and very regular form.

If each implication in the chain rule:

(A->B) AND (B->C) DEDUCE (A->C)

is written in the form NOT A OR B we get:

FROM      NOT A OR B
AND       NOT B OR C
DEDUCE    NOT A OR C

and this is can be thought of as 'cancelling' the terms B and NOT B in the first two expressions to produce the third.

This includes modus ponens because if we set A to the trivial proposition TRUE we get:

FROM   NOT TRUE OR B     =     B
AND    NOT B OR C        =     B->C
DEDUCE NOT TRUE OR C     =     C

What all this tells us is that as long as all the statements in the premises are similar to:

A OR NOT B OR C OR NOT D

i.e. statements that use only ORs and NOTs, then there is a very simple and mechanical method of looking at a set of premises and deriving new truths.

All you have to do is:

1. Scan the premises for two compound statements one containing a X and the other containing NOT X
2. Join the two statements together but leave out any mention of X or NOT X

This is called inference by resolution.

For example, if the premises are:

1. A OR NOT B
2. C OR NOT A
3. A OR B OR NOT C OR D

then we can easily make new true statements by combining or resolving 1. with 2. so eliminating A and giving:

4. C OR NOT B

Then 4 could be resolved with 3 eliminating both B and C giving:

5. A OR D

and so on.

You could easily program this search and combine method and as long as the original premises were true you would carry on generating new truths to add to the set of known truths. 

Eventually it would add to the original premises every single statement that could be proved using them as the starting point. If you want to prove something simply set the computer running until the statement that you want to prove turns up - well not quite because there are two problems.

The first is that not all Boolean statements are made up of nothing but ORs and NOTs and secondly  you could be searching a long time to find the statement that you are looking for.

Both of these problems have very easy solutions.

Normal form and reductio ad absurdum

The first difficulty in 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)

i.e. a set of subclauses joined together with AND. Each subclause is the OR of variables or their negation. 

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 sub-statements 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 also 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:

1. Convert all of the statements that are known to be true, i.e. the premises,a into clause form.
2. 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
3. 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.

<ASIN:0136042597>

<ASIN:1840468416>

<ASIN:1558604677>

<ASIN:0763773379>

<ASIN:0136070477>

<ASIN:0262062712>