Analysing Mathematical Proofs (Or Reading Between the Lines)

Introduction

The problem domain we address ourselves to in this paper is equation solving. In fact we are interested in finding real valued solutions to equations involving rational, trigonometric, inverse trigonometric, exponential and logarithmic functions. In this paper we concentrate on find­ ing general solutions to single equations in a

single unknown.

A study of this domain is overdue because although the experienced human mathematician finds equation solving straightforward, no existing computer program can match his performance. Traditional theorem proving programs are inad­ equate to explain the directness (lack of search) of his solutions. The well known algorithms for polynomials (e.g. Gaussian elimination, Sturm sequences, Newton-Bairstow, etc.) are inadequate to explain his range (e.g. trigonometric, logarithmic equations, etc.). See, for instance, Martin and Fateman, 1971 p68 or Moses 1974. Neither can his solutions be regarded as part of a process of putting the equations into some normal form or of reducing their syntactic complexity. So the standard simplification packages provided by systems like REDUCE (Hearn 1967 3.3) or MACSYMA (Martin and Fateman 1971 p64) are inad­ equate to explain the success of his solutions.

In order to try to match the human mathematician's performance we analyse his solutions. This analysis reveals a system of high level descript­ ions, strategies and goals, which can be used to guide the search for a solution through an explosively large search space . These high level concepts appear to be useful not only in equation solving, but throughout elementary algebra. We believe, the methodology should prove useful throughout mathematics.

In addition elementary equation solving appears to be an especially appropr i ate domain to start with

because:

i) Many useful high level concepts are revealed in the language used by mathemati cians when they discuss equation solving, e.g., elimination of

Alan Bundy

Department of Artificial Intelligence University of Edinburgh Edinburgh, Scotland.

variables, change of variable, collecting terms, isolation, trigonometric equations, etc.

ii) Equation solving and pattern matching (unification)are very similar. Since all algebraic manipulation is made easier by having a sophisticated pattern matching package, we make life easier by studying equation solving first.

In this paper we analyse some solutions, tease out some high level strategies and discuss how these might be incorporated in a computer program. The strategies we discover are:

isolation, collection, attraction and the basic method.

In the extended version of this paper, Bundy 1975, we show how these strategies can be used to de­ rive some historically interesting general solu­ tions. We go on to analyse some solutions which cannot be explained by the above strategies and discover further strategies.

The Proposed Program

At the time of writing not all ·these ideas have been implemented in a computer program. I have no doubt that they all could be, and a student at Edinburgh, Bob Welham, has experimented with implementing some of them in the PROLOG language (see Warren 1974). However, it would be prem­ ature to invest a lot of effort in a program before the whole domain has been explored. New connect­ ions between strategies are constantly being dis­ covered, and new problems are constantly emerging, so that such programming effort might be wasted. Our current ideas about the form of the program are reproduced below:

The program will be organised around a convent­ ional theorem prover, run in proof checker mode. That is, the theorem prover will not be able to do anything unless instructed to. The strategies are the procedures which will do the instruction . The word "strategy" was adopted to describe each of these procedures because they provide the theorem prover with search strategic guidance information. · However, for some of them descript­ ions like "tactic", "method" or "algorithm" seem more appropriate. In such cases we will some­ times use the more appropriate description as a synonym for "strategy", albeit with connotations.

These strategies will examine the current equation, using high-level predicates,to decide what to do. On the basis of this examination they may call other strategies or apply individual axioms . They will also decide whether those calls were success­ ful, and what to do next. The strategies will need to exploit all the benefits of a high-level programming language, e.g., recursion, condition­ als and search. It would be convenient if this language and the theorem prover could share facilities such as search and database mechanisms. This may be possible using PROLOG, but care must be exercised in the mixing of Metalanguage and Object language concepts . For instance,we might decide to have a predicate ISVAR which is true if and only if its argument is a variable. Then ISVAR (U) would be true and ISVAR (3) false. However, we can derive ISVAR (3) from ISVAR (U) leading to a contradiction. Our solution to this problem is to regard all expressions in the object language (constants, variables, terms and formulae) as constants in the metalanguage, so that we cannot deduce ISVAR (3) from ISVAR (U). For a further discussion of these issues see, for instance, Kleene 1962 pp62-65 and p298.

The strategies will have available to them a store of laws of real number theory. We will call these laws axioms because the program will assume them true without proof. The axioms which we are planning to put in this store are listed in an appendix to Bundy 1975. These axioms are highly redundant and include many facts which would normally be regarded as theorems in a parsimonious logical system. We will reserve the words theorem and lemma for facts proved at run time. Strategies may pick which axiom to apply next, in a variety of ways, according to the context.

For instance:

1. A strategy may have the axioms useful to it earmarked at compile time.
2. iil A strategy may have only a general descript­ ion of the axioms useful to it and have to retrieve suitable axioms at run time. (This does not prevent some prior indexing).
3. iii) A suitable axiom may not be available, and the strategy may have to appeal to a theorem proving program to prove a lemma to use instead.

No suitable axioms may be found, and the strategy will have to fail. On the other hand several suitable axioms may be found and the strategy will have to conduct a short search.

No manipulation of the equation will be allowed except by the theorem prover applying an axiom to it. This idea of separating the inference system from the search strategy is due to Kowalski 1970 pl81. It has a number of advantages (see Hayes 1974, section 3). For instance:

1. Provided the theorem prover is sound, the correctness of any solution is guaranteed. This is sometimes in doubt in a more ad-hoc program.
2. ii) All the axioms can be equally accessible to all the strategies, so a new axiom need only be added once.
3. iii) The learning of new axioms and new strategies is made easier.

A Logarithmic Example

Let us consider an equation which most people will find fairly easy to solve .

Solve for X: loge(x+l) + loge(x-1) 3

To the best of my knowledge, there are no known equation solving algorithms which could solve this equation (because it i s logarithmic) . In addition, it defines a search space which al­ though modest by equation solving standards would present a considerable challenge to most Resolut­ ion (see Robinson 1965) theorem provers.

The solution we are going to analyse is given below:

Analysis will lead us to discover the strategies of attraction, collection, and isolation, which we will link up into a strategy called the basic method.

Notation

Since in what follows we shall be reading between the lines of this solution, it will be necessary to be able to refer to the spaces between the lines. We have, therefore, labelled these spaces with Roman numerals, (on the right of the solution). These spaces will be referred to as steps, e.g., step (iii) is the one from line 3 to line 4.

In problem solving, the word "solution" has two different meanings. It can mean either

1. The written protocol of the solver, as in the sentence "Hand in your solutions by Friday".
2. ii) The answer to the problem, as in the sentence "The solution of the equation is x·6".

For instance in the above solution the written protocol is the whole thing from lines 1 to 6, the answer is just line 6. Since we will need to distinguish carefully between these two concepts we use the word "solution" to mean the written protocol and we will use the word "answer" to mean the answer.

We will also need to define what syntactic forms are acceptable as answers. In equation solving, answers give values for the unknown in terms of expressions not involving the unknown. So close is this to the concept of a substitution that we have decided to make the connection between pattern matching and equation-solving more explicit and use the word "substitution" to mean those formula which are syntactically acceptable as answers.

As explained in Bundy 1974, the x in the above solution is not a variable in the predicate logic sense. If it were we would be allowed to sub­ stitute arbitary terms for it during the course of the solution and we would get solutions such as

In fact x actually behaves like a constant when we are searching for a general solution and like a variable when we are searching for a particular solution. In this paper we are concerned only with general solutions so we regard x as a con­ stant. Following Polya 1962 we distinguish it from any other constants in the equation by calling it the unknown. We reserve the letters

x,y,z for unknowns

a,b,c,d for other constants

u,v,w for (genuine) variables (in the axioms)

s,t for terms

f,g,h for function sympols

A,B,C for formulae

and E for equations

The Analysis

In this analysis, because we look only at the final solution, we are guilty of the sin of not display­ ing the search involved in discovering that sol­ ution. We will try to atone for this sin when we discuss how to implement the strategies we discover. Unfortunately it will not be possible, until the program is run, to be certain about the size of the space searched before the solution is found. However, in the conclusion we argue that this space will be a small function of the length of the solution.

We look first at the end of the solution, lines 3 to 6. In line 3, for the first time the equation contains only a single occurrence of the unknown, x. From here on the solution is straightforward. The next three steps consist of stripping away the functions surrounding this single occurrence of x until it is left isolated on the left hand side of the equation. Each step consists of identifying the outermost (or dominant) function symbol on the left-hand-side, recovering the axiom which will remove it from the left-hand-side and insert it's inverse on the right-hand-side, and then applying this axiom. We will call the strategy which guides these three steps isolation, because it isolates the single occurrence of x on the left­ hand-side. We will explain it in more detail in the isolation section. It can be regarded as the basis of nearly all work in equation solving as well as much of the rest of algebraic manipulation. As with simplification, mathematicians often omit isolation steps from their written protocols, crowding as many as three or four steps into the transition from one line to another.

We look next at line 2 :

This contains 2 occurrences of x, so isolation is not applicable. However, we can see step (ii) as preparing for isolation, by achieving a reduction in the number of occurrences of x from 2 to 1. This is done by applying the identity :

This is an example of our second strategy, which we call collection, namely, when there is more than one occurrence of the unknown, try to find an axiom which will collect occurrences together.

Finally we look at line 1 and step (i)

The two occurrences of x ·cannot be immediately collected, presumably because a suitable axiom was not stored. We can however prepare the occurr­ ences for collection by moving them closer to­ gether, so that more identities will match the term containing them both. This is what happens in step (i). The notion of "closer" is defined in the next section. The strategies of moving occurrences closer together to increase their chances of collection, we call attraction.

When the above three strategies are combined we will call the resulting equation solving strategy, the basic method.

our analysis is now as below.

Definitions

In order to explain how we might implement these strategies, we will need to have some notation to discuss algebraic expressions, especially the notion of distance between occurrences of symbols.

6.

we can represent any algebraic expression as a tree (we do not use a graph, since we want to be able to distinguish between occurrences) :

can be represented as

The distance between several occurrences of symbols in an expression is the size (number of links) of the smallest subtree in the tree which connects them all, e.g., the distance between the two occurrences of x in the example is 6 and the distance between the three integers is 8.

Any term or formula will be represented by a complete subtree. The symbol at the root of that subtree is called the dominant Symbol of that term or formula:

log is the dominant symbol of loge(x+l)

• is the dominant symbol of x+l

An occurrence of an expression is said to contain another expression if the tree of the second is a subtree of the tree of the first:

An occurrence of a symbol is said to dominate an expression (¢ say) if the symbol is the dominant symbol of an expression which contains¢:

log dominates x+l, e, and 1 in loge(x+l)

Isolation

we now consider the four strategies in more detail in order to see how they might be implemented.

If we have an equation, E, containing a single occurrence of the unknown x then we can apply isolation. For the sake of argument suppose x occurs on the left-hand- side of E and that the dominant function symbol on the left-hand-side is the n-ary symbol f, i.e., E is of the form

where s . (say) is the only term containing x. The isolation process is to first isolate si, and then to call isolation recursively to complete the isolation of x . To isolate si we need an axiom of the form

where A is some substitution for u . in terms of the uj, jji and v. A is often of~the form

But this is not always the case, as the axioms for sin and squared illustrate.

We therefore define a substitution for x as follows

1. If S does not contain x, then x non-trivial substitution for x. s is a
2. ii) If A and B are non-trivial substitutions for x then AvB is a non-trivial substitution for x.
3. iii) If A(n) is a non-trivial substitution for x and S is a set of real numbers then <3n E S) ( A(n) ) is a non-trivial substitution for x.
4. iv) "True" and "False" are trivial substitutions for x.
5. A substitution for x is a trivial or non­ trivial substitution for x.

With this definition of substitution there is an axiom of the required form associated with each of the functions of elementary algebra. We might speculate that this is not an accident, that mathematicians have deliberately defined new inverse functions, (e.g.,arcsin and square root) so that these axioms would exist. About these inverse functions little is known, and this causes prob­ lems when they occur in equations we are trying to solve. How these problems are· tackled is dis­ cussed in Bundy 1975.

It should be a straightforward matter to write a procedure which can : decide whether or not there is a single occurrence of the unknown in an equat­ ion and on which side it occurs; identify the dominant symbol of that side1 recover the appro­ priate axiom; apply it and then apply isolation recursively to the resulting equation or dis­ junction of equations. The only difficulty that might arise is if the axiom was stored in the wrong form:

e.g., the sin axiom as

the right form would have to be recovered as a subgoal. We delay consideration of this problem.

Collection

Collection is the strategy which takes . an equation and tries to reduce the number of occurrences of the unknown which it contains. For the sake of clarity we will limit our discussion initially to the case when two occurrences are reduced to one. This is the most common situation and, at the cost of some complication, our discussion can easily be extended to the more general case.

Having decided which two occurrences to collect,·>'e focus our attention on the smallest expression which contains them both. If the two occurrences are on the same side of the equation this will be a term, called the containing term, otherwise it will be the whole equation. We deal with the former case first. The containing term must now be replaced by another term containing one occur­ rence of the unknown, say x, so we must look for an axiom, say A, which will do this. We can easily build up a description which A must obey.

1. A must be an identity, i.e., an expression of the form:

s 1 = s 2 or B -> s 1 precondition. s 2 , where B is called its

• ii) One of the variables, say u, must occur either :

• or (b) twice in s2 and once in sl

without loss of generality we will assume case (a).

• iii) s must match the containing term, with one of 1 its variables, say u, being instantiated to x. Note that we are not allowing u to be matched to a proper term, say t(x), contain­ ing x. This situation will be handled by making a prior change of unknown of, say y, for t(x). We are also not allowing the situation where two variables, say u and v, are both matched to x. If A(u,v) is useful to collection by matching u and v to x then A (u,u) is also useful, and therefore non­ trivial. We will assume that we will not need to do collection using A(u,v), because A(u,u) will also be present. To justify this assumption we need only make sure that all non-trivial axioms which can be gotten by identifying the variables of existing axioms are added to the axiom store.

If A obeys parts(i) and (iia) of the above description we will say that it is useful to col­ lection, left to right, relative to u. If A obeys parts (i) and (iib) we will say that it is useful to collection, right to left, relative to u-.-----

sin 2u = 2.sinu.cosu

is useful to collection, right to left, relative to u.

is useful to collection, left to right, relative to u (and v)

w~ u+v) = w.u + w.v

is useful to collection, right to left, relative to w

u+o = u

is useless to collection To find a suitable axiom the collection strategy need only search among those axioms useful to it and find one which also obeys part iii) of the description.

The case when the two occurrences of x appear on opposite sides of the equation can be dealt with in a similar way. This time we are interested in axioms of the form :

where c (or c in situation (a)) can be matched to the whole equation. We can build the appropriate definitions of "useful to collection" by replacing s 1 with c 1 ~nd s 2 with c 2 in parts (ii) and (iii) of the prevLous descriptions.

We will want to extend these definitions to deal with any reduction in the number of occurrences of the unknown. Then we can include in collection

the use of axioms like

to reduce 2 occurrences to none. The modification to the definitions is straightforward, (iia) be­ comes : u must occur more often in s 1 than in s 2 > .

Even though strategies like collection guide the search for a solution, they do not eliminate search altogether. For instance, collection has to choose:

• (a) which set of occurrences of the unknown to try to collect, (and therefore which subterm to try to replace)
• (b) which matching, useful-to-collection axiom to apply.

Our initial experience is that collection narrows the search considerably. In fact we are lucky to find a single axiom, useful for collection, which matches one of the containing terms. In the event of a real choice we could use heuristics based on the fact that we would like to reduce the number of occurrences as much as possible.

Notice that we are demanding that collection do its job with one application of an axiom. This is because we want collection either to succeed or to fail quickly, so we can try something else. We could allow it to conduct a short search, but it would be difficult to know on what grounds to terminate an unsuccessful search. The problem with keeping such a tight rein on collection is that it might fail simply because the axiom which should have succeeded was not in the right form.

It would be a pity to fail to collect x in

because the axiom were in the form

1. (u+v) . (u-v) 2 2. u -v

our solution to this problem is to have a pattern matcher which can recognise that axiom (2) matches (x+l) .(x-1). This entails building-in axioms like the commutativity of multiplication (c.f. Plotkin 1972). One aspect of this build­ ing-in process is discussed in the section on pattern matching in Bundy 1975, but a complete discussion is delayed until a later paper. Such a pattern matcher will increase the number of axioms which will match the containing term. However, we still believe that collection will be lucky to find an axiom which both matches and is useful to it.

we will want the pattern matcher to spend a large, but bounded, amount of effort to try to make an axiom match an expression. If this is not to be computationally very time-consuming, collection had better only feed good candidate axioms to the pattern matcher. It can select good candidates by :

• (a) Only choosing those "useful to collection"
• (b) Insisting that both the axiom and the expression it is to match obey the same high level description e.g., both are quadratic, trigonometric, logarith­ mic, etc.

Attraction

The attraction strategy is very similar to col­ lection. As before we must choose the occur­ rences we are going to attract, then focus on their containing term. As before we will use a definition of axioms useful to attraction to recover a sui table axiom to apply. The main difference is in the type of axioms useful to attraction.

An axiom is useful to attraction, left to right, relative to some subset of its variables, » say, if for all utu, u has the same number of occurr­ ences on left~and right, but the distance between all the occurrences is strictly smaller on the right than the left. We can make a similar definition for useful to attraction, right to left.

is useful to attraction, left to right, forfu,v}

is useful to attraction, right to left, for[u,v}

is useful to attraction, right to left, for i."u,v!

The variables in the subset ~ will each be bound to terms containing the unknown, x.

Isolation, collection and attraction can be com­ bined into a basic method for solving equations.

If the equation contains a single occurrence of the unknown we isolate this occurrence. Other­ wise we try collection on each combination of occurrences until either the number of occurrences is reduced to one, or no more collections are possible. In the first case we call isolation, in the second case we call attraction. We try attraction on one combination of occurrences. If this is successful we call collection, otherwise we try attraction on some other combination. If we run out of attractions to attempt, the method fails.

Conclusion

We have studied elementary equation solving. Existing equation-solving, computer programs, do not match either the range or the directness of the human mathematician. We have analysed such mathematician's solutions and discovered a system of high-level strategies. These strategies are not restricted in their range of application. They guide the search for a solution by

1. Providing a series of intermediate subgoals between the present equation and the final solution.
2. ii) Focusing on the subterm of the equation which is to be manipulated next.
3. iii) Selecting a small set of axioms which can be · made to apply to that subterm and which are ·relevant to achieving the next subgoal.

We claim that this guidance reduces the size of the space searched considerably and that sometimes there is no search at all.

We have discovered and investigated the strategies of isolation, collection, attraction, and the basic method. This is only a small part of the story. There are many other strategies at work in equation solving. There are general-purpose strategies like simplification, pattern-matching, change of unknown, and elimination, and there are special­ purpose strategies for well understood types of equation; like polynOMial and trigonometric equations. We delay discussion of these to another paper.

Acknowledgements

we would like to thank the many people with whom we have interacted over this work for their en­ couragement, suggestions and inspiration. It is difficult to separate the contributions of each individual. Odd remarks and suggestions have often fermented together, resulting in a product unrecognisable to the original contributors. However, we single out for special mention : Soei Tien Tan, Gordon Plotkin, Ira Goldstein, Joel Moses, Luis Pereira, Bob Welham, Alan Robinson, Woody Bledsoe, Bob Kowalski and George Luger. We apol­ ogise to the many other people we have omitted.