--- title: "Doing Arithmetic with Diagrams" authors: - "Alan Bundy" doi: "" url: "https://ijcai.org/proceedings/1973/18" pdf: "https://ijcai.org/proceedings/1973/0018.pdf" venue: "Proceedings of the Third International Joint Conference on Artificial Intelligence" year: 1973 pages: "130-137" track: "Theorem Proving and Logic: 2" keywords: --- # Doing Arithmetic with Diagrams Alan Bundy *Proceedings of the Third International Joint Conference on Artificial Intelligence*, pages 130-137. ## Abstract A theorem prov er for part of a rith metic is described which p rove s t heorems by re presenting t hem in the f orm of a diag r am or networ k . The nodes of this network re p res e nt ' ideal intege r s ', i . e . objects which ha ve al l the pr ope rt ies of intege r s , without being any par ticu l ar integer . The links in the network re presen t relationships between ' ideal integers '. The procedures which dr aw these diag r ams make elementary deductions based on their built - in know l edge of the functions and predicates of a rithmet i c . This t heo re m prover is in t ended as a mode l of some kinds of human problemsolving behaviour. ## Full text ## 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 . ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000000_a9a9d7b21233ee73fe81c725ed6fd8c04aef062822dba21dc3b827aab1246b59.png) 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) · ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000001_ee27e0fd5fed1e3d621d7a5db6e1a044c64f2638b9f78ac8a5d2e6332906f569.png) ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000002_6d863088f4c6a6934da1ed18c6593e95b943b6988473611addc0a9bb1ef0c241.png) 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) . ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000003_ee6b7ac057870acc6f6bad9689b10b185cc23f96e2b9fa0e5d048c59c26d116d.png) 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 ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000004_086be16a74a8e4bbebc9ff55d6b0e94a4e7afb974ca725cfef369d1ca4ed9bf8.png) ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000005_5501e3a1e7d35bd10333d0d23fee917ff129953254956e41e789c2d31b6fd1a9.png) 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 ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000006_75265b53ac930270b7b2e6eacec6b87d904a2b352a35b9b74ec43eb579f2eb0c.png) 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 : ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000007_7cdb2d9395d3efbe45cda0f5bb873266a29895fc636eeb0fa5dc22fb4db62f36.png) - (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. ![Image](https://ijcai.org/proceedings/1973/fulltext/18/image_000008_ba1d6bab539b7e5b8f21068d4553a13d9fcf671fdb83ca20b3fe1aa92f4f973a.png) 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 . | Theorem | Time Spent (in sees. of C.P .U. Time) | |----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------| | 1 . 2 . 3· 4· 5. 6. 7. 8 . g. 10 . 11. 12. 13 . 14. 15. a + ( b + c) a + ( b .: a) a .: ( b + c) (a + b) .: c 0 < Suc(a) (a+ b) + c b + ( a .: b) (a b) • c (a .: c) + ( b ( c ~ a)) ( b