On Automating Diagrammatic Proofs of Arithmetic Arguments.
Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is often more clearly perceived in these proofs than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete, rather than general diagrams are used to prove particular concrete instances of the universally quantified theorem. The diagrammatic proof is captured by the use of geometric operations on the diagram. These operations are the inference steps of the proof. An abstracted schematic proof of the universally quantified theorem is induced from these proof instances. The constructive -rule provides the mathematical basis for this step from schematic proofs to theoremhood. In this way we avoid the difficulty of treating a general case in a diagram. One method of confirming that the abstraction of the schematic proof from the proof instances is sound is proving the correctness of schematic proofs in the meta-theory of diagrams. These ideas have been implemented in the system, called Diamond, which is presented here.
Introduction
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
Portions of this work were published in the Proceedings of the International
Joint Conference on Artificial Intelligence in (Jamnik et al, 1997).
Mateja Jamnik et al.
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 a challenge and are trying to capture the kind of
diagrammatic reasoning that Penrose is talking about so that we will
be able to emulate it on a computer.
The importance of diagrams in many domains of reasoning has been
extensively discussed by Larkin and Simon (Larkin & Simon, 1987),
who claim that "a diagram is (sometimes) worth ten thousand words".
The advantage of a diagram is that it concisely stores information,
explicitly represents the relations among the elements of the diagram,
and it supports a lot of perceptual inferences that are very easy for
humans. Diagrams have been extensively used in the history of mathematics
to aid informal mathematical reasoning. The use of diagrams in
explanations of theorems and proofs of geometry dates back to Ancient
Greece, and the time of Aristotle and Euclid. Thus it is surprising perhaps
that more recently, starting with the invention of formal axiomatic
logic in the sense of Frege, Russell and Hilbert, diagrams have
been denied a formal role in theorem proving. It is generally thought
by logicians that diagrams have no accepted syntax nor semantic theory
in a logical formalism which would make them rigorous enough to
be used in formal proofs. Only very recently, in the last two decades,
have there been efforts to fill this gap and investigate whether and how
diagrams can be used in formal proofs. For instance, the investigation
of Pierce's existential graphs in (Sowa 84), the work on GROVER in
(Barker-Plummer & Bailin, 1997), the work on Hyperproof in (Bar-
wise & Etchemendy, 1991), the introduction of computational models
for interpreting Euler's circles in (Stenning & Oberlander 95), the analysis
of the use of Venn diagrams as a formal system in (Shin 95), and
the formalisation of a logical theory of Venn diagrams in (Hammer 95).
Our work contributes in some sense to the effort in the research
from the formal perspective on the use of diagrams, especially that of
automated reasoning systems which use diagrams in the reasoning pro-
cess. Our aim is to formalise diagrammatic reasoning and to show that
diagrams can be used for proofs. In this paper we show how diagrams
can be used for proofs in a formal system. We look into how theorems
Roger Penrose presented his position in the lecture at International Centre
for Mathematical Sciences in Edinburgh, in celebration of the 50th anniversary of
UNESCO on 8 November, 1995.
On Automating Diagrammatic Proofs of Arithmetic Arguments 3
of mathematics can be expressed as diagrams for some concrete values,
i.e., ground instantiations of a theorem. The initial diagram is manipulated
using some geometric operations. The sequence of geometric
operations on a diagram represents the inference steps of a diagrammatic
proof. Such a concrete proof instance is called an example proof.
The set of all available operations defines the proof search space. A general
pattern is extracted from these proof instances, and is captured in
a recursive program. This recursive program constitutes a general diagrammatic
proof for the universally quantified theorem. An existing
technique in logic, namely the constructive !-rule, justifies the step
from schematic proofs to theoremhood.
We also aim to investigate the relation between formal algebraic
proofs and more "informal" diagrammatic proofs. Usually, theorems
are formally proved with the use of inference steps which often do not
convey an intuitive notion of truthfulness to humans. The inference
steps of a formal symbolic (as opposed to diagrammatic) proof are
statements that follow the rules of some logic. The reason we trust
that they are correct is that the logic has been previously proved to be
sound. Following and applying the rules of such a logic guarantees that
there is no mistake in the proof. We want to have such a guarantee
in our proof system, and moreover, to gain an 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.
We implemented a diagrammatic proof system called Diamond,
which automates such diagrammatic reasoning and applies it to problem
solving in mathematics. The user interactively constructs example
proofs by choosing an initial diagram which represents the theorem,
and then applies diagrammatic operations to build a proof. Diamond
then automatically extracts a general pattern from these instances, and
captures it in a recursive program.
First, we list some of the theorems and their diagrammatic proofs.
These help us define our problem domain. Second, we present Dia-
mond's architecture, some operations required, the abstraction mechanism
employed, and indicate how to verify the abstracted proof. Next,
we report on some of our results and discuss future work. Then, we discuss
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
4 Mateja Jamnik et al.
we first list some example theorems. 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
2.1.1. Pythagoras' Theorem
Pythagoras' Theorem states that the square of the hypotenuse 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):
a
c
a
b a
a
a
The proof consists of first taking any right angle triangle, completing a
bigger square by joining to it identical triangles and squares along its
sides, and then rearranging the triangles in a bigger square.
2.1.2. Sum of Odd Naturals
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 we take a square we can cut it into
as many ells (which are made up of two adjacent sides of the square)
as the magnitude of the side of the square. Note that one ell is made
out of two sides, i.e., 2n, but the shared vertex has been counted twice.
Therefore, one ell has a magnitude of (2n \Gamma 1), where n is the magnitude
of the square.
2.1.3. Geometric Sum
This example is also taken from (Nelsen, 1993, page 118). A theorem
about a geometric sum of 1
states the following:
On Automating Diagrammatic Proofs of Arithmetic Arguments 52
1 _Note the use of ellipsis in the diagram. Take a square of unit magnitude.
Cut it down the middle. Now, cut one half of the previously 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 (see (Jamnik, 1998) and (Nelsen, 1993)), three categories of
proofs can be distinguished:
Category 1: Non-inductive theorems. Usually, there is only one representative
diagram for all instances of the theorem. There is no
need for induction to prove the general case: proofs are not schem-
atic. Simple geometric manipulations of a diagram prove the individual
case. Abstraction is required to show that this proof will
hold for all a; b. Theorems are of continuous space. Example the-
orem: Pythagoras' theorem.
Category 2: Inductive theorems with a parameter. A diagram is a representative
of a particular instance of a theorem. Proofs are schem-
atic: they require induction for the general diagram of magnitude n
(a concrete diagram cannot be drawn for this instance). An alternative
method can sometimes be used to capture the generality of
the proof. Theorems are of discrete space. Example theorem: sum
of odd naturals.
Category 3: Theorems whose proofs 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 represented as a diagram requires the use of abstractions
to represent infinity. Theorems are of continuous space. Example
theorem: geometric sum.
6 Mateja Jamnik et al.
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, abstractions 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 theorems 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 problemat-
ic, since it is very difficult to keep track of these abstractions 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 concrete situations and objects. We cannot draw, for
example, an n \Theta n square without some abstraction device, e.g., ellipsis.
Our challenge is to find a mechanism for extracting a general proof that
does not require using abstractions in diagrams. 2 The generality of the
proof will be captured in an alternative way (by using the constructive
!-rule - see x2.4).
Third, to date we consider theorems of natural number arithmetic
only. Diamond is designed to prove examples of Category 2, where diagrams
represent natural numbers. A more formal definition of diagrams
is given in x3.4.1. We may extend diagrammatic theorem proving for
examples of Category 1 as well.
One of the possibilities for future work is to consider a need for a
more formal problem domain definition.
2.4. Constructive !-Rule
As mentioned above we use the constructive !-rule to prove theorems
of Category 2. Siani Baker in (Baker et al, 1992) did some work on the
constructive !-rule and schematic proofs for theorems of arithmetic.
Here, we explain the idea behind constructive !-rule and schematic
proofs and how they can be applied to diagrammatic proofs.
2.4.1. Schematic Proof
Schematic proofs use the constructive !-rule which is an alternative
to induction. The constructive !-rule allows inference of the sentence
8xP (x) from an infinite sequence P (n) of sentences.
2 Note that (Barker-Plummer & Bailin, 1997) formalises the use of abstractions,
however in the domain of well founded relations.
On Automating Diagrammatic Proofs of Arithmetic Arguments 7
where "if each P (n) can be proved in a uniform way (from parameter
n), then conclude 8nP (n)." The criterion for uniformity of the procedure
of proof using the constructive !-rule is taken to be the provision
of a general schematic proof, namely the proof of P (n) in terms of n,
where some rules R are applied some function of n (i.e., f R (n)) times
(a rule can also be applied a constant number of times). Let the proof
of P (n) be captured using a recursive function proof(n). Now, proof(n)
is schematic in n, since we applied some rule R n times. The following
procedure summarises the essence of using the constructive !-rule in
schematic proofs:
1. Prove a few special cases (e.g. P (2), P (16), .
2. Abstract (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) from the individual proof
instances by (learning type) inductive inference. By meta mathematical
induction we mean that we introduce system Meta such that for all n:
where ":" stands for "is a proof of ". Baker used PA ! (i.e., Peano
arithmetic with !-rule) for the system Meta (Baker et al, 1992). The
meta inductive rule is defined as follows:
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 al, 1992).
2.4.2. Diagrams and Schematic Proofs
We claim that we can extend Baker's work on schematic proofs to our
diagrammatic proofs so that the generality of the diagrammatic proof
is embedded in the schematic proof. Thus, we eliminate the need for
abstractions in diagrams, and can extract a general schematic proof
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., operations) on the diagram are performed next,
8 Mateja Jamnik et al.
capturing the inference steps of the diagrammatic proof. This step corresponds
to the first step of the schematic proof procedure given in the
previous section x2.4.
The second step is to abstract the operations involved in the schematic
proof for n. Note that the generality is represented as a recursive
program which specifies a sequence of diagrammatic procedures (oper-
ations) that are used on a diagram, and not as a general representation
of a diagram. More precisely, the basic idea is to consider proofs for
which can be reduced to proofs for n (or conversely, such proofs
for n which can be extended to proofs for by adding to them
some additional sequence of operations). The difference between the
proof for (n and the proof for n, i.e., the additional sequence of
operations in the proof for (n respect to the proof for n is
referred to as the step case of the abstracted schematic proof.
The last step in the schematic proof procedure is to prove by meta-
induction that the abstracted diagrammatic schematic proof is indeed
correct. One way of proving the correctness of schematic proofs is to
create a theory of diagrams that models the processes in a diagrammatic
reasoning system and prove correctness there. A formal definition of
a diagrammatic proof of an arithmetic statement, and the correctness
of this diagrammatic proof will be discussed in x3.4.
2.4.3. Schematic Diagrammatic Proof for the Sum of Odd Naturals
Now we can 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 ells, where an ell consists of 2 adjacent sides
of the square.
2. For each ell, continue splitting from an ell pairs of dots at the end
of two adjacent sides of the ell until only 1 dot is left (note that for
each ell of magnitude n, we will have of dots plus another
dot which is a vertex of the two adjacent sides, i.e., 1).
Identifying the operations (i.e., geometric manipulations) 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 !-
rule, by which we take a few special cases of the diagram (say squares
of magnitudes 15 and 16), and find the general pattern of the proof
that will hold for each case (e.g., the schematic proof given above).
On Automating Diagrammatic Proofs of Arithmetic Arguments 9
3. Diamond System
The diagrammatic proof system Diamond is an embodiment of some of
the ideas presented in this paper. Diamond stands for Diagrammatic
Reasoning and Deduction.
Clearly, an important issue in the development of Diamond is the
internal representation of diagrams and operations on them. It was
George P'olya who was first to advise us on the importance of knowledge
representation (see (P'olya, 1945) and (P'olya, 1965)). Simon argued
P'olya's point further in (Simon 96) by stating that solving a problem
means representing it so that the solution becomes trivial, or at least
transparent. In automated reasoning it is difficult to see how to use
this advice, since there is normally only one representation scheme for
the problem which is available to the system. In Diamond we choose
a representation which we hope captures the intuitiveness, rigour and
simplicity of human reasoning with diagrams. We aim to represent diagrams
in a way which enables a theorem prover to prove theorems using
diagram.
In Diamond we use a mixture of Cartesian and topological rep-
resentations. Diamond uses a primitive notion of a diagram, a dot.
All other elementary and derived diagrams (e.g., rows, columns, ells,
frames, squares, triangles, rectangles, etc.) are composed in various
ways out of dots. The advice of P'olya about alternative representations
can readily be used in Diamond. Namely, diagrams can be represented
in a variety of different ways. For instance, a square is represented as: a
sequence of rows; a sequence of columns; a concentric sequence of cir-
cumferences, each of which is called a frame; a nested sequence of ells;
a sequence of four similar squares; a matrix; a sequence of diagonals.
The choice of the representation that Diamond uses is important.
Most of the proofs that Diamond proves require some kind of recursive
decomposition of a diagram. Each alternative representation makes
available a different form of recursive decomposition. For more information
on the choice of internal representation for diagrams in Diamond
see (Jamnik, 1998).
The architecture of Diamond consists of two parts. The diagrammatic
component forms and processes the diagram. It is the interface
between Diamond and the user. The inference engine deals with the
diagrammatic inference steps. It processes the operations on the dia-
gram. An important submodule is the abstraction mechanism which is
used to extract general schematic proofs from example proofs.
The rest of this section presents the operations used to construct
proofs, the structure of proofs and the abstraction mechanism used in
Diamond.
Mateja Jamnik et al.
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.
Diamond is targeted to prove theorems of discrete arithmetic. Diagrams
are a way of representing natural numbers. The interest lies in
the effect on the numbers that diagrams represent after an operation
has been applied on the diagrams. Thus, the operations join and split
diagrams apart in various ways. Some operations are just simple ones
(e.g., split a row from a square), and some are more complicated ones
(e.g. decompose a square into a sequence of rows). Hence, Diamond
distinguishes between two types of operations, atomic and composite: 3
Atomic operations: are basic one-step operations that can be combined
into more complex operations. Examples of such operations
are: rotate, translate, cut, split, join, remove, insert a segment,.
To date, there are fourteen atomic operations implemented in Diamond

Composite operations: are more complex, typically recursive opera-
tions, composed from simple atomic ones. One can think of them as
tactics in automated reasoning. Composite operations are defined
in terms of decomposition of different recursive representations
of diagrams. Depending on the theorem at hand, the diagram is
viewed using a particular representation, which enables one to use a
particular recursive composite operation. Ideally, the internal representation
of the diagram is pertinent to the composite operation
that is being carried out on it. Such a representation would
render an operation very easy to apply. It would be just a simple
decomposition of the representation of a diagram. Examples of such
operations are: recursive decomposition of a square into rows, or
columns, or ells, or frames,.
In the example of the theorem for the sum of odd naturals the proof
consists of the following operations: lcut and split ends.
3 A complete list of operations can be found in (Jamnik, 1998), however, a more
formal definition of operations as part of the diagrammatic theory can be found in
On Automating Diagrammatic Proofs of Arithmetic Arguments 11
3.2. Constructing a Proof
Diamond's example proof consists of a sequence of applications of
geometric operations on a diagram. The abstraction is then carried out
automatically, if any such abstraction exists for the two example proofs
given. 4 Diamond expects the example proofs to be formulated in a
particular way where the order of operations in the user's formulation
of the example 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 of (n + 1) for some particular n.
Consider the example for the sum of odd naturals. The step cases
for proofs for look as follows:
The aim is to recognise automatically the structure of the proof from
a linear sequence of applications of operations, so that the example
proofs for n and n+ 1 can be reformulated in the general case into the
where for each n, A(n) is a step case consisting of a sequence of applications
of some operations and B is a base case for Alternatively,
we seek this recursive reformulation:
Note that proof(0) is often an empty list of operations, because often
no diagram is defined for a diagram which consists of no
dots.
4 If the proof contains a case split for say, even and odd integers, and the two
example proofs given are for two different cases, then Diamond cannot abstract
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 abstract. This will be further explained in x 3.3.2.
12 Mateja Jamnik et al.
A further issue that we are investigating currently is to relax the requirement
for a particular ordering of operations in formulating example
proofs. Sets with partial ordering could be used as an alternative.
3.3. Abstraction
Given some example proofs Diamond needs to abstract 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 is a general program
which specifies the applications of some operations, where the number
of application of each operation is dependent on n or is a constant.
We distinguish between two types of example proofs: destructor, i.e.,
the example proofs which are formulated so that the base case operations
are performed last (in a sense, the initial diagram is "destructed"
by the application of operations down to a trivial diagram, forming the
proof along in this way); and constructor, i.e., the base case operations
are performed first followed by the step case operations. In Diamond
we arbitrarily choose to use destructor schematic proofs.
A proof that has the same structure for all n, i.e., one recursive
function defines a complete proof for all n, is called a 1-homogeneous
proof. Proofs can be c-homogeneous; then there are c cases of the proof.
For instance, when there are two cases of a proof, one for odd and one
for even natural numbers, then there need to be two recursive functions
defining each case of the proof - the proof is 2-homogeneous. 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 abstracted, then
the proof is c-homogeneous. If there are c cases, then there are c different
abstracted proofs, one for each case. We seek the smallest complete
recursive definition of a proof, i.e., c potentially different schematic
proofs, if there are c cases. The following theorem and corollary will
help us define what we mean by the smallest complete proof:
THEOREM 1. If a proof is c-homogeneous, then it is also (kc)-homo-
geneous 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
f-homogeneous for every factor f of c.
In a c-homogeneous proof we will denote by B r a base case for a branch
of numbers which give remainder r when divided by c. B r is actually
a proof for the smallest natural number that gives remainder r when
divided by c.
A schematic proof is defined to be the smallest complete proof if
there is no other f-homogeneous proof obtainable from a c-homogeneous
On Automating Diagrammatic Proofs of Arithmetic Arguments 13
proof for any factor f of c, and all f schematic proofs for f cases are
defined.
The general representation of a destructor proof is formalised as
number of cases and r ! c, and
1. Then the recursive definition of a general proof is:
where A r is a step case and B r is a base case for a class of proofs where
denotes concatenation of sequences of operations: "do
operations of A(n+ 1), then proof(n)". The formalisation of abstracted
proof for constructor proofs is symmetric to the one given above.
3.3.1. Abstracting 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 abstract
them for all n. The general methodology employed for doing this can
be demonstrated as:
The first step of the abstraction algorithm is to extract the difference
between the two given example proofs for
in the hope that this, when abstracted, will be the
step case A of the proof. This is done by commutative and associative
matching 5 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 op k each applied x k;n 1
times for
some natural k.
To make a step case general, we need to find the dependency function
between every x k;n 1
and n 1 . This demands identifying a function of n 1 ,
which would give a specific x k;n 1
for some k and
assumes that the dependency is linear: an + b. This is a
heuristically adequate choice. Thus, let us write for each op k a linear
equation an 1
, where n 1 and x k;n 1
are known.
The subsequent stage of the abstraction is to extract the next step
case from the rest of the example proof for the corresponding new n
5 Using commutative and associative matching reduces the sensitivity to the order
of proof steps (Jamnik, 1998).
14 Mateja Jamnik et al.
(i.e., n 2 ). 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 expected that every
step case of a proof will have the same structure, i.e., will consist of
the same sequence of application of operations, but a different number
of times. Thus, we could in the same way as above for every operation
op k write a linear equation an However, the number x k;n2
of applications of a particular operation op k in the next step case is not
known. A possible value of x k;n 2
is acquired by counting the number x 0
of times every operation op k 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 0 . Thus, we do branching
for all such values and thus we have:
an
an
are known, so the equations can be solved
for a and b, and x k;n 2
takes values from 0 to x 0 . This results in several
possible potential abstractions of the step case. The aim is to eliminate
those that are impossible. After checking if step cases for all n down to
the base case are structurally consistent one hopes to be left with at
least one possible abstraction 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 abstraction of
the two given example proofs.
The example proof for the sum of odd naturals is abstracted into the
following step case and base case:
diagonal ends,n-1)]
where the function in parentheses indicates the number of times that
the operations are applied for each particular n.
3.3.2. f-Homogeneous Proof
Assume two example proofs for the sum of odd naturals (the example
proof would consist of making n lcuts, and then showing that each ell
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
On Automating Diagrammatic Proofs of Arithmetic Arguments 15
problem, so Diamond will abstract normally and determine that the
proof is 1-homogeneous. However, should the user supply proofs for
concrete n, the first stage of abstraction would
determine that the step case consists of two lcuts. However, a complete
recursive function for abstraction requires a step case to consist of one
lcut only.
Diamond checks this by trying to split the step case into a further
f structurally the same sequences of operations, for all factors f of c
in order to obtain an f-homogeneous proof. If the method fails, then
there is no such f-homogeneous further abstraction of the step case
A(n). If the method succeeds, and Diamond finds a new abstraction
of the step case, call this A 0 (n), then it also needs to find a new base
case
r 0 where the previous r for c was such that
and the new r 0 is now such that
3.4. Correctness of the Schematic Proof
The last stage of extracting a diagrammatic proof is to check that
the guessed general schematic proof is indeed correct. To prove that
the schematic proof is correct we need to show in some meta-theory
that proof(n) uniformly proves P (n) for all n, i.e., it gives a proof tree
with P (n) at its root, and axioms at its leaves. This requires reasoning
about proofs, i.e., meta-level reasoning. A meta-level proof using general
diagrams would be an obvious method for verifying our schematic
proof. However, such a meta-level proof would reintroduce the need for
abstractions (e.g. ellipsis) of diagrams, which we are trying to avoid.
One way of overcoming this problem is to define diagrams and operations
in a theory of diagrams where we can express abstract diagrams
symbolically rather than diagrammatically. In this theory we can verify
schematic proofs by defining the notion of applicability of a posited
proof. Given that a particular theorem is expressed as an equality, its
schematic proof is correct if applying the operations specified in the
schematic proof of the diagrammatic representation of the left hand
side of the theorem results in the diagrammatic representation of the
right hand side of the theorem. There are two conditions that need
to be satisfied. The first condition is that there is an appropriate diagrammatic
representation available for the conversion of the theorem
into its diagrammatic representation. The second condition is that the
operations of the schematic proof are defined on those diagrams.
Before we can state the definition of the correctness property of
schematic proofs, we need to formalise the machinery which will enable
us to model the processes of a diagrammatic proof. Therefore, we need
to formally define diagrams, operations on them, and the applicability
of operations of a schematic proof.
Mateja Jamnik et al.
3.4.1. Diagrams
Diagrams in the theory are defined to be of object type. Some examples
of the different kinds of object names in the theory are: row, column,
ell, frame, square, rectangle, and triangle.
Diagrams of the theory model natural numbers. Diamond's primitive
notion of a concrete diagram, a dot, is represented in the theory as
the natural number 1. Objects are introduced via a constructor func-
tion, diagram, which takes the name of the type of a diagram and the
list of parameters of its magnitude. Thus, the type of constructor function
diagram is name \Theta pnat list ! object. So, for instance, a square of
magnitude 4 is expressed in the theory as diagram(square,[4]). All elementary
and derived concrete diagrams are expressed using a primitive
object dot, hence in the theory they can be expressed using a constructor
function, the object name and some parameter representing a
natural number for the magnitude of the diagram.
Constant ; denotes a null diagram, or in other words an empty
diagram. We define that any diagram that is of 0 magnitude is an
empty diagram (note that a 2 b denotes that a natural number a is an
element of a list b; thus the type of an infix 2 is: pnat \Theta pnat list !
Note also, that all triangles are equilateral. 6 here are some examples
of diagrams: diagram(row,n), diagram(column,n), diagram(square,n) and
diagram(ell,n).
3.4.2. Operators
This section gives the operators available in the theory. First, we write
diagrammatic equality using d
which denotes that two lists of diagrams
are identical. here is the definition of d
where the function count can be defined by:
count(d; d ::
d
6 It is hard to represent discrete triangles that are of any magnitude, i.e., the
sides are of different and any magnitudes. Triangles are represented in a discrete
space. Hence, they appear to be right-angle triangles, despite the fact the all the
sides of any triangle are of equal discrete magnitude. Were we to extend Diamond to
prove theorems of real arithmetic (see x4), then there would be a need for continuous
space, and therefore a scope for triangles of any magnitude.
On Automating Diagrammatic Proofs of Arithmetic Arguments 17
Diagrammatic equality d
is a larger relation than an arithmetic
equality =, because it has all the properties of =, i.e., reflexivity, sym-
metry, transitivity and substitution properties, plus an additional one
- the order of elements in a list does not matter. Therefore, two lists
of diagrams, X and Y, are diagrammatically equal, X
d
even if the
orders in which the diagrams are listed in both lists differ. 7
We now define some operators that introduce the existence of several
diagrams (note that the data type pnat stands for non-negative natural
number of Peano arithmetic): @ is append on lists,; :: and nil are list
constructors (concatenation of elements onto a list, and an empty list);
\Omega is an infix operator which introduces a combination of a number
of identical lists of diagrams;
U denotes a collection of diagrams of
increasing magnitudes which are all of the same kind - it is analogous
to
for summation of integers. here is the recursive definition of
for all a  b: 8
a
d
a
d
diagram(name; f(i))@
Note that f is some function which generates a list of natural numbers
for a given number i. This list denotes the parameters of a magnitude
of a diagram.
3.4.3. Operations
Diagrammatic operations are represented via a function op : opname \Theta
object list ! object list. We give here a definition of one operation only,
but there are many more operations defined in the theory - see (Jamnik,
1998).
op(lcut; diagram(square; n):: D) d
diagram(ell; n)]@D (4)
3.4.4. One Apply and Apply
here we define what it means to apply an operation on a diagram
several times. We use a function apply and function one apply. Let:
7 Note that our definition of diagrammatic equality of lists is equivalent to bag
equality. The order of the elements in a bag does not matter.
8 Note that to simplify the notation we write
D(i) instead of
U (a; b; i:D(i)).
Mateja Jamnik et al.
one apply(0; opnm; D) d
one apply(n
apply([ ]; D) d
3.4.5. Equations
here we give a theorem which will be needed. (9) is provable from (7)
and (8). Its proof is not given here, but can be found in (Jamnik, 1998).
apply(ops; D :: D s
Let dmap denote a relation between a particular class of statements of
arithmetic and their equivalent diagrammatic expressions in the theory
of diagrams. The equivalence is defined to be over the size of the
diagram. The size of a diagram is defined to be the number of counters
(dots) in the diagram, i.e., the natural number that the diagram rep-
resents. dmap takes two arguments, an arithmetic expression and a list
of diagrams which could collectively represent this expression. Hence,
the type of the relation dmap is pnat \Theta object list. here are some general
conversions:
We have now formalised enough machinery to be able to define the
correctness property of a schematic proof.
DEFINITION 1 (Correctness of Schematic Proofs).
proof is a correct schematic proof of a particular conjecture 8n
R(n) if for all n there exist two lists of diagrams D and E such that
dmap(L(n); D) and dmap(R(n); E), and
apply (proof (n); D) d
On Automating Diagrammatic Proofs of Arithmetic Arguments 19
It is possible to prove the property in Definition 1 only if L(n),
R(n) and proof are known, i.e., for a specific case of a conjecture and
a schematic proof. Knowing L(n) and R(n) allows us to infer some
conversion relations which specify two lists of diagrams D and E. This
satisfies the first part of Definition 1. In the next section we prove the
correctness of a schematic proof for a particular conjecture at hand.
3.4.7. Proof of Correctness of Schematic Proofs for an Example
here we prove the property given in Definition 1 for an example of
a schematic proof of a theorem about the sum of odd naturals. The
theorem is stated as
1). The schematic proof of this
theorem is given as: 9
The proof of correctness of a schematic proof for this particular
example requires induction on n. The base case for
since by (10) no operations are applied to an empty diagram list which
results in [ ]. We consider a step case of induction.
Step case:
Hypothesis: for n
Using
hence let
Using (13) and (12) notice dmap(
diagram(ell; [i])),
hence
diagram(ell; [i]).
diagram(ell; [i])
Conclusion: for
Similarly to the hypothesis, D and E are converted for n + 1.
diagram(ell; [i])
diagram(ell; [i])
9 For the brevity of presentation we take a simpler version of the schematic proof
which does not include the operation split ends.
20 Mateja Jamnik et al.
apply(proof(n); one apply(1; lcut;
diagram(ell; [i])
diagram(ell; [i])
diagram(ell; [i])
diagram(ell; [i])
(RHS of hypothesis)
diagram(ell;
diagram(ell; [i])
diagram(ell; [i]) d
diagram(ell; [i])
3.5. Arithmetic Conjecture and Diagrammatic Proof
Definition 1 makes no claims about the link between a schematic proof
and the theoremhood of a conjecture 8n We still need to
consider the possibility of a correct schematic proof of a false conjecture.
To establish that the conjecture is true when proved by a schematic
proof, an explicit algebraic link between them needs to be defined. We
establish this link via the size of diagrams. We first define the size of
a diagram, and later, in Theorem 2, we state the theorem about the
algebraic correctness of a schematic proof for a given conjecture.
Let us denote the size of the diagram D by j D j. here is a definition
for the size of a diagram:
DEFINITION 2 (Size of Diagrams).
The size of a list of diagrams is equal to the value of the arithmetic
expression that it represents: if dmap(e; D) then j D
Note that the type of j j is: object list ! pnat. Using the property of
size defined in Definition 2 on formulae from (10) to (13), we have the
On Automating Diagrammatic Proofs of Arithmetic Arguments 21
Apart from being diagrammatically correct, we want every schematic
proof to be algebraically correct as well. A schematic proof is algebraically
correct if the sizes of the diagrams representing both sides of
the proposition after the operations of the schematic proof have been
applied are the same. Theorem 2 states the property of algebraic correctness
for any schematic proof.
of Schematic Proofs).
For all instances of a schematic proof P and for all pairs of lists of
diagrams D and E, a schematic proof P is algebraically correct if and
only if
apply
The proof of Theorem 2 is straightforward by appealing to the properties
of diagram size invariance under applications of multiple opera-
tions. The lemmas about these properties and the proof of Theorem 2
are not given here, but can be found in (Jamnik, 1998).
There is one last theorem needed in the formalisation of diagrammatic
theory which will allow us to prove theorems of arithmetic using
diagrammatic proofs. We state in Theorem 3 the property about the
diagrammatic provability of arithmetic arguments.
THEOREM 3 (Diagrammatic Provability of Arithmetic Conjecture).
A conjecture 8n diagrammatically provable if and
only if for all n there exist two lists of diagrams D and E such that
dmap(L(n); D) and dmap(R(n); E), and
The proof of Theorem 3 is trivial by the definition of size of a list of
diagrams given in Definition 2.
3.5.1. Diagrammatic Provability for an Example
We consider now an example of an arithmetic conjecture and prove it
diagrammatically using a schematic proof that Diamond extracts. Let
the arithmetic conjecture be
22 Mateja Jamnik et al.
and the schematic proof proof that Diamond extracted be as defined
in (14) and (15). here are the reasoning steps of the proof:
1. Appealing to Theorem 3 we can discharge the conjecture by:
using (11) notice dmap(n 2 ; [diagram(square; [n])]), hence let
using (13) and (12) notice dmap(
diagram(ell; [i])),
hence
diagram(ell; [i]),
and proving for all n
diagram(ell; [i])
2. Appealing to Theorem 2 and proof(n) that Diamond extracted, we can
discharge the expression in (20) by proving for all n
apply (proof(n); [diagram(square; [n])]) d
diagram(ell; [i]) (21)
3. Finally, notice that we already proved (21) in x3.4.7.
4. Results and Further Work
Diamond is implemented in Standard ML of New Jersey, Version 109. 10
The code is available upon request to the first author.
The entire process of interactive construction of proofs, automatic
abstraction from example proofs, and automatic verification of schematic
proofs in the theory of diagrams have been implemented in Dia-
mond. In the evaluation of Diamond we distinguished between a development
and a test set of theorems which we proved using Diamond.
The development set of theorems included three theorems: the sum
of odd naturals, i.e.,
the sum of all naturals, i.e.,
i\Gamma0 i, and an odd triangular sum, i.e., T ri
3T ri n , where T ri i is an i-th triangular number (Nelsen, 1993). The
Standard ML of New Jersey (SML/NJ) is a compiler and programming environment
for the Standard ML programming language. SML/NJ is publicly available via
the internet on the following site: http://cm.bell-labs.com/cm/cs/what/smlnj/-
index.html
On Automating Diagrammatic Proofs of Arithmetic Arguments 23
test set included twenty six theorems. Some proofs of these theorems
are reported more elaborately in (Jamnik, 1998). All of these theorems
contribute to the significant range and depth of theorems proved using
Diamond. For more information, the reader is referred to (Jamnik,
1998).
We want to relax the restriction currently imposed on the formulation
of example proofs. Our abstraction mechanism can deal with a
linear sequence of operations. This sequence is in fact a linearisation of
some partially ordered sequence of operation. We want an abstraction
mechanism which would be sensitive to partially ordered sequences of
operations.
There is also a possibility of allowing non-linear dependency functions
in general schematic proofs: e.g. exponential or polynomial function

Some recognition and generalisation of diagrams using abstractions
could be an interesting issue to consider. This requires some formalisation
of abstractions (e.g. ellipsis) in diagrams.
There is a possibility to extend Diamond's problem domain from
natural number arithmetic to geometry or even further to a different
field such as hardware verification. Extending our problem domain to
geometry would enable us to prove theorems of Category 1 which are
usually geometric theorems of continuous space. These do not require
induction, hence there would be no need for Diamond's abstraction
mechanism. The generality is embedded in the use of continuous space
and diagrams of general magnitude. The existing operations and the
formalisation of schematic proofs can be used. Additional operations for
moving diagrams in various directions would need to be implemented.
For more information on the possible extension of Diamond to other
problem domains, see (Jamnik, 1998).
Diamond is an interactive proof checker. A long term goal is to
design an automated theorem prover capable of discovering diagrammatic
proofs.
5. Related Work
Several diagrammatic systems such as the Geometry Machine (Gel-
ernter, 1963), Diagram Configuration model (Koedinger & Anderson,
1990), GROVER (Barker-Plummer & Bailin, 1997), and Hyperproof
(Barwise & Etchemendy, 1991) have been implemented in the past and
are of relevance to our system. Additional information about issues in
reasoning with diagrams can be found in (Chandrasekaran et al, 1995)
which is a good reference for demonstrating how extensive and important
this field is.
Mateja Jamnik et al.
One of the first systems to use a diagram in proving theorems was
Gelernter's Geometry Machine (Gelernter, 1963). The diagram in the
geometry machine has two roles. Its negative role is to reject hypotheses
(subgoals) that are not true in the diagram. In this way the search space
is pruned. The positive role of the diagram is to shorten the inference
paths by assuming various facts that are obvious in the diagram as
true.
(Koedinger & Anderson, 1990) implemented a geometry problem
solver called the Diagram Configuration (DC) model. The key feature
of the system is that it organises its data in perceptual chunks, called
diagram configurations. These are analogical to key features of diagrams
that humans recognise when they inspect a diagram. Therefore,
during the process of generating a solution path, DC infers the key
steps first, and ignores along the way the less important features of the
diagram, i.e., the less important inference steps.
"&"/GROVER, developed by (Barker-Plummer & Bailin, 1997) is
an automated reasoning system which uses information from a diagram
to guide proof search. Its problem domain are theorems of well founded
relations. It consists of the "&" automated theorem prover, based on
the sequent calculus for Zermelo set theory, and GROVER, which is
the diagram interpreting component of the system. It passes information
extracted from the diagram and translated into logical formulae
in the language of "&" to the "&" theorem prover. These formulae are
then used as additional hypotheses to the main proof of the conjecture.
GROVER considers only subgoals that are known to be true in the
diagram.
The main common feature of these three systems is their use of dia-
grams. The diagram is used to model algebraic statements, and the
system uses these models for heuristic guidance while searching for an
algebraic proof. Thus, the basic underlying reasoning process is non-
diagrammatic. In contrast, proofs in Diamond are explicitly constructed
by operations on diagrams, thus the inference steps of the proof are
entirely diagrammatic.
Perhaps a more closely related system to Diamond is Hyperproof
(Barwise & Etchemendy, 1991). Hyperproof reasons about the blocks
world. It is an educational tool to teach principles of logic reasoning and
proof construction. Hyperproof is an interactive tool for proof checking,
as opposed to an automated theorem prover. It is a heterogeneous logic
system, because it models inferencing between different kinds of rep-
resentation. Unlike traditional systems for first-order logic, which use
sentential representation, Hyperproof uses sentential and diagrammatic
(graphical) representation. It uses a diagram for a concise representation
of a complex system aiming to aid human reasoning. The user
On Automating Diagrammatic Proofs of Arithmetic Arguments 25
can take advantage either of conventional sentential inference rules or
diagrammatic inference rules. It differs from Diamond in that Hyper-
proof's diagrammatic inference rules deduce from a diagram to a sentential
formula or vice versa. It does not have diagrammatic inference
rules between two diagrams, as it is the case in Diamond. Moreover,
in Hyperproof the sentential inference rules (as well as diagrammatic
description of a situation) are essential to construct a proof.
Closer to our work is work done by Siani Baker (Baker et al, 1992)
described in x2.4 on constructive !-rule, whereby she exploits the uniform
structure of inductive proofs to abstract from example proofs.
The main difference between Baker's work and ours is the problem
domain. Baker implemented the use of constructive !-rule for proving
theorems. Our domain, on the other hand, is diagrammatic
theorems. Furthermore, Baker's motivation was to use schematic proofs
for theorems that require a cut rule in the inductive proof, otherwise
the proof cannot be carried out automatically. Schematic proofs avoid
the need for a cut rule. On the other hand, we use the constructive
!-rule in order to justify the automatic provision of general arguments
about theorems and their proofs from particular instances.
6. Conclusion
One of the aims in the research reported here is to see whether it is
possible to automate the use of diagrams in formal proofs. The hope
is that automating the 'informal' diagrammatic reasoning of humans
will shed light on the issues of formality, informality, rigour and 'intuit-
ive' understanding of the correctness of diagrammatic proofs. We have
made good progress in exploring this important and difficult area. In
particular, we have an explicit handle on abstraction. We showed that
diagrams can be used for formal proofs. We presented, as an example, a
diagrammatic reasoning system, Diamond, which supports interactive
construction of diagrammatic proofs. Diamond applies diagrammatic
reasoning to problem solving in mathematics. The user proves concrete
examples of a theorem, and the system automatically abstracts these
instances to give a general schematic proof which we hope holds for
all n. In Diamond we have the logical machinery (meta-theory, constructive
!-rule) to subsequently justify that the schematic proof does
indeed prove the original theorem.

Acknowledgements

The research reported in this paper was supported by an Artificial Intelligence
Department Studentship, from the University of Edinburgh,
26 Mateja Jamnik et al.
and a Slovenian Scientific Foundation supplementary studentship for
the first author, and by EPSRC grant GR/L/11724 for the other two
authors.



--R

On the use of the constructive omega rule within automated deduction.
Visual information and valid reasoning.
In Zimmerman

Realization of a geometry theorem-proving machine
Logic and visual information.
Automation of diagrammatic reasoning.
In Pollack
Also available from Edinburgh as DAI Research Paper No.
Automating diagrammatic proofs of arithmetic arguments.
Forthcoming PhD thesis.
"Diagrammatic Reasoning: Cognitive and Computational Perspectives"
"Diagrammatic Reasoning: Cognitive and Computational Perspectives"
Proofs Without Words: Exercises in Visual Thinking.
How to solve it.
Mathematical discovery.
The Logical Status of Diagrams.
The Sciences of the Artificial.
Conceptual Structures: Information Processing in Mind and Machine.
A cognitive theory of graphical and linguistic reasoning: Logic and implementation.
--TR

--CTR
Oliver Lemon , Maarten De Rijke , Atsushi Shimojima, Editorial: Efficacy of Diagrammatic Reasoning, Journal of Logic, Language and Information, v.8 n.3, p.265-271, July 1999
automated reasoning;theorem proving;diagrammatic reasoning