Automation of Diagrammatic Reasoning

Automation of Diagrammatic Reasoning

Mateja Jamnik, Alan Bundy, Ian Green

Department of Artificial Intelligence, 80 South Bridge Edinburgh, EHl lHN, UK

matejaj@dai.ed.ac.uk, A.Bundy@ed.ac.uk, I.Green@ed.ac.uk

Abstract

Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which humans can prove in a different way by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is more clearly perceived in these than in the corres­ ponding algebraic proofs: they capture an intu­ itive notion of truthfulness that humans find easy to see and understand. We are identify­ ing and automating this diagrammatic reason­ ing on mathematical theorems. The user gives the system, called DIAMOND, a theorem and then interactively proves it by the use of geo­ metric manipulations on the diagram. These operations are the "inference steps" of the proof. DIAMOND then automatically derives from these example proofs a generalised proof. The constructive w-rule is used as a mathemat­ ical basis to capture the generality of inductive diagrammatic proofs. In this way, we explore the relation between diagrammatic and algeb­ raic proofs.

1 Introduction OOOIOIOIQ

It requires only basic secondary school knowledge of mathematics to realise that the diagram above is a proof of a theorem about the sum of odd naturals.

It is an interesting property of diagrams that allows us to "see" and understand so much just by looking at a simple diagram. Not only do we know what theorem the diagram represents, but we also understand the proof of the theorem represented by the diagram and believe it is correct.

Is it possible to simulate and formalise this sort of diagrammatic reasoning on machines? Or is it a kind of intuitive reasoning particular to humans that mere machines are incapable of? Roger Penrose claims that it is not possible to automate such diagrammatic proofs. 1 We are taking his position as an inspiration and are try­ ing to capture the kind of diagrammatic reasoning that Penrose is talking about so that we will be able to sim­ ulate it on a computer.

The importance of diagrams in many domains of reas­ oning has been extensively discussed by Larkin and Simon [Larkin and Simon, 1987], who claim that "a dia­ gram is (sometimes) worth ten thousand words". The advantage of a diagram is that it concisely stores inform­ ation, explicitly represents the relations among the ele­ ments of the diagram, and it supports a lot of perceptual inferences that are very easy for humans.

It is exactly these characteristics of diagrams that we wish to exploit in our project. In this paper we present a system (which is currently being developed) called DIAMOND (DIAgraMmatic reasONing and Deduction), which reasons with diagrams. With this system, the user inputs a theorem of mathematics to be proved, instructs the system what diagram to start the search for the proof from, and decides what geometric operations to perform during the proof search. To implement these components is a hard task. We do not aim to discover proofs, but to investigate the relation between formal algebraic proofs and more "informal" diagrammatic proofs. Usually, the­ orems are formally proved with the use of inference steps which often do not convey an intuitive notion of truthful­ ness to humans. The inference steps are just statements that follow the rules of some logic. The reason we trust that they are correct is that the logic has been previ­ ously proved to be sound. Following and applying the rules of such a logic guarantees us that there is no mis­ take in the proof. We might not have such a guarantee in DIAMOND, but will gain a more informal insight into the proof. Ultimately, the entire process of diagrammatically proving theorems will illuminate the issues of formality, rigour, truthfulness and power of diagrammatic proofs.

1 Roger Penrose presented his position in the lecture at International Centre for Mathematical Sciences in Edin­ burgh, in celebration of the 50th anniversary of UNESCO on 8 November, 1995.

In Section 2 we list some of the theorems that we aim to prove. Section 3 presents DIAMOND's architecture, some operations required, and the generalisation mech­ anism employed. Section 4 reports on some of our results and discusses future work. Section 5 discusses some of the related diagrammatic reasoning systems. Finally, we conclude by summarising the main points of this paper.

2 'Diagrammatic' Theorems

We are interested in mathematical theorems that admit diagrammatic proofs. In order to clarify what we mean by diagrammatic proofs we first list some example the­ orems. Then, we introduce a taxonomy for categorising these examples in order to be able to characterise the domain of problems under consideration.

2.1 Examples

Pythagoras' Theorem

Pythagoras' Theorem states that the square of the hypo­ tenuse of a right angle triangle equals the sum of the squares of its other two sides. Here is one of the many different diagrammatic proofs of this theorem, taken from [Nelsen, 1993, page 3]:

The proof consists of first taking any right angle triangle, completing a bigger square by joining to it identical tri­ angles and squares along its sides, and then rearranging the triangles in a bigger square. For a more elaborate explanation, see [Jamnik et a/., 1996].

Sum of Odd Nat urals

This example is also taken from [Nelsen, 1993, page 71]. The theorem about the sum of odd naturals states the following:

Note the use of parameter n. If 2 we take a square we can cut it 1+3+ · ·+(2n-l) = n into as many L's (which are made 0 10 \0 IOIOlQ up of two adjacent sides of the square) as the size of the side of the square. Note that one L is 0 10 10 0 0 0 made out of two sides, i.e., 2n, but the shared vertex has been counted twice. Therefore, one L has a size of (2n- 1), where n is the size of the square.

Geometric Sum

This example is also taken from [Nelsen, 1993, page 118]. A theorem about . a geometric sum of 2 1 n states the fol­ lowing:

Note the use of ellipsis in the diaTk f 2 + 4 + 8 + · · · = gram. a e a square o unit size. Cut it down the middle. Now, cut one half of the previous cut square into halves again. This will create two identical squares making up a half of the original square. Take one of these two squares and continue doing this procedure indefinitely.

2.2 Classification

From the analysis of the examples that we presented above, and many others, three categories of proofs can be distinguished:

Category 1: Proofs that are not schematic: there is no need for induction to prove the general case. Simple geometric manipulations of a diagram prove the individual case. At the end, generalisation is required to show that this proof will hold for all a, b. Example theorem: Pythagoras' Theorem.

Category 2: Proofs that are schematic: they require no inductive step to prove the theorem for each con­ crete diagram (i.e., problem), but require induction for the general diagram of size n (a concrete diagram cannot be drawn for this instance) . The construct­ ! ve w-rule (explained in more detail in Section 2.4) ts used to generate a generalised proof from the indi­ vidual proof instances. Example theorem: Sum of Odd Naturals.

Category 3: Proofs that are inherently inductive: for each individual concrete case of the diagram they need an inductive step to prove the theorem. Every particular instance of a theorem, when represen­ ted as a diagram requires the use of abstractions to represent infinity. Thus, the constructive w-rule (defined later) is not applicable here. Example the­ orem: Geometric Sum.

2.3 Problem Domain

We choose mathematics as our domain for theorems since it allows us to make formal statements about the reasoning, proof search, induction, generalisations, and such issues. Having introduced the examples and their categorisation, which is by no means exhaustive, we are now able to further restrict our domain of mathematical theorems.

First, we narrow down the domain to a subset of the­ orems that can be represented as diagrams without the need for abstraction (e.g., the use of ellipsis, as in the above example theorem for geometric sum). Conducting proofs and using abstractions in diagrams is problematic, since it is very difficult to keep track of these abstrac­ tions while manipulating the diagram during the proof procedure.

Second, we consider diagrammatic proofs that require induction to prove the general case (i.e., Category 2 above). Namely, diagrams can be drawn only for con­ crete situations and objects. We cannot draw, for example, an n x n square. Our challenge is to find a generalisation mechanism that does not require using abstractions in diagrams. The generality of the proof will be captured in an alternative way (by using the con­ structive w-rule; see Section 2.4).

It is clear that we will need a stronger problem domain definition which remains a subject of our research. One possibility is to consider theorems of arithmetic or num­ ber theory only. To date, DIAMOND is targeted to prove examples of Category 2, but we may also implement dia­ grammatic theorem proving of examples for Category 1.

2.4 Constructive w-Rule

As mentioned above we could use the constructive w-rule to prove theorems of Category 2. Siani Baker in [Baker et a/., 1992] did some work on the constructive w-rule and schematic proofs for arithmetic theorems. Here, we explain the idea behind schematic proofs and how it can be applied to diagrammatic proofs.

Schematic Proof

Schematic proofs use the constructive w-rule which is an alternative to induction. The constructive w-rule allows inference of the sentence VxP(x) from an infin­ ite sequence P(n) nEw of sentences.

where "if each P(n) can be proved in a uniform way (from parameter n), then conclude VnP(n)." The cri­ terion for uniformity of the procedure of proof using the constructive w-rule is taken to be the provision of a gen­ eral schematic proof, namely the proof of P(n) in terms of n, where some rules Rare applied some function of n (i.e. , fR( n)) times (a rule can also be applied a constant number of times). Now, proof(n) is schematic inn, since we applied some ruleR n times. The following procedure summarises the essence of using the constructive w-rule in schematic proofs:

1. Prove a few special cases (e.g., P(2) , P(16) , ... ).
2. Generalise (guess) proof(n) (e.g., from proof(2), proof(16), ... ).
3. Prove that proof(n) proves P(n) by meta-induction on n .

The general pattern is extracted (guessed, to be exact) from the individual proof instances by (learning type) inductive inference. By meta (mathematical) induction we mean that we introduce system PAw (i.e., Peano Arithmetic with w-rule) such that:

where ":" stands for "is a proof of", and s( n) is a nota­ tion for successor of n . This essentially says that by using the rules on P(s(n)) we can reduce it to P(n). For more information, see [Baker et a/., 1992] .

Diagrams and Schematic Proofs

We claim that we can extend Baker's work on schematic proofs in our diagrammatic proofs in that the generality of the diagrammatic proof is embedded in the schem­ atic proof. Thus , we eliminate the need for abstractions in diagrams , and can generalise from manipulations on concrete diagrams.

The diagrammatic schematic proof starts with a few particular concrete cases of the theorem represented by the diagram. The diagrammatic procedures (i .e., opera­ tions) on the diagram are performed next , capturing the inference steps of the diagrammatic proof. In DIAMOND , this step (also referred to as the proof checking step) is done interactively with the user, and corresponds to the first step of the schematic proof procedure given in the previous section.

The second step is to generalise the operations involved in the schematic prooffor n. Note that the gen­ erality is represented as a sequence of diagrammatic pro­ cedures (operations) and not as a general representation of a diagram. In DIAMOND, this step is done automatic­ ally. More precisely, the basic idea is to consider proofs for n + 1 which can be reduced to proofs for n (or con­ versely, such proofs for n which can be extended to proofs for n + 1 by adding to them some additional sequence of operations). The difference between the prooffor (n+ 1) and the proof for n, i.e., the additional sequence of oper­ ations in the proof for (n + 1) with respect to the proof for n is referred to as the step case of the generalised proof.

The last step in the schematic proof procedure is to prove by meta-induction that the generalised diagram­ matic schematic proof is indeed correct. It remains a subject of this research project to determine whether this will be considered at all or not. An alternative at this point could be to translate the diagrammatic proof to an algebraic proof.

2.5 Schematic Diagrammatic Proof for the Sum of Odd Naturals

Now we can attempt to structure the diagrammatic proofs in a more formal way. Here we list the proof for the theorem about the sum of odd naturals as a sequence of steps that need to be performed on the diagram:

1. Cut a square into n L's, where an L consists of 2 adjacent sides of the square.
2. Cut each L into two segments.
3. For each L, join these two segments one on top of the other length-wise (note that one of the two segments is always one unit longer than the other , thus an L always consists of an odd number of units, i.e., 2n- 1).

Identifying the operations (i .e., geometric manipula­ tions) that were required to prove the theorem will help us define a large repertoire of such operations which will be used in the diagrammatic proofs. The generality of the proof is captured by the use of the constructive w­ rule, by which we take a few special cases of the diagram (say a square of size 15 and 16) , and find the general pat­ tern of the proof that will hold for each case (e.g., the schematic proof given above).

3 DIAMOND System

Clearly, an important issue in the development of DIA­ MOND is the internal representation of diagrams and operations on them. The hope is that these capture the intuitiveness, rigour and simplicity of human reasoning with diagrams. We aim to emulate human visual percep­ tion to enable a theorem prover to prove theorems using diagrammatic inference steps. There are several repres­ entations available to achieve this. In DIAMOND we use a mixture of Cartesian and topological representations.

The architecture of DIAMOND consists of two parts. The diagrammatic component forms and processes the diagram. The inference engine deals with the diagram­ matic inference steps. It processes the operations on the diagram. An important submodule is the generalisation tool (i .e., implementation of the constructive w-rule) .

The rest of this section presents the operations used to construct proofs, the structure of proofs and the general­ isation mechanism used in DIAMOND. For more inform­ ation see [Jamnik et a/. , 1996].

3.1 Geometric Operations

Geometric operations (also referred to as manipulations or procedures) capture the inference steps of the proof. Thus, a sufficiently large number of such operations which are then available to the user in the search for the proof, needs to be identified and formalised. Since we are not generating, i.e. , discovering diagrammatic proofs, but rather we are trying to understand them, we can expect from the user to input these operations. To date, a small number of such operations has been implemented and is available to the user.

We distinguish between two types of operations:

Atomic operations: they are basic one-step opera­ tions that will be combined into more complex oper­ ations. Examples of such operations are: rotate, translate, cut, join, project from 3D to 2D, remove, insert a segment .

Composite operations: they are more complex, typ­ ically recursive operations, composed from simple atomic ones. Perhaps, we can think of them as tactics or tacticals in automated reasoning. In the future we need to investigate several different recursive structures of diagrams. Depending on the theorem that we are proving, we use a different recursive composite operation. Ideally, the internal representation of the diagram should be pertinent to the composite operation that we are performing on it . ·

In the example of the theorem for the sum of odd naturals the proof consists of the following operations: /cut, spliLtop_row, rotate90, join, rem_/efLcolumn , remove_dot.

3.2 Constructing a Proof

DIAMOND's example proof consists of a sequence of applications of geometric operations on a diagram. The generalisation is then carried out automatically, if any such generalisation exists for the two given example proofs. 2 DIAMOND expects the example proofs to be formulated in a particular way where the order of oper­ ations in the user 's formulation of the proofs is crucial. Both example proofs are expected to be given with the same order of operations, but with some extra operations in the case of the proof(n + 1) for some particular n.

Consider the example for the sum of odd naturals. The step cases for proofs for n = 4 and n = 3 look as follows :

olo:o:o o o o:o -o o 0 0 0 0 0 01010 o o o o-o1o o o-o o olo olo:o o 0 0 0 0 010 o o o-o1o o-o olo

The aim is to recognise automatically the structure of the proof from a linear sequence of applications of oper­ ations, so that the example proofs for n and n + 1 can be reformulated in the general case into the following:

where for each n, A(n) is a step case consisting of a sequence of applications of some operations and B( 1) is a base case for n = 1. Alternatively, we seek this recursive reformulation :

A further issue that we are investigating currently is to relax the requirement for a particular ordering of oper­ ations in formulating example proofs. Sets with partial ordering could be used as an alternative.

3.3 Generalisation

Given some example proofs DIAMOND needs to general­ ise from them, so that the final diagrammatic proof is not only for the cases of specific n's, but holds for all n. Such a schematic proof consists of a general sequence of applications of some operations, where the number of application of each operation is dependent on n or is a constant.

DIAMOND distinguishes between two types of example proofs: destructive , i.e., the example proofs which are formulated so that the base case operations are per­ formed last (in a sense the initial diagram is "destruc­ ted" by the application of operations down to a trivial diagram, forming the proof along in this way) ; and con­ structive, i.e., the base case operations are performed first followed by the step case operations.

The proofs that have the same structure for all n are called !-homogeneous proofs. Proofs can be c-homo­ geneous; then there are c cases of the proof. We say that if all concrete instances of the proof (for instances of numbers that "equal modulo c" ) have the same structure and can be generalised, then the proof is c-homogeneous. If there are c cases, then there are c different generalised proofs, one for each case. The following theorem can be proved:

2 If the proof contains a case split for say, even and odd integers, and the two example proofs given are for two dif­ ferent cases, then DIAMOND cannot generalise from them. However, DIAMOND recognises that the example proofs were given for different cases, and requests the user to supply another example proof for each case, in order for it to be able to generalise. This will be further explained in Section 3.3.

Theorem 1: If a proof is c-homogeneous, then it is also (kc)-homogeneous for every natural number k > 0.

The immediate consequence of Theorem 1 is:

Corollary 1: If a proof is not c-homogeneous, then it is also not /-homogeneous for every factor f of c.

In a c-homogeneous proof we will denote by Br a base case for a branch of numbers which give remainder r when divided by c. Br is actually a proof for the smallest natural number that gives remainder r when divided by c. A special case is a class of numbers divisible by c, where a base case is going to be Be, which is a proof for n =c.

The general representation of the destructive proof is formalised as follows- let:

• n = kc+ r
• where c = number of cases and r < c
• and i > 1.

Then the recursive definition of a general proof is:

for r # 0:

where Ar is a step case and Br is a base case for a class of proofs where n = r(mod c). The formalisation of generalised proof for constructive proofs is symmetric to the one given above.

Generalising For All Linear Functions

As mentioned above, we aim to recognise the particular recursive structure of the given example proofs. More precisely, we want to extract the step case A and the base case B of the proof and then generalise them for all n . The general methodology employed for doing this can be demonstrated as:

The first step of the generalisation algorithm is to extract the difference between the two given example proofs for n1 and n2 (n1 > n2), where c = n1 - n2, in the hope that this, when generalised, will be the step case A of the proof. This is done by associative matching which detects and returns the difference between the two example proofs. Now we have a concrete step case of the proof. This difference consists of a few operations opk each applied Xk,n 1 times for some natural k.

To make a step case general, we need to find the dependency function between every Xk,n 1 and n1. This demands identifying a function of n1, which would give a specific Xk,n 1 , i.e., fk(nt) = Xk ,n 1 for some k and n1. DIAMOND assumes that the dependency is linear: an+ b. Thus, let us write for each opJi a linear equation an1 + b = Xk,n 1 , where n1 and Xk,n 1 are known.

The subsequent stage of the generalisation is to extract the next step case from the rest of the example proof for the corresponding new n (i .e., n2). If successful , continue extracting step cases for the corresponding n's from the rest of the proof until only the base case is left.

Since we are dealing with inductive proofs, it is expec­ ted that every step case of a proof will have the same structure, i.e., will consist of the same seq~ence of applic­ ation of operations, but a different number of times. Thus, we could in the same way as above for every operation opk write a linear equation an2 + b = Xk ,n,· However, the number Xk,n 2 of applications of a particu­ lar operation opk in the next step case is not known. A possible value of Xk,n, is acquired by counting the num­ ber x' of times every operation opk of the initial step case occurs in the rest of the proof. The actual value of the number of occurrences of each operation could be any number from 0 to x 1 · Thus, we do branching for all such values and thus we have:

where n1, n2, Xk ,n, and Xk,n, are known, so the equa­ tions can be solved for a and b, and Xk,n, takes values from 0 to x'. This results in several possible potential generalisations of the step case. The aim is to eliminate those that are impossible. After checking if step cases for all n down to base case are structurally consistent one hopes to be left with at least one possible generalisation of the example proofs. The step case is rejected when the sequence of operations in the subsequent step cases is impossible, i.e. , the functions were wrong. This normally occurs when the dependency function gives a negative number of applications of a particular operation, when the calculated sequence is not identical to the rest of the example proof, or when there is no integer solution to our equations. Usually, there will be only one possible generalisation of the two given example proofs.

The example proof for the sum of odd naturals is generalised into the following step case and base case: A(n) = {lcut{1), spliUop_row{1}, rotate90{1},

where the function in parentheses indicates the number of times that the operations are applied for each partic­ ular n.

£-Homogeneous Proof

Assume two example proofs for the sum of odd naturals (the example proof would consist of making n !cuts, and then showing that each L consists of an odd number of dots). If the user supplies two example proofs for values of n and n + 1, for some concrete n, then there is no prob­ lem, so DIAMOND will generalise normally and determine that the proof is !-homogeneous. However, should the user supply proofs for n and n + 2 for some concrete n, the first stage of generalisation would determine that the step case consists of two lcuts. However, a complete recursive function for generalisation requires a step case to consist of one lcut only.

DIAMOND checks this by trying to split the step case into further f structurally the same sequences of oper­ ations, for all factors f of c in order to obtain an /­ homogeneous proof. If the method fails, then there is no such /-homogeneous further generalisation of the step case A(n) . If the method succeeds, and DIAMOND finds a new generalisation ofthe step case, call this A'(n), then it also needs to find a new base case B' ( r') if r' # 0, or B'(f) if r' = 0, where the previous r for c was such that n = kc + r and r < c, and the new r' is now such that n = kf + r' and r' <f.

4 Results and Further Work

DIAMOND is implemented in Standard ML of New Jer­ sey, Version 109. The code is available upon request to the first author.

So far, the interactive construction of proofs and auto­ matic generalisation from example proofs have been implemented in DIAMOND. We can prove a few the­ orems: sum of odd naturals, sum of all naturals, sum of Fibonacci squares. We are working on more examples.

VVe want to relax the requirement for a particular for­ mulation of example proofs. Partially ordered sets could be used. However, this would require recognition and generalisation of diagrams (as opposed to a sequence of operations).

There is also a possibility of allowing non-linear dependency functions.

Another issue that will be addressed is to prove that the derived generalisation of a diagrammatic proof is indeed correct .

Finally, some recognition and generalisation of dia­ grams using abstractions could be an interesting issue to consider. The difficulty is to keep track of these abstrac­ tions while manipulating the diagram.

5 Related Work

Several diagrammatic syste~s such as the �eo~etry Ma­ chine [Gelernter, 1963], Dmgram Configuratwn model [Koedinger and Anderson, 1990], GROVER [Barker­ Plummer and Bailin, 1992], and Hyperproof [Barwise and Etchemendy, 1991] have been implemented in the past and are of relevance to our system.

However, they all use diagrams to model algebraic statements, and use these models for heuristic guidance while searching for an algebraic proof. In contrast, proofs in our system are explicitly constructed by operations on diagrams.

Closer to our work, but not in the domain of diagram­ matic reasoning, is work done by Siani Baker [Baker et a/. , 1992] described in Section 2.4, whereby we exploit the uniform structure of inductive proofs to generalise from example proofs.

6 Conclusion

We presented a diagrammatic reasoning system, DIA­ MOND, which supports interactive construction of dia­ grammatic proofs. The system automatically generalises from examples to give a general proof for all n . The hope is that automating the 'informal' diagrammatic reason­ ing of humans will shed light on the issues of formality, informality, rigour and 'intuitive' understanding of the correctness of diagrammatic proofs. In the long run, tools such as DIAMOND could lead to e.g. improved maths courses in schools.

Acknowledgements

We should like to thank Predrag J aniCic for inspir­ ing discussions about some of the work presented here. The research reported in this paper was supported by Artificial Intelligence Dept. grant, University of Edin­ burgh, and the Slovenian Scientific Foundation supple­ mentary grant for the first author, and by EPSRC grant GR/L/11724 for the other two authors.