The Greeks, George Boole and Prolog
Written by Mike James   
Thursday, 22 April 2010
Article Index
The Greeks, George Boole and Prolog
Proof and automated reasoning
Normal form
Prolog

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

 

A

B A ->B
F F T
F T T
T F F
T T T
 

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.

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.

<ASIN:0262062712>

<ASIN:0135717795>

<ASIN:0321545893>

<ASIN:0136042597>

<ASIN:048624864X>



Last Updated ( Wednesday, 21 April 2010 )
 
 

   
RSS feed of all content
I Programmer - full contents
Copyright © 2014 i-programmer.info. All Rights Reserved.
Joomla! is Free Software released under the GNU/GPL License.