Inductive Reasoning in Mathematics

1. Introduction

We begin a study of inductive reasoning in mathematics. Inductive reasoning in mathematics differs from inductive reasoning in the empirical sciences in that there is an ultimate test although not necessarily a decision procedure, which can be used to determine what is a correct induction. Namely, that if what is induced is true, that is: if it can be deduced by one's deductive system then it must be correct. Because of this relation­ ship between induction and deduction one of our goals is to classify what instances of reasoning are inductive and what are deductive.

Our main goal however, is to create a taxonomy of feasible inductive methods. Such a goal is not unrelated to the work of the mathematician: � . Poly~ [1967, 1968A, 1968B], it is just more detailed. ln particular, we try to carry out the analysis of each method to a level detailed enough so as to be programmed. Also, where necessary, we relate the inductive methods to the level and capabilities of contemporary deductive systems. Due to this re­ quirement for detail we shall restrict our atten­ tion t o a particular, but significant domain.

1.1 Our Problem Domain

We consider the problem of trying to find by inductive reasoning a closed-form solution, that is an algebraic solution, to a recursive function. That is, from a set K of equations of the form*: ~k(n,fn,f(n-h) ,f(n-2h) .·. )=O or rather :

fn = ~ (n,f(n-h),f(n-2h), .·. ) we wis~ to find an equation of the form:

Vn fn = ~n where f does not occur in ~·

For example, given the recursive equation for the Fibonacci function:

F(n+2) = F(n+l)+Fn

Fl = 1

FO = 0

We would like to find a theorem of the form: Vn Fn = ~n

where ~n is a sentence constructed from algebraic symbols such as numerals, plus (+), times (*),

power (t), minus (-),division {/), logarithm (ln), and Sten-Ake Tarnlund Dept. of Information Processing & Computer Science University of Stockholm, Royal Institute of Technology, Sweden.

* Our convention for parenthesizing complex sub­ expressions is to place the left parenthesis be­ fore the function symbol as is done in EVAL-LISP. Thus we write (F n) and (a+ b) not F(n) and

(a) + (b).

s ine (sin) and cosine (cos) .

Or as another example, given the recursive equations for the minimum number of moves that must be made in the Tower of Hanoi puzzle of n discs (a description of this puzzle may be found in Luger [1976].)

H(n+l) = 2(Hn)+l

HO = 0

we would like to find a closed form solution: Vn Hn = ~n.

1. 2 A de£init.ion of "Inductive Reasoning"

0£ course if we, or rather our program al­ ready "knew" a closed form solution ~n for a re­ cursive £unction such as F or H then we would not want to call the method by which that ~n was pro­ duced: "intluctive reasoning". The problem then o£ defining just which methods of producing ~n are examples of inductive reasoning, and which are not - resides in the question as to what it means for a system to "know" something. For example if the system had;

Vn Hn = ~n

explicitly stored as an axiom we would clearly say that the system knew that Vn Hn = ~n. Further­ more, i£ the system could apply a sequence of items (i.e. axioms, lemmas, axiom schemas and lemma schemas, written say in LISP) which transformed Hn into ~n, then if the system knew that each applic­ ation of an item in that sequence produced a cor­ rect result, then again we would say that the system knew that (Vn Hn = ~n).

So far this is an omnipotent sense of knowledge: We know whatever is deducible. We would like to modify it by the further requirement o£ feasibility. That is, any sequence of application of items must not be so long as to exhaust the system's resources or our patience. In regard to feasibility, it is pointed out that we don't strictly speaking have to "know" that each application o£ an item is cor­ rect, (for after all, proofs from axioms only are very long), but rather all that is needed is the possibility of "knowing" that our items are correct in the sense of an extensible deductive system (Brown [l976A]), coupled with the "belief"* that our items are correct in at least the sense of never having been refuted (i.e. shown to be incorrect) (Popper [1968] ) ·

In summary then we will call any method of producing a closed-form solution ~n, which is not "known" to be the closed-form solution, inductive reasoning. For example, enumeration of all poss­ ible algebraic functions or random guessing would count as inductive reasoning (albeit poor inductive reasoning) because as items of a deductive system they would quickly be refuted by producing false results.

*We speak o£ "knowledge" as true "belie£". The point is that although we hope that our deductive system is sound, there does not seem to be anyway to absolutely guarantee this fact.

2. Elementary Inductive Methods

we first describe two basic methods of in­ ductive reasoning, and then compare them.

2.1 The Method of Generalization with Beliefs

One popular theory of inductive reasoning (Meltzer [1969], Plotkin[l969, 197l],Popplestone [1969], Feldman[l969], Hardy[l976]) suggests that it is basically generalization.* Consider for example the Tower of Hanoi problem. Using the recursive equations we can deduce closed-form solu­ tions for numerical instances of Hn.

HO 0

Hl HO+l = 2·0+1 = 1

H2 2Hl+l 2·1+1 3

H3 2H2+1 2·3+1 = 7

H4 2H3+1 2·7+1 = 15

H5 2H4+1 2·15+1 = 31

H6 2H5+1 2·31+1 = 63

I suspect the reader has already induced a closed­ form solution for Hn, but let us investigate how this might be done. From

HO=O Hl=l H2=3 H3=7 H4=15 H5=31 H6=63

we wish to find**

_ First let us note that a least general generalixation method such as Plotkin [1969,1971] does not work because the least general generalization:

Furthermore,even if we include an algebraic matching facility similar to that used in Feldman [1969] and Hardy [1976]***which allows us to try to relate the arguments of the Hn function to its val­ ues by adding,multiplying,subtracting,and dividing, we still would not obtain a solution. For example, adding one to the sequence of values of Hn gives:

HO+l=l Hl+l=2 H2+1=4 H3+1=8 H4+1=16 H5+1=32 H6+1=64

But still the remaining least general generalization is false.

So how can the closed form solution be induced? Let us suppose that the inductive system has avail­ able a belief that any function which produces the sequence of values 1, 2, 4, 8, 16, 32, for the arguments O, 1, 2, 3, 4, 5, is probably equal to the exponential function of base 2:

(Belief 1, 2, 4, 8, 16, 32 is probably 2n) Then given this belief a system might try to com­ pare the sequence 1, 2, 4, 8, 16, 32 to the se­ quence of values given by the recursive function by applying various algebraic operations pairwise * We consider analogy to be an essential component of the method of generalization as here described, and hence do not define a separate: method of analogy.

** V is our symbol for all .

*** In our case, however, we work directly on the numbers themselves rather than applying algebraic operations to the number of occurrences of symbols such as: the successor symbol.

to the elements of each sequence. For example,in the case of Hn we might subtract from each element of the belief sequence, the corresponding element generated by Hn, obtaining

a sequence of ones. ledge ohat This would give us the know-

HO = 2 1 - 1

and via our belief, we induce that: Hn = 2n - 1

which in fact is true.

There is, however, another inductive method which, other than for possibly the triggering of the belief that the closed form solution might in­ volve an expenential function of base 2, does not really need to produce those instances of the Hn function. Nor does it need to go through any generalization steps. We call this method, the Method of Successive Refinement.

2.2 The Method of Successive Refinement

The basic idea of the Method of Success Re­ finement is to make an initial (incorrect) guess as to what is the closed form solution, let a theorem prover try to prove this guess, and when it fails to prove it, go back and try to modify each branch of the protocol on which a had been produced , For example, let us suppose that we believe a solution to Hn might involve an exponent­ ial function to a power of two :

(Belief Hn involves 2n)

In other words, let us first form the hypothesis that:

and see what expression. a deductive system Inducting on n we will do to this get*:

Already we are in trouble as the deductive system shows that our hypothesis is false, on the base case. Can we modify our hypothesis to induce a better one? Analysing our proof we see that if the expression o = 1 were replaced by 0 = 1 - 1, then ll and not a would be produced. This means that HO 1 0 would have to be HO = 1 0 1, HO = 2n would have to be HO = 2n - 1, and Hn = 2 would have to be hn = 2 - 1 . Giving our new hypothesis to a deductive system we get:

* · is our symbol for true; a is our symbol for false, and + is our symbol for implication. The left branch is the base of the induction, and the right branch is the induction step.

which we deduce to be true.

·

we see then that we can obtain a proof by mod­ ifying a previous unsuccessful attempt at proving a theorem. This leads naturally to the question as to what is the space of all such modifications? Although, potentially this space may be quite large, we will only consider two simple modifications:

1. addition of a constant to an equation in order to make it true
2. multiplication of a constant to an additive part of an equation in order to make it true.

We have just seen an example of (1) in obtaining a solution to the Hanoi function. An example of (2) applied to the false equation

1 = Is would be to multiply Is by 1/IS and an example of (2) applied to an additive part of the false equation o = 1 + Is

would be to multiply the additive part 1 by - 1/IS Note that modifications are only made to the right hand side of an equation. The reason for this is that that side contains the closed-form solution whereas the other side merely contains the recursive function.

The reader will see in the method of success­ ive refinement an' echo of Meltzer's [1969] hypo­ thesis that inductive reasoning is inverse deduc­ tion. But in our case, this is not so much a semantical hypothesis: if A+B then A may be in­ duced from B, as it is a notion of search strategy in the sense that if B is deduced from A by apply­ ing the item* A ++ B to A, then A is induced from B by applying the item in the opposite direction.

We have seen how the closed-form solution for Hn may be obtained from the belief that the solu­ tion involves an exponential function of base two. Note that this belief is stronger than what is necessary, and that the belief that some arbitrary exponential function a is involved suffices: That is, if 2 is replaced by a ·in the previous protocols, essentially the same result will be obtained.

2.3 Comparison of the two Methods

So far, we have found that simple generaliza­ tion methods are not sufficient and that sophisti­ cated beliefs seem to be used in inductive reason­ ing. We have cast doubt on the suggestion that inductive reasoning is only generalization by de­ scribing another technique, the method of success­ ive refinement, which seems to be more powerful (because it needs a weaker belief to produce the solution).

One advantage of the generalization method is the possibility of triggering the 2n belief by an algebraic matching of the 1, 2, 4, 8, 16, 32, se­ quence to the sequence generated by the Hanoi function : Hn. A second advantage is that it is * ++ .is .our symbol for iff ~f and only if).

quite easy to explain how the belief, that a func­ tion whose initial instances are 1, 2, 4, 8, 16, 32, is the exponential of base 2:

(Belief 1, 2, 4, 8, 16, 32 is probably 2n) was produced by simply instantiating n in 2n to successively 0, 1, 2, 3, 4, S whereas it does not seem quite as easy to explain the production of the initial hypothesis that Hn involved some ex­ ponential function:

(Belief Hn involves an)

Are we for example to believe that the closed-form solution of every recursive function involves an exponential function or what?

Although it is easier to explain the origins of a belief of the form:

(Belief 1, 2, 4, 8, 16, 32 is probably 2nl than of the form:

(Belief Hn involves an)

we note that if a recursive function is not actu­ ally equal to a simple algebraic function such as 2n then it is quite improbable that the necessary belief of this first form could be available to be used in obtaining the closed-form solution. we will now give an example of such a function and suggest that the closed-form solutions of most re­ cursive functions are of this character. This example is interesting because it supports the view that inductive reasoning based only on the method of generalization even with sophisticated beliefs, is not sufficient, and that other methods are also needed.

Our example is the Fibonacci function. its recursive equations we deduce: Using

FO 0

Fl 1

F2 Fl + FO 1 + 0 1

F3 F2 + Fl 1 + 1 2

F4 F3 + F2 2 + 1 3

FS F4 + F3 3 + 2 s

F6 FS + F4 s + 3 8

F7 F6 + FS 8 + s 13

Thus from

FO=O Fl=l F2=1 F3=2 F4=3 we wish to find: FS=S F6=8 F7=13

Fn = ?

But there is no simple algebraic function which produces an initial sequence anything like 0, 1,1, 2, 3, S, 8, 13. In other words there could not be any belief of the form:

which would be helpful in solving this problem. For after all we cannot expect to have beliefs about every algebraic function in our system; only the simple ones. We can see that the closed-form solution is not simple, by actually exhibiting it. Concurrently we will take the opportunity to show how this closed-form solution could be obtained by the method of successive refinement using the belief that the solution involves two exponential functions:

(Belief Fn involves an, bn) where a # 0 can b # 0.

From this belief we form an initial hypothesis that:

Fn = an + bn

and see what our deductive system will do to this expression. Inducting on n twice, because Fn does not recurse on Fn+l, we obtain:

The two base induction step seems to be true, cases are false. Can we modify thesis to induce a better one? but our the hypo-

·

Analysing the Fl base case we see that if the Is in (1 = Is> had been 'divided by Is then W would have been produced. This means that the base case would have haS to have looked something like: Fl=aFO+((b-a)/IS)b Fl=a·O+((b-a)/IS)·l Fl=O+(b-a)/IS Fl=(b-a)/IS 1= (b-a)/IS 1= ((1-/S)/2-(l+IS)/2)/IS 1= 2/S/2/S 1=1 ll Working upwards we see that the five previous lines in the oroof must have been something like.:

* In contemporary deductive systems (Brown [1976B, 1977], Boyer [197S]) the equality or unification items would end up replacing all occurrences of say "a" by b-1. A system used in successive refine­ ment should not do this because if Fn = an + bn is false a might not equal b - 1, and then we would not want to propagate this falsity into the branch of the proof which is the induction step which may after all be true as in this example. The reason we prefer to have a derived on the branch of the proof which is the induction base rather than the induction step is that it is a simpler branch and will be easier to analyse why it produced a, in order to induce a hypothesis.

·

?

So far we have been able to induce a new hypothesis which will probably make the Fl-base branch of the proof result in a. But, does this change the re­ sult of u we had previously obtained in the in­ duction step branch of the proof? Since induct­ ing onF(n+l)"=aFn+(b-a)/IS- bn gives :

Fn+l=aFn+ (b-a) ;/s b n+Fn+2=aFn+l+ (b-a) ; / s bn+l (b-a)//S bn=Fn+l-Fn +Fn+2=aFn+l+(b-a)/IS bn b

Fn+2=aFn+l+(Fn+l-aFn)b

and since the third line is identical to our prev­ -ious third line we see that the induction step branch of our proof will still result in W.

Of course we don't actually have to analyse our proofsteps downward, as we could simply apply our deductive system to such a step and see what it does. For example, to see that Fn+l = aFn +( (b-a)/1 S)bn results in · all we need do is to apply our deductive system to it.

We have now produced a modification which re­ sults in · on both the Fl base, and induction step branches of our proof. Only the FO base step re­ mains. The FO base branch resulted in c, so we know that some sort of modification is what was needed to make the FO base branch result in a: We first check to see if the modification induced from the Fl base branch will suffice to make this branch result in ll:

ll

So there is still a problem. If, however, 0 = 1 + 1//S were 0 = 1//S - 1//S then 0 = 0, · would have been deduced. For this to be the case FO=l+l/IS would have to be FO=l/IS - 1/IS FO=a 0 +b 0 / I S would have to be FO=a 0 ;/s - b 0 /IS and finally:

Fn=(an-bn)/.'S would have to be and then our deductive system would easily be able to deduce that this new hypothesis :

is true.

Replacing a and b by the algebraic terms that we have found them to be in our proof we find that the closed form solution for the Fibonacci func­ tion is:

Thus we see that although it is plausible that we might be able to induce this solution by the in­ ductive method of successive refinement, it is not very plausible that we could have induced this solution by the generalization method. The reason for this, as will be recalled, is because the gen­ eralization method would require prior beliefs that:

And it simply does not seem plausible that such beliefs would be available.

2.4 The Supplementary Method of Existential Functions

We have one final point to make about the Fibonacci example: If we had a slightly more sophisticated belief as to what the closed-form solution might be, then our deductive system would be able to obtain the solution in a very direct manner. Let us suppose that we have the belief that the closed-form solution of the Fibonacci in­ volves a linear combination of two non-zero func­ tions:

(Belief Fn involves a an + Sbn)

Then the hypothesis is: jajS3a3b Vn Fn = aan+Sbn A solution is obtained by inducting twice on n:

-

n

·

j F(n+l)=aFn+(b-a)Sb +F(n+2)=aF(n+l)+(b-a)Sbn

~

. (b-a) Sbn=F (n+l) -aFn+F (n+2) =aF (n+l)+ (b-a) Sbnb

t

Fl+aFO+ (b-a)BbO

Fl=a·O+(b-a)S·l

Fl=O+(b-a)S

Fl=(b-a)S

l=(b-a)S

s~

b-a

I s~--=-1--\

\ i-ls - 1+ls ;

/,

-2- -2- :

2 -,

tf3= ""Us )

F(n+2)=aF(n+l)+F(n+l)-aFn)b

F(n+2)=aF(n+l)+bF(n+l)-abFn

F(n+2)=(a+b)F(n+l)-abFn

F(n+l)+Fn=(a+b)F(n+l)-abFn

(a+b-l)F(n+l)-(a·b+l)Fn=O

a+b-1=0 1\ a·b+l=O

a+b-1=0

"/,._____ .

a·b+l=O

a =1-b .. ·> (1-b) ·b~

( l+IS ':

·

\a=---:;:---:

2

b2b +1=0

b -b-1=0

1-ls

b~---

· 2

This technique of using existential functions has been used by Bibel [1976] (in our case constants: a,b,a,B),Because it is so powerful that we shall raise it to the status of a third inductive method which we shall call: The supplementary method of existential functions. It should be noted that this technique is no substitute for the more gen­ eral method of successive refinement, for its power depends on knowledge possessed by the deductive system. In the protocols using the method of existential functions we have assumed the ability to solve equations of the form:

cj> f = 0

for an arbitrary existential constant. This. knowledge was not assumed when not using this method. We shall see more of this method in sec­ tion 3.

2.S summary

In summary then we have described two basic inductive methods and one supplementary method; and have shown that the effectiveness of each method depends on the availability of particular beliefs. We have suggested that the beliefs needed by the generalization method would only be available if the recursive function is equal to some very simple algebraic function, such as is the case with the Tower of Hanoi function. For most other recursive functions such as the Fibonacci functions we have suggested that the beliefs needed by the generaliz­ ation method would not be available.

In section 3 we describe how the beliefs need­ ed by the method of successive refinement might be automatically produced.

3. Temporal Inductive Methods

We now describe methods of inductive reasoning based on information obtained from the solutions of previously solved problems. Such methods are call­ ed temporal inductive methods. There are two temporal inductive methods, distinguished by the type of information on which they are based. The first temporal method is based solely on informa­ tion obtained from the theorem which expresses a previously solved problem, whereas the second temporal method is based on information obtained from the proof of a previously solved problem.

Referring back to section 2.S we shall see in section 3.2 how the second temporal method may be applied to producing the kind of beliefs needed by the method of successive refinement.

3.1 The Temporal Method based on Theorems

The basic idea of the temporal method based on theorems is for any given problem F to try to find a similar problem H which has already been solved, and then to use something similar to the solution for Has a hypothesis for the solution of F.

For example let H be the Tower of Hanoi prob­ lem whose solution we discovered in Section 2, and let F be the Fibonacci function whose solution we are trying to find. The theorem which expresses the solution to the Hanoi problem is then: (Vn H(n+l)=2(Hn)+lAH0=0) + Hn=2n-l

and the (as yet incomplete) theorem which expresses the Fibonacci problem is then: (\fnF (n+2) =F (n+l) +Fn /\Fl=l/\ FO=O) + Fn=? we now try to compare these two theorems in order to produce a guess as to what ? should be: (Vn H(n+l)=2Hn + 1 1\ HO = 0)+ Hn=2n-l Vm F(m+2)=F(m+l) + Fm ' Fl = 1 !. FO = 0 + Fm =?

We see that there is no reasonable analogy that we can make which will help us to solve F. For ex­ ample, if we form the analogy that m is n - 1 from (Hn+iL 1 Fm+2), then we might conjecture that: Fm=2 -1

which is false. In any case, so much syntax has been left unexplained by this analogy (for example the 2· , +1, HO = 0, +Fm, and Fl = 1) that we can have no confidence in this conjecture anyway.

Furthermore even if our generalization system were sophisticated enough to rewrite the H theorem as the equivalent theorem: n

(':fnH(n+2)=2H(n+l)+l I'.Hl=l ll HO=O) + Hn=2 -1

(VmF(m+2)=F(m+l)+Fm ; . Fl=l , , FO=O) + Fm=?

The closest analogy would still not explain the 2·, +1, and +Fm.

The problem here is that H and F are so dis­ similar that no immediate analogy can be made.

3.2 Temporal Method based on Proofs

The basic idea of the temporal method based on proofs is as follows:

1. First using the temporal method based on theor­ ems find a problem H which is similar to the prob­ lem F you are trying to solve and conjecture a solution for F.
2. Using the deductive system produce the proof of H and a protocol of F with that hypothesis.
3. Finally compare the proof with the protocol to find out why no solution was obtained, and form a new hypothesis.

Suppose, now that we are trying to find a solution to the Fibonacci function F, given that we already know the solution to the Tower of Hanoi function H. we shall use the proof of the solution qf H which is given as described in section 2.2,starting with: 3a Vn Hn = an- 1 ·

The hypotheshs for the solution of F is 1a Vn Fn = a -1

(We could throw in a few existential constants, for example: Fn = ~·an-S, but it won't make any dif­ ference at this stage.)

Using our deductive system we obtain the fol­ lowing protocol:

We now compare this protocol with the proof of Hn. We see that in both cases the induction principle was first applied. we then see that the steps in the base case of proof and protocol were the same, and that the first few steps on the induction step branch of the proof and protocol were the same. In fact we find that they differ exactly where H(n+l) is replaced by 2(Hn)+l H(n+l)=a(Hn)+a-1 F(n+l)=a(Fn)+a-1

2·H(n+~)=a(Hn)+a-l Fl=aFO+a-~

F (n+l)=a (Fn)+ac-l+F (n+2)=a.(Fn)+l+a-l

This then is the problem. On F the theorem prover inducts because it can't recurse, because F recurses on n+2 not n+l, whereas H immediately recurses to obtain a solution.

So granted that F recurses on n+2 and that the theorem proven inducts twice the question, is: why is not a solution obtained after the second induc­ tion? Let us compare the steps beginning with the second induc~ion in F to the steps in Hn: 3a 'in Hn = a - 1 3a 'in. F(n+l) = aFn+a - 1 We see that Hn involves some term "a" exponentiated by the induction variable n. Comparing Hn to Fn+l this leads us to suspect that Fn+l might also in­ volve some term exponentiated by the induction term n+l. Thus ~~ 1 would hypothesize that Fn+l involves some term b or rather than Fn involves some term bn. The reade¥ 1 should bear in mind that the hypothesis is not an for this a would clash with the bound variable a already occuring in the above Fibonacci expression. The point is that the "a" in the Hanoi expression and "a" in the Fibonacci expression are two distinct bound variables,which do not necessarily refer to the same number.

There are two other indications that Fn in­ volves a term of the form bn. Inducting on n in each case we get respectively the base cases:

Note that in the prsof of H a skolem function dis­ appears by having a replaced by 1 whereas in the protocol of F no skolem function disappears in this manner. Here taen is a second indication that a term of the form b or rather bn is needed in the Fibonacci protocol.

Finally, by comparing the induction steps of H and F we note that in H the equality item re­ placed an by an expression, whereas in F it merely replaced "a" by an expression. Here then is a third indication that Fn involves an expression of the form bn (where b is not necessarily equal to a).

Thus, for three reasons we are lead to the belief that Fn involved some term bn where b is not neces­ s arily a. We now go back and modify our original belief: that Fn involves an: (Belief Fn involves an)

to the new belief that Fn involves both an and bn: (Belief Fn involves an + bn)

And this new belief, as we have already seen in section 2.3, sufficies to find the closed-form solu­ tion to the Fibonacci function.

3.3 Summary

In summary we have described two temporal in­ ductive methods, one based on comparing the state­ ment of a problem with the statement of a similar previously solved problem, and the other based on comparing the unsuccessful attempts to solve a problem with the proof of an analogous problem. In either case we have found that inductive reasoning depends on the ability to make use of previous solu­ tions.

We have also seen how the type of belief need­ ed to apply the method of succession refinement to the Fibonacci problem might be generated.

4. Conclusion

We have investigated and described several feasible methods of inductive reasoning which are useful in the domain of solving difference equations We stress that these methods use no mathematical knowledge in terms of lemmas, strategies or rules other than that which would be available to a simple algebra theorem prover which has only the following rules*.

1. Rules to simplify algebraic expressions.
2. The logical rules needed to put formulas in conjunctive and disjunctive normal form.
3. The two equality rules:
4. (Vx x = y + ~x) ++ ~y

(3x x = y A ~x) ++ ~y

1. A mathematical induction principle.
2. Rules to equate the coefficients of various types of expressions. (This ability is needed by the method of existential functions)

Of course, if we were to allow the use of sophis­ ticated mathematical techniques we could easily solve the problems we have considered in this paper. In particular, we could implement a theorem prover based either on the rules of the finite difference calculus (Spiegel [1971], Jordan [196S]), or on the method of generating functions (Lin [1968], Bekenbach [1964], Knuth [1969], Jordan [196S]).

But this is just what we do not want to do,for this would not explain how the mathematical knowledge embedded in these techniques was actually created. In our view of mathematics, we see that this knowledge is basically created by trying to solve a number of problems using only one's general inductive abilities and the current status of one's deductive abilities. Then one generalizes and organizes the methods that one has found useful in solving these problems into some sort of deductive calculus, such as for example the theory of finite difference equations or the method of generating functions. One then adds this calculus to one's deductive abilities, henceforth making what were difficult problems quite easy, thus allowing one to try to solve problems in more difficult domains by repeating this process.

* These rules are embedded in an algebra theorem prover which one of the authors (Brown) implemented about a year ago.

Acknowledgements

we thank Professor B. Meltzer for criticizing a draft,of this paper and for arranging for Dr. Tarnlund to visit the Department of Artificial Intelligence so that we could collaborate on this research.