Doing Arithmetic with Diagrams

1. INTRODUCTI ON .

This is a report of work in progress . I t de scr i bes what is , t o the best of the author 's knowledge , a new kind of automatic theorem prover , called SUMS (a 2Ys tem which Qnderstands ~athematical 2Ymbo l s) · SUMS does not explicitly use axioms or r ules of inference to prove theorems . Instead it r epr esents the candidate t heorem as a network (or diagram) in which t he nodes ar e t he property lists of ar ithmetic terms and the links describe relationships (e . g . ~ . ~. J) between t hem. Statements are asserted by adding new links and proved by accessing the diagr am. Knowledge about arithmetic is built into the procedures that draw the diagram so that when links ar e added to it , el ementar y deduc t ions are made (and more links added) automat­ ically.

The domain of SUMS is the Elementary Theory of Natural Number s ( i . e . the arithmetic of the non- negative integer s) . At pr esent it can only handle the cl asses of terms and formulae defined below:

• (a) An arbitrary skolem constant or natural number is a term.
• (b) If A and B are terms then Suc(A) ; Pre(A) ; A + B ; A .: B and A x B are terms .

by

Alan Bundy

Department of Computational Logic , University of Edinburgh , Edinburgh , Scotland.

(c) If A and B are terms then A = B; A ~ B; A ~ B ; A > B ; A ? B ; A < B ; A J B and A /. B are atomic formulae . (Note t hat for each predicate symbol , S , there i s a symbol $ su· ·l that ., S(x 1 , ··· , xn) -4-+ $(x 1 , ··· , xn) . )

• ( d) An atomi c fo rmul a is a formul a .
• (e) If P and Q ar e formulae t hen , P ; P & Q; P v Q; p - Q and P ~ Q are formulae , ~here Sue and Pre are the successor and pr edecessor
• funct ions .

• and .: , the modified difference function , is j us t ordinary subtract ion modified so that its result is al ways a natural number

Before describing t he representat i on of the diagram and the procedures which dr aw it , it is best to illustrate how the theorem prover works with some examples .

( i ) The Associative Law of Addition.

SUMS always starts by constructing nodes for 0 and 1 and dr awing the appropri ate l inks between them ( e . g . 0 ~ 1, 0 ~ 1, 1 Jo, etc . ) New nodes are always appropri atel y r el ated to 0 and 1. However , since these links play no part in the proof which follows they have been omitt ed for clarity.

The machine then creates nodes for each of the subterms involved in (1) and draws in the appropriate links .

Fig. 1.

The links in the tion l inks , e . g . 'a + (b + c) '. is compar ed with can be drawn . above diagram ar e distance and dir ec­ 'a ' is a distance 'b + c ' less than When a new link i s added to a node it t he old links t o see if any conclusion For instance in Fig. 2 the link from 'a ' to 'a + b' is compared with the link from 'a ' to 'a + ( b + c) ' , which causes the distance l abel 'b' to be compared to the distance label 'b + c'. The node 'b' is found to be a distance 'c ' less than the node 'b + c ' in the diagr am; so SUMS deduces that 'a+ b' must be a distance 'c ' less than 'a+ (b + c) ', and draws in the appropriate link (dotted) ·

Finally the node for ·(a +b) + c ' is created but as the first link is being drawn (dotted in Fig . 3) it is compared with the link connecting ' a~ b ' to 'a+ (b + c) ' and found to be of equal length.

SUMS deduces that a + (b + c) = (a + b) + c and achieves this by merging the two nodes and not adding the new link (Fig . 4) .

SUMS now proves the theorem by accessing the diagram and discovering that these two terms have the same node .

(ii) Commutativity of Maximum.

If we define max(x ,y) as x + (y · x), (2) becomes the commutative law of maximum.

As before SUMS creates nodes for each of the subterms involved in (2) , except that this time it considers two cases . SUMS always draws terms of the form A .:. B by first interrogating the diagr am to see if either of the cases A~ B or B ~A hold . Otherwise it dupli­ cates the diagram, asserts A ~ B in one and B < A in the other and then tries to prove the theorem i n both cases .

So in this example the final diagrams are :

Case a~ b

means that A ~ B. These links are not needed in this example but are inc l uded for completeness . They occur because asserting B < A involves asserting both B ~ ~ and B ~A .

3 . THE REPRESENTATION OF THE DIAGRAM.

The diagrams are represented using lists and POP- 2 records . We find records convenient , but they coul d, if necessary , be replaced by lists or arrays .

E~ch diagram is a record with 6 components (or slots) in which information is recorded . These slots are called and contain:

• (a) Title : a formula in list notation which says which case the diagram represents , e . g . [LESS A B) .
• (b) Contra: a 1 or 0 according as the diagr am has or has not been found contradictory.
• (c) Net work : a list of the entr ies (defined below) in the diagram.
• (d) Nought and Unity: 2 redundant slots pointing to the, frequently used , entries for 0 and 1 respectively.
• (e) File : a list of terms which were not represented in t he diagram when wanted, but which SUMS may decide to represent l ater .

Every term is represented, in the diagram, by a unique record with 3 s l ots , called an entry. These slots are called and contain:

• (a) Label : The name of the term being represented in lis t n~on, e . g . [ADD A [DIFF B A) )
• (b) Proplist : A record of type 'node ' which contains all the links to the other entries . When two terms are made equal all the information from the firs t term's 'proplist ' (property list) is put into the second term's 'proplist ', which then replaces the first wherever it appears . Thus equal terms share 'proplists ' which justifies the adoption of the name 'nodes ' for the 'proplist ' rather than the entries . This method of dealing with equality is mor e convenient than using equal ity links, because : it makes checking for equality mor e efficient (the 'proplists ' must be EQ); the equality axioms are automatically incorporated , and all the information about a s i ngle node is kept in one place .
• (c) Replace : A slot used in the copying of diagrams .

STRUCTURE OF DIAGRAM

Each node is a r ecord with 6 slots called and cont ­ aining:

• (a) Smaller: A list of pairs of entries . The front of each pair represents a term smaller than the present one ; the back represents the distance between them.
• (b) Bigger: Similar to (a) except that the front of each pair is the ent ry of a term bigger than the present one .
• (c) Unequal : A list of entries representing terms known to be unequa l to the present one .
• (d) Factor: Similar to (a) except that the front of each pair is the entry of a term which exactly divides the present one , and the back is the entry representing the quotient produced .
• (e) Multiple: Similar to (d) except that the front of each pair is the entry of a term which the present term exactly divides .
• (f) Mark : A slot used for markers when measure­ ments are being made in the diagram.

4. THE PROGRAM.

In order to distinguish functions in SUMS from functions in Arithmetic , we will call the former procedures .

There are four classes of top level procedures arranged roughly in a hierarchy. They are :

• (a) Logical Procedures : which analyse the origina l formula and decide which atomic formul ae to assert and which to prove .
• (b) Drawing Procedures : which analyse the terms in the formulae , draw them in the diagram and assert relationships between them.
• (c) Asserting Procedures : which make relationships between terms hold in the diagram by adding links .
• (d) Interrogating Procedures: which discover whether relat ionships between terms hold by accessing the diagr am.

(i) The Logical Procedures .

After the initial diagram has been created all negations are eliminated from the candidate theorem by passing them down to , and absorbing them into , the atomic formulae . i . e. each negated atomic formula , s(x1, ··· xn) is replaced by ~(x1 , ... , xn) . The candidate , P, is then passed to the procedure 'Prove ' whose description follows .

To prove l':

• (a) If P is a conjunction of atomic formulae , its terms are drawn in the diagram, which is then interro­ gated to see if P is true .
• (b) If P is of the form Q & R then a copy of the diagram is made , Q is proved in the first diagram and R in the second .
• (c) If P is of the form Q v R (or Q- R) then we assert , Q ( Q) in the diagram and prove R.
• (d) If P is of the form Q- R then a copy of the diagram is made . In the firs t diagram, Q is asserted and R is proved ; in the second R is asserted and Q

proved .

To assert a formula in the diagram the following procedure is called .

To assert P :

• (a) If P is already true in the diagram then the procedure is exited .
• ( b) If P is already false the diagram is closed , by making it contradictory , and the procedure exited .
• ( c) If P is atomic , its subterms are drawn , and it is made true in the diagram by cal ling an approp­ riate asserting procedure .
• ( d) If P is of the form Q & R then both Q and R are asserted .
• (e) If P is of the form Q v R, (Q- R) then :

If Q is false (Q is true) , R is asserted; If R is false, Q is asserted( , Q is asserted) ;

Otherwise a copy of the diagram is made and Q is asserted ( , Q is asserted) in the first diagram and R in the second .

• (f) If P is of the form Q- R then :

IfQ is true , R is asserted;

IfR is true , Q is asserted ;

IfQ is false , 1 R is asserted ;

IfR is fa l se , 1 Q is asserted ;

Otherwise a copy of the diagram is made and Q and R are asserted in the first diagram and , Q and , R are asserted in the second .

The referee has pointed out the similarity of these procedures to Beth' s Semantic Tableaux (see 2) . The main differences are that :

• (a) SUMS cannot yet handle arbitrary quantifi­ cation. Semantic Tableaux provides some valuable clues as to how to correct this defect .
• (b) in SUMS the left (valid) and right (invalid) columns of Beth 's tableaux have been combined in a single diagram, making a neater and more powerful procedure .
• ( c) At present SUMS does not assert the negation of the theorem to be proved, a practice which would certainly lead to an increase in power .
• (d) Before dividing into 2 cases SUMS checks the present diagram to see if either of the new diagrams would be contradictory (see the checks in ( e) and (f) above , and in the drawing procedure for ~ below) · This limits the number of cases to be consider ed , but i s not perfect , and unnecessary cases are sometimes considered.
• ( e) Most importantly, the assertion of an atomic formula , in SUMS , is not just the passive addi tion of the formul a to a list , but an act which may have wide repercussions within the diagram.

( ii) The Drawing Procedures .

Between them the drawing and asserting procedures are mainly responsible for drawing the diagram. Their general philosophy is to limit the number of nodes in the diagram to t hose representing terms mentioned in the candidate theorem, but to draw as many links between these nodes as possible . Thus the diagram is prevented from expl oding , since onl y a finite number of links is possibl e be tween a finite number of nodes, but quite sophi sticated r e l ationships ar e deduced between the nodes that ar e r epr esented . This kind of heuri­ stic is quite common i n mathematics for instance as advice to students proving theorems in Euclidean geometry, to deduce as much as possible about a diagram without constr ucting any further points (cf . 3) . The only exceptions to th1s rule are :

• (a) the cr eation of nodes for 0 and 1, often needed because they are the identity e l ements for addition and multiplicat ion .
• (b) the limited creation of nodes needed to l abel links between existing nodes , e . g . if a ~ b is one of the pr emises of the candida t e theorem and b ~a is not already r epresented, then we r epr esent it.
• ( c) the creat ion of new nodes as part of a proof strategy ( see Section 6) .
• (d) the suppression of those c l asses of links which do not appear to be necessary to prove the theorem, e . g . multiplicative l inks in a theorem only involving addition . This has not yet been implemented .

(a) and (b) only produce a strictly l imited number of extr a nodes.

We now turn to a desc r iption of the procedures them­ selves . 11: formula is drawn in the di agram by creating ent r ies for each of its subterms which do not already have them, from the bottom up , and then passing these entries to procedur es which ext rac t information from the term's function symbols . Ther e is one of these drawing procedures for each arithmetic function symbol , and the procedure r eceives every term beginning with this symbol . It assumes tha t the term' s ar gu­ ments have alr eadY been represented . If necessary it can use t he interrogation procedures to di scover the state of the di agram before using its knowledge of arithmetic to assert relationships with the asser ting procedures .

As an example we describe the procedure for terms of the form A .:. B:

If A ~ B then make A .:. B equal to 0 . else if B ~ A then make A .:. B l ess than or equal to A by an amount B. el se Copy the pr esent diagram. IfF is the title of the old diagram make P & A~ B the title of the old one wnd P & B < A the tit l e of the new one . In the old diagram cr eate an entry for B .:. A if one does not already exist . make A less than B by amount B .:. A make .A .:. B equal to 0 . In the new diagr am make A .:. B unequa l to 0 make A .:. B l ess than A by amount B. end .

These drawing procedures are sufficiently close to the original funct ion definitions to make one fee l optim­ istic about having t he machine ' learn ' a new function by const r ucting its drawing procedure from its definition. The cr eation of an entry for a term involves constructing a new entr y , inserting the term in its ' label ' s lot and a new node in its 'proplist ' s lot and adding this entry to the diagram's 'network' slot . The property list i s then filled with as much information as possible . For instance, all terms are made bigger than 0 and divis ible by 1. In addition if t he term i s a natural number we compute and record , subject to the normal limitations , its rel ationships to all pr evi ously created natural numbers . e . g . 2 is made bigger than 1 by an amount 1 and unequal to 0 and 1 etc . This is still non- explosive if the number of nodes is st rict ly contr ol led , and ensures that all nodes relevant in a particular situation can be conveniently recovered .

(iii) The Asserting Procedures .

There is an asser ting procedure for each predicat e symbol . These pr ocedures update the property lists of the entries in the diagram thus cr eat ing new links in the network . Befor e and aft er these links are created various 'antecedent ' pr ocedures ( cf . 4) are called , which examine the local state of the diagr am to see whether any further f acts can be deduced . In parti­ cular a contradiction may be detected in some diagram and then registered by assigning 1 to the diagr am's 'contra ' slot .

These ant ecedent procedures contain a good deal of the arithmetic knowledge which is built into the theor em prover . They are constantly evolving as new infor­ mation is included or neater ways of achieving the same effect are discovered , and so it would be mis­ leading to over- emphasise their present state by describing one in detail . However , we can give some examples of their action .

Suppose that an assert ing procedure is making A divide C with quotient B (i . e . A x B =c) . Let A, B and C be represented in the diagram by the entr ies Ae, Be and Ce r espectively , and in generai if X is a term, let Xe be the entry r epresenting it . Befor e adding any new links between Ae , Be and Ce , SUMS compares,for instance, Ce and Be with each of the pai r s , (Ee .De) , in the 'multiple ' slot of Ae . We illust r ate this situ­ ation in t he following diagram, in which the double a rrows indicate that the links are mul tiplicative.

If say B is equal to D then because :

C is made equal to E and the pr ocedure is exited .

Adding the new links involves consing the pairs

(Ae .Be) and (Be .Ae) onto the l ist cont ained in the 'factor ' slot of Ce ; ( Ce .A e) onto the list contained i i1 the 'mul t ipl e ' slot of Be and (C e .Be) onto the list contained in the 'multiple ' slot of Ae .

The redundancy of this method of link s torage i s justified by the convenience of having all the information about a particular node stored in that node .

After the links have been added , for instance , Ce and Be are again compared with each of the pairs (Ee .De) in the 'multiple ' s lot of Ae . If , say , A is known to be unequal to 0 and C exactly divides E with quotient FJthen B is made to divi deD exactly with quotient F . Because :

(A x B = C & A x D E & A ~· 0 & C x F ~ BxF= D E)

Again if, say , B is smaller than D by an amount F and there is a term, G, equal to A x F represented in the diagram then D is made less thanE by an amount C. Because :

Formulae like (3) , (4) and (5) are the mainstay of the antecedent procedures . Although apparently arbitrary, they often have a simple geometric interpretation and turn out to be surprisingly powerful in antecedent mode . In general the asserting and antecedent proc­ edures fall into the following pattern:

• ( a) Check whether the relationship already holds . If so , exit without adding any more links .
• (b) Check whether the opposite relationship already holds . If so , declare a contradiction and exit .
• ( c) Otherwise add all new links .
• (d) Now do a lot of very cheap (in time and space) checks to discover the current local state of the diagram. Deduce and assert as many new facts as possible without creating any new nodes in the diagram.

(iv) The Interrogating Procedures .

There is an interrogating procedure for each predicate symbol . They are used to settle all questions about the relationships between terms and they do this by accessing the diagram. Because they are used so f requently the present procedures are designed , for efficiency, to do very little searching. For instance , the procedure which asks whether A is equal to B returns true if and only if A and B have the same node stored in their 'proplists'. The procedure which asks whether A is less than B starts at A and climbs up through the 'bigger ' slots , marking its passage , until either it comes to B and returns true or it exhausts all possibilities and returns false . It 1~ould be possible to design procedures which tried a lot harder than this , but their use would have to be selective .

There is a subclass of the interrogating procedures , called the measuring procedures , and ther e are measuring procedurescorresponding to most of the function symbols . For instance, the measuring procedure for + takes as arguments two entries , Ae and Be , (say) representing the terms , A and B, and returns true if and only if it finds an entry for a term equal to A + B, in which case it also returns this entry. It does this by looking in the 'bigger ' slot of Ae for a pair whose back is equal to Be and returr£the corresponding front if successful . This pr ocedure may well succeed even if A + B is not represented . e . g . B + A may be represented or in a diagram where a S b , A is a and B is b ~ a we may return the entry for b. If the procedure does not succeed the term A + B is stored in the diagram's "file ' slot where it may be used at a later date as grounds for constructing a node for A + B.

5. RESULTS .

74 of the 86 theorems which have been attempted so far were drawn from 1, which contains about 700 formal theorems . The remaining 12 ·~ere invented to test SUMS 1 ability to deal with particular numbers (see numbers 14, 15 and 20 below) . SUMS can now prove 64 of them with times ranging from 0 . 125 sees, of C.P .U. time (number 13) to 45 . 94 sees, of C.P .U. time (number 12) . There follows a selection of 15 of these 64 successfully

(i) Successes .

Failures .

Most of these theorems are quite difficult to prove from the Peano axioms of arithmetic . For instance , the normal proof of number 1 involves two induction steps . Although normalization algorithms might be used to prove some of them, it is extremely difficult to see how such a method would deal with number 4 , number 7 or number 12 .

6. GOALS .

. 1 In order to pr ove the remalnlng 636 theorems ln , SUMS requires abilities outsiue its present scope . Plans for adding some of these abilities are well advanced and only await implementation ; others are further in the future . A description of these pl ar£ follows .

(i) Further Arithmetic .

I n order to tackle more sophisticated arithmet ic formulae , SUMS needs to be abl e to deal with the quotient ; remainder; exponential ; nth odd prime ; greatest common divisor ; is- a- prime and other functions and predicates . All these abilities require a drawing procedure for each new function , an asserting and an interrogating procedure for each new predicate and its negation, and new slots in the property lists. These will be added soon.

( ii) Quantific-ation .

At present SUMS is not capable of dealing with any formula that would contain existential quantifiers if it were written in Prenex normal form. Beth' s Semantic Tableaux2 and Robinson 's Resolution5 both provide valuable clues as to how to correct this deficiency . There follows a proposed solution.

Firstly, replace any call of the procedure 'To prove P', described in Section 4 , by a call of 'To assert 1 P' and then the theorem is proved when all the diagrams become contradictory. Non- contradictory diagrams will be used to suggest counter- examples or will be candi­ dates for more strenuous proof s trategies (see next sub- section) .

Secondly , update the · to assert P' procedure by adding :

(g) If P is of the form V x Q(x) t hen an entry of t ype 'variable ' is created for x . x is added to a local variable list 'vars ' and Q(x) is asserted .

(h) If P is of t he form 3 x Q( x) then an entry of type 'skolem function ' is created for x. x is made dependent on all the variables in the current value of 'var s ' and Q(x) is asserted.

Thirdly, during the course of t he proof we may 'substitute ' for a variable x , any term A, which is not dependent on x. This involves making a copy of any ent ry containing x, r eplacing each occurrence of x in each copy by the term A and making equal any terms with the same labe l . The ability to substitute needs to be handled with the same circumspection as the other proof strategies mentioned in the next sub­ section.

(iii) Proof Strategies .

With the additions mentioned above , SUMS should be able to prove a wide class of straightforwar d theorems . However , it performs no search and a lways terminates with or without a solution aft er it has represented the candidate theorem. To prove more sophisticated theorems SUMS need~ to have and to know how to use , a store of proof s trategies (PLANNER consequent theorems4) ·

For instance , it may decide to try mathematical induction, to const ruct some new terms , to make a substitution, to divide into cases , to use some previously proved theorem or to set up some inter­ mediate sub- goals . All these abilities are relatively straightforward to apply once a decision about how to use them has been made , but deciding on what to use and how is difficult . Our int ention, therefore , is to implement this stage in two parts . The first task will be to make SUMS interactive . Procedures wi l l be written to correspond to the mathematical use of such instruct ions as :· Try induction on ··· ; Consider the term ··· ; Substitute ··· for ··· ; Consider the cases ··· ; Use ··· ; First prove ··· ; etc . Then SUMS will be led through the proofs of some moderately difficult theor ems in Number Theory. The second t ask is to use this experience to evolve a language for classifying candidate theorems and selecting and applying suitable proof strategies .

Some progress has now been made on the first task . If SUMS fails to prove a theorem it asks for help i n constructing new terms and offers the contents of the diagram' s 'file ' slot as evidence . The user may then tell SUMS to construct some terms before continuing with the proof . For-instance , after representing a < b & c < d a + c < b + d (number 16 in Sec tion 5) i; the diagram, ;nd failing to prove it , SUMS asks for help and suggests the constructions : a + d ; c -t b ; ( d .: c) + b and ( b .: a) + d . If the user orders a + d or c + b to be constructed a proof is imm.edia te . If instead he chooses (d .: c) + b or (b .: a) + d, help is requested again . On the initial t rial run through the 22 previous failures (see Section 5) , 16 were proved using this method - 7 on the basis of the proffered evidence alone . Of the remaining 6 theorems 3 were abandoned and 3 produced stack overflow because the length of deductions got too deep.

7. CONCLUSION .

This theorem prover uses an anal ogical representation of arithmetic and lets this representation do all the work . In the traditional representations of mathe­ matical theories , e . g . a set of axioms in a resolution theorem prover , it is quite easy to assert a contra­ dictory set of formulae without this situation being readily detected. I n the present representation assertions once made are readily accessible and any new assertion causes all s orts of conclusions to be drawn and asserted so tha t contradictions are usually spotted quickly.

In, 3 Gelernter achieved a similar effect by using two representations: a syntactic one for proving theorems with rules and axioms , and a diagram to guide this proof . His 'syntax computer ' discovered groups of sub- goals which would imply the present goal , and his 'diagram computer' vetted these sub- goals , rejecting those that were false in the diagram. The diagram was also used to pf ove certain very basic sub- goals (see 3 p . 42 No . 7 but this is a risky process , because although precautions were taken to prevent spurious coincidences entering into the diagram, there were still statements , true in the diagr am, but not provable from the hypothesis of the candidate theorem. The analogue of Gelernter 's diagrams in arithmetic would be to substitute particular numbers for the variables in some subgoal , and then compute the truth or falsity of the r esulting formula .

SUMS arose from an attempt to represent in the machine the concept, fairly common among mathematicians (see for instance 2) , of an ' i deal (or typical) integer ', i . e . an object with all the properties of an integer (e . g. being equal to , less than , not equal to or a divisor of some other integer) but which is not any particular integer (e . g . 3 , 13 or 53) . In a 'diagram' composed of ' idea l integers ' no spurious coincidences arise , so that anything true in the diagram is provable from the hypothesis of the theorem and anything false is not provable . So this diagram can be legitimately used for rej ecting and proving sub- goals . Of course something may be neither true nor false in the diagram.

Does SUMS prove theorems or does it check their validity? It certainly does not produce proofs in a formal logica l system, but neit'her does it exhaustively test the candidate theorem in some model . Nor, of course , does the practising mathemat ician confine him­ self to either of these techniques . Rather he is prepared to use a variety of methods to achieve his ends (see 6) . To convince himself , and others , of the soundness of his final proof , he produces a protocol . Formal logical systems were introduced to analyse and justify this procedure , and not to replace it as a method of discovery . SUMS is designed to simulate the behaviour of mathematicians . During the course of a proof it ' proves ' many facts ( i . e . convinces i tself of their truth) and records t hese as true ; it also produces a protocol which is intended to convince others of their truth ( i . e . a proof) .

It is the author's hope that the method of theor em proving outlined in this paper will prove applicable not just to arithmetic , but to all mathematical theories , especially classical systems with a single standard mode l , like analysis , geometry and set theory . In fact similar systems for geometry and set theory are now being built by Aaron Sloman and Mike Liardet respectively.

The author a l so hopes that this representation may make some contribution to the study of Psychological Modelling. In particular , maybe it sheds some light on the curious blackboard diagrams which mathematicians use to help them 'understand' problems .

ACKNOWLEDGEMENTS .

My debt to the M. I .T. Progress Report 7 will be obvious . Not quite as obvious, but equally important, are 'the conversations with my colleagues - Aaron Sloman , Bob Boyer , J Moore , Mike Liardet and numerous others.

REFERENCES .

1. Bundy , A. 'The Metatheor y of the Elementary Equation Calculus '. Ph .D. Thesis , University of Leicester, England . 1971 .
2. 2 . Beth, E.S . 'Semantic Entai lment and Formal Derivabil i ty'. Mededelingen der Kon. Ned . Ekad . v. Wet. New Series , Vol . 18 No . 13, Amsterdam, 1955 .
3. Gelernter , H. 'A Geometry Theorem Proving Machine '. Computers and Thought pp . 134- 52 , McGraw Hill, 1963 .
4. Hewitt , C. 'PLANNER : A Language for Manipulating Models and Proving Theorems in a Robot '. Proceedings of 1st IJCAI , Washington D.C. , 1969 .
5. Robinson, J .A. 'A Machine Oriented Logic based on the Resolution Principle ' . J .Assoc .Comput . Mach . 12 , pp . 23- 41 , 1965 .
6. Sloman, A. 'Interactions bet ween Philoaophy and Artificial Intelligence : The Role of Intuition and Non-Logical Reasoning in Intelligence '. Proceedings of 2nd IJCAI , pp . 270- 8, The British Computer Society, 1971 , also Artificial Intelligence 2 , pp . 209- 25 , North Holland Publishing Co ., 1971 .
7. Minsky, M. and Papert , S. 1 Pro.ject M.A.C. Progress Report' , pp . 129- 244, M. I .T., 1971 .