--- title: "Discovery and Reasoning in Mathematics" authors: - "Alan Bundy" doi: "" url: "https://ijcai.org/proceedings/1985/246" pdf: "https://ijcai.org/proceedings/1985/0246.pdf" venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence" year: 1985 pages: "1221-1229" track: "General" keywords: --- # Discovery and Reasoning in Mathematics Alan Bundy *Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 1221-1229. ## Abstract We discuss the automation of mathematical reasoning, s urveying the abilities displayed by human mathematicians and the computational techniques available for automating these abilities. We argue the importance of the simultaneaus study of tliese techniques, because problems inherent in one technique can often be solved if it is able to interact with others. ## Full text ## 1. Introducbon A major goal of artificial intelligence is to automate reasoning. Salutions to this goal will have both technological applications, enabling us to build more powerful expert systems, and scientific ap­ plications, providing models to compare with human reasoning. Mathematics is an excellent domain for exploring the automation of reasoning because: - (a) it provides a wide range of examples of reasoning, from the . simple and shallow to the complex and deep; - (b) it is poss ible to detach this reasoning from other considerations, such as sen­ sory input of data; and , - (c) to of a first approximation, the problems knowledge representation have been - solved. Compare mathematics with other AI domains in which reasoning plays a part , e.g. natural language under­ standing or visual perception. In mathematics one is not bogged down with huge amounts of noisy data, nor concerned that what seems to be a difficult reasoning issue may evaparate if the knowledge representation were changed. One is free to con­ centrate on the reasoning problems and then make an attempt to translate any solution found to other· domains. In this paper I discuss the automation of math­ ematical reasoning, by which I mean any cognitive activity that mathematicians engage in as math- 1 Thi s research was supported by SERC grant, nu11b·r GR/C/20826 . ## DISCOVERY AND REASONING IN HATHEHATICS 1 Alan Bundy Oepar·tment of Artificial Intelligence, University of Edinburgh ematicians. The main theme will be that math­ ematical reasoning consists of mor·e than just theorem proving, and that the simultaneaus automa­ tion of other reasoning processes, e.g. learning, simplifies the automation task. Each reasoning process outputs knowledge but also demands knowledge as input. If a computational technique for automating a particular reasoning p r ocess is studied in isolation then the provision of its input knowledge may prove a major barrier to automat ion. But the input knowledge of one technique is the output knowledge of another, so that the tech­ niques fit tagether in an intercommunicating net­ work. Some techniques for automated reasoning may involve search. In isolation the search involved may be computationally expensive. But one technique may be used to control the search of another, especially if the two techniques are co-routined or even merged into one. The power of a system in which the various techniques interact in well-crafted ways will be more than just the sum of the power of the par·ts. I advocate the simultaneaus study of all the the processes of mathematical reasoning with particular emphasis on the possible interactions between the techniques that automate them. ## 2. Reasoning Abilities in Mathematics What processes are involved in mathematical reasoning? In this section we discuss the various processes and the AI techniques that have been proposed to automate them. More details about these techniques can be found in [Chang l. Lee 73, Bundy 83]. The first problern we face is how to classify mathematical reasoning into different processes - what my psychology friends call defining the task ecology . Our starting point is a 'folk ecology' of reasoning processes, i.e. the terms used in pre­ scientific discussion of reasoning. We will call these mathematical abilities. With these abilities we must associate computational techniques which implement them. These techniques will form our scientific classification. But the association of abilities to techniques not a neat 1-1 mapping. We are likely to find many techniques to associate with each ability. Same abilities, e.g. learning, have so many diverse techniques associated with them that they seem highly unsuitable as scientific categories, whereas the techniques associated with some abi lities, e.g. theorem proving, all have a strong family resemblance. Some abilities require a com­ bination of techniques. Consider, for instance, anal­ ogy which requires separate techniques for finding and then using the analogy. Each of these techniques will techniques abilities. deduction require sub-techniques. Some of these may contribute to several different Consider, for instances, resolution-type techniques, which are ubiquitous. We Iist below the mathematical abilities we will be considering under the heading of mathematical reasoning and mention some of the techniques which have been used to implement these abilities. - Proving theorems: The ability that has received the most attention in the AI study of mathematical reasoning, almost to the exclusion of all others, has been theorem proving. Automated theorem proving has been an important subfield of AI throughout its history. The main techniques required to automate theorem proving are deduction which involves search control. Deduction traverses a search space of legal inference ·steps. Search control decides which of these steps to try. - Formalizing Problems: However, math­ ematicians, especially applied math­ ematicians, spend a large part of their time translating informal problern state­ ments into mathematical formulae to which deduction, etc. may be applied. The initial stages of this translation in­ volve natural language understanding, visual perception, etc but these are not specifically mathematical techniques. Later stages involve the specifically math­ ematical technique of formula extraction from the internal meaning representation, which may itself involve deduction (see section 3.5). - Learning: This term covers a multitude of processes, for instance, the learning of new mathematical theorems, the learning of new proof methods, the defining of new concepts, the conjecturing of results, etc. New theorems must be as­ similated into the theorem proving ability so that they may be used effectively in the future. The assimilation technique required will depend particularly on the search control technique being used, e.g. the new theorem will need to be Iabeiied so that it can be accessed when needed. Similarly, new proof methods must be in­ corporated into the current search con­ trol technique. This may involve a proof analysis technique to analyse new proofs and generalize them to extract control information, e.g. proof plans. Oefining new concepts can be done by indu.:tive inference from descriptions of examples and non-examples of the concept.2 Con­ jecturing of theorems can be done by considering the hypothesis of the conjec­ ture to be a concept to be defined using the above techniques. - Using Analogy: Mathematicians use analogy to suggest conjectures and new defini­ tions, and to guide proofs. All uses require analogical matehing techniques to find and apply the relationship between the target and the source of the analogy (see [Owen 85] for a survey). This is all that is required for suggesting conjec­ tures and definitions, but to use a source proof to control the search for a target proof a further proof plan ap­ plication technique is required. This is by no means an exhaustive Iist; math­ ematicians also find counterexamples, write, publish and deliver papers, teach students, read textbooks, etc. Unfortunately, we have nothing to say about these other abilities, so they are omitted. ## 3. Mathematical Reasoning Techniques In this section we classify and discuss some of . the techniques that have been developed for automating the mathematical abilities described in the last section. There is only space to discuss those we consider particularly promising. We group these techniques according to their computational purpose and mutual similarity, e.g. deduction, search control, inductive inference, etc. This provides a more scientific classification of math­ ematical reasoning processes than the Iist of math­ ematical abilities above. But even this classification is bound to be improved as we discover new tech­ niques and gain a better understanding of the ex­ isting techniques and their inter-relationships. It should therefore be regarded as both incomplete and highly preliminary. ## 3.1. Deduction The most weil known deduction technique is r·esolution, [Robinson 65]. Resolution is a rule of inference for Predicate Calculus, that is, it is a rule for deducing new logical formulae from old. To prove that a conjecture is a theorem of a mathematical theory both the axioms of the theory and the negation of the conjecture are expressed as clauses (a normal form for Predicate Calculus formulae). Resolution takes a pair of clauses and makes subparts of each identical using a matehing technique called unification. The remaining parts are combined tagether to make a new clause. Resolu­ tion applied repeatedly to the initial clauses and to their successors defines a search space of clauses. This is searched for a contradiction. lf the search is successful then the conjecture is a theorem. The representation of axioms and conjectures as logical formulae is given in the texts of math­ ematics and logic. It is in this sense that I claimed that the knowledge representation problern was solved to a first approximation. 2 Not· that inductiv· inf·r·nc· 11 not th· nM ao toath­ ··atical induction I··· ··ction 3.2 b·lowl, which ie a d·ductiv· rul· of inf·r·nc·. The resolution search space is guaranteed to con­ tain a contradiction if and only if the conjectur-e is indeed a theorem. The ' i f' part is called complete­ ness and the 'only if' part is called soundness. The snag is that if the conjecture is not a theorem then the search may never terminate. The number of new clauses generated rises exponentially, or worse, with the length of the proof. If the proof is non-trivial then either the storage capacity of the computer or the patience of the human operator is exhausted before the proof is found. This is an example of the phenomenon called the combinatorial explosion. Various refinements of or alternatives to resolu­ tion have been designed and implemented, with the aim of improving on its space and/or time efficiency without losing completeness. One of the most powerful alternative deduction techniques is the Connection Calculus, [Bibel 82]. These improvements reduce the combinatorial explosion, however, but do not conquer· it. There have also been attempts to avoid the com­ binatorial explosion by proposing radically new deductive techniques. This has sometimes ted to techniques which are efficient at proving restricted classes of theorems, e.g. rewrite rules [Huet &. Oppen 80]. It has also led to the reinvention of the wheel some researchers have rejected the logical approach, only to reinvent it tagether with the attendant problems of incompleteness and/or combinatorial explosion. Rather than reject logical deduction techniques it is necessary to augment them with heuristic tech­ niques to control the search for a proof, [Hayes 77]. Search control techniques developed have ranged from weak but generat purpose ones, e.g. evaluation functions based · on the complexity of the formulae, to powerful but special purpose ones, such as those described in the next section. For a survey see [Biedsoe 77]. ## 3.2. Search Control A number of powerful search control techniques have been developed by careful analysis of the proofs of human mathematicians to extract the un­ derlying control ideas and express them computa­ tionally. The simplest technique, called heuristic ru/es, is to add these control ideas into the mathematical for­ mulae as preconditions for their application. For instance, the LEX program, [Mitchell et al 81] , uses rewrite rules to symbolically integrate algebraic terms, e.g the rule: is used to integrate by parts. which this rule successfully where u is a variable, x, and One class of terms integrates is those dv/dx is a constant multiple of a sine or cosine. This knowledge is represented in LEX preconditions to the above rule, i .e. search control by appending where n is an integer and trig any trigonometric function Note that this precondition is too general; trig includes tan, for which the rule does not work. We discuss this problern in section 3.3 below. Note that these preconditions can get very com­ plicated since the same rule may be used success­ fully in a number of d i fferent circumstances and the precondit10n must be the disjunct of these crrcumstances. 3 Note also that the rule now con­ tains a mixture of factual and control knowledge. These complications can cause difficulties, e.g. in the automatic learning of such rules, so some researchers prefer to separate factual and control knowledge. For instance, the Boyer/Moore Theorem Prover, [Boyer &. Moore 79], represents its control knowledge as procedures for manipulating the math­ ematical formulae. This theorem prover exploits the relationship between recursion and mathematical in ­ duction to guide inductive proofs of the properties of Lisp functions. The recursive definitions of the Lisp functions are first used to symbolically evaluate the conjecture to be proved. This may fail because the conjecture contains arbitrary constants and the evaluation process requires lists with internal struc­ ture. This failure is used to guide the choice of induction scheme and variable, so that when symbolic evaluation is applied to the induction conclusion just enough structure will be available to enable the induction step to be performed. We will call this technique, recursion guidance. Note that recursion guidance involves an analysis of the conjecture and its failed proof, and the choice of an appropriate proof technique on the basis of this analysis. This analysis uses meta­ concepts4 to describe the conjecture, its proof and the proof methods, e.g. the terms induction hypothesis, induction step, etc in the Boyer/Moore Theorem Prover or trigonometric function in LEX. These meta-concepts must be discovered by study of existing proofs, introspection, etc. It is in this sense that the knowledge representation problern is only solved to a first approximation, since the num­ ber of possible meta-concepts is open ended and the choice of appropriate ones determines the suc­ cess or failure of the technique. 30r an additional rul· uaed for each circu.atance. 4 Th· ter· · Mta Ia u .. d becauee the concepta in quut1on ducribe the repruentat1on of the problem, i ··· they are about it rather than of it. This process of analysis and guidance using meta­ concepts is itself a reasoning process and can be conveniently represented as deduction - but deduc­ tion in a meta-theory, rather than the theory it­ self. Such a use of deduction to guide deduction is made explicit in the PRESS system, [Bundy ~ Wel­ nam 61], for solving equations. The PRESS meta­ concepts describe the equation to be solved, e.g. the number of unknowns, their distance apart, the kind of functions involved, etc, and they describe various methods of solving equations or of acnieving useful subgoals, e.g. reducing the number of un­ knowns, moving them closer together, making them occur within identical subterms, etc. Deduction with these meta-concepts induces an implicit, but highly controlled, search for the solution to an equation. We call this technique, meta-level in­ ference5 (see figure 3-1). ![Image](https://ijcai.org/proceedings/1985/fulltext/246/image_000000_1a6547215470b6d0076be6f0dec054685457b81138da7405b0aae91c0655860d.png) These meta-concepts can also be used to express proof plans, e.g. the plan to move two unknowns closer together, then merge them and then isolate the remaining occurrence. This plan might be provided by the programmer or learnt by pr·oof analysis of a worked example (see section 3.3). Al­ ternatively the proof plan may be at the object­ level, e.g. the proof of an analogaus theorem, or a generalized proof, [Piummer ~ Bundy 84]. In each case it must tnen be applied by a proof plan application technique. This application might be Straightforward - the target proof exactly following the plan - or the plan may need to be relaxed or augmented at various points. A variety of tech­ niques have been suggested for realising such a flexible plan application technique (see, e.g. [Silver 64]) ## 3.3. Proof Analysis The process of constructing and augmenting powerful search control techniques, by adding meta­ knowledge gained from analysing proofs, can itself be automated. This analysis will depend crucially an the search control technique in question. For in­ stance, in tne case of the PRESS system, described in section 3.2. the solution to an equation must be analysed using tne meta-concepts of PRESS. For each step an account must be given of not only what algebraic identity was applied but also wny it was applied and how this reason fitted into the overall proof plan. For instance, sin u.cos u = 1 /2.sin 2u was applied to reduce the occurrences of u from 2 to 1 in order that that single occurrence could be isolated an tne left hand side of the equation. This kind of analysis is performed by the LP program, [Silver 64], which was able to learn new methods of equation solving and extend tne range of problems that PRESS could solve. The technique used by LP is called Precondition Analysis because it discovers new methods by considering how un­ explained steps establish the preconditions . of suc­ cessive steps. 5 tn centrast to the deduction of the ~quation aolution. which is called object-level inference. In the case of the LFX program for symbolic integration (also described in section 3.:?) the tech­ nique of back propagation was developed to analyse successful solutions and extract the control infor­ mation. This technique was incorporated in the LEX2 program, [Mitchell et al 63]. In back propagation the successful sequence of rewrite rules was applied in reverse order to a generalized answer to see what constraints this would impose an the original problem. These constraints then became the ~recon­ ditions of the first rule of the sequence. For instance, given a successful integration of cos 7 (x), LEX2 used back propagation to discover that the same sequence of rules would have worked an any term of the form cos"(x). where n was an odd integer. The first rule of this sequence, was then given the precondition, f=cos ~ odd(r). In forming this constraint, back propagation also defined the concept 'odd' as any number of tne form 2k+ 1, where k is an integer·. Proof analysis can also be used to analyse faulty proofs and repair them. For instance, a classic faulty proof in the history of analysis is due to Cauchy, namely that a conver~ent serie.s of . con­ tinuous functrons rs contrnuous. Thrs proof can be analysed using deduction and the fault identified as a missing occurs check during unification (see section 3.1. This suggests an obvious patch, namely changing the order of quantifiers in the theorem statement, and this generates three new concepts and three new and correct theorems. One of these is the traditional replacement of convergence by uniform convergence; one is a trivial theorem whose conclusion is always true; and one is a new theorem involving the concept of equi-continuity. This reasoning process, which we will call argument removal, has been implemented in a program, SEIDEL, descr·ibed in [Bundy 65]. 6 It would have been mor~ powerful to r~member the wholo sequence aa a proof plan and make the conatraints the preconditions of the plan rather than just its first atep. 7 See [Lakatoa 761 for a diacusaion of this proof and i ta hiotory. For a survey of the use of proof anatysis for learning see [Boswell 85]. ## 3.4. Inductive Inference Inductive inference has received a tot of atten­ tion in the tearning literature, with a number of techniques being developed. For a survey see [Oietterich et al 82] and for an analytic com­ parison of some of these techniques see [Bundy et al 83]. They alt learn a concept from examples and, sometimes, non-examples of it. From examples of the concept the techniques might generali~e: replacing specific relations and terms with more generat ones. From non-examples of the concept the techniques might discriminate: pruning away rela­ tions and terms that are not an essential part of the concept. This can be used for the learning of both new object-level (factual) and new meta-level (search control). For instance, Mitchell et al's LEX program, [Mitchell et al 81], used induction to learn the meta-level conditions for applying a particular strategy for integrating by parts. Given that the strategy worked correctly to integrale 3x.cos(x) and 5x.sin(xl. LEX generali:.::ed these terms to hypothesise that the strategy will work for terms of the form nx.trig(x), where n is any integer and trig any trigonomGtr·ic function. Both the sub-techniques of generali:lation and dis­ crimination are crucially dependent on the descrip­ tion space. For instance, in LEX the description space contains concepts like 3, 5, n, cos, sin, trig, etc. The generalization of two concepts is the most specific concept in the description space which includes both of them, e.g. trig is the generali7.ation of cos and sin. However, if a term for 'sine or cosine' were added to the description space then it would replace trig as the generaliza­ tion of cos and sin. In fact, this is the concept required, as discussed in ·section 3.1. Without it, I.EX overgeneralises to trig. ## 3.5. Formula Extraction A key technique in the mathematical formalisation of problems is the extraction of formulae from a meaning representation, e.g. the semantic represen­ tation of an English description of the problem. Formutae extraction techniques have received little at tention in AJ despite their importance in human mathematical reasoning. However, the MECHO program, [Bundy et al 79], contained a formuta ex­ traction technique called the Marp/es algorithm, for forming equations to describe mechanics problems. The Marples algorithm is a kind of plan formation techr.ique. Equations are formed by instantiating physical laws, e.g. F=MA. With each taw is stored a Iist of the things it is about and a togicat descrip­ tion of how these things relate to the variables in the law. For instance, F=MA is about an object and a direction. The variable M is the mass of the object , A its acceleration in that direction, and F the sum of the forces acting in that direction. A taw and a situation are chosen after an anatysis of the unknowns and givens of the problem. The vari­ ables are then instantiated by inferring the togical description from the meaning of the English problern statement. This inference process may use deduction and default reasoning to fill gaps between the state­ ment of the problern and the knowledge requirGd to instantiate the taw. MECHO used resolution guided by meta-level inference for the deduction and the closed world assumption for the default reasoning. Deduction was needed, for instance, to work out the contributions to the sum of forces from gravity, the tensions of strings, the reactions of contact surfaces, etc. Default reasoning was used, for instance, to assume that the only surfaces in contact were those mentioned in the problern statement. ## 4. The Interaction of Reasoning Techniques The mathematical reasoning techniques outtined above can interact in a variety of . ways. For instance, successful deductions might provide the material for proof analysis and for analogy. Proof analysis may suggest proof plans to aid deduction. The desire to make a particutar theorem hold may trigger a process of proof analysis that Ieads to changes in definitions and axioms. Sometimes these interactions can be more intimate. Several deduction techniques may be co-routined or even merged so that each prunes the search space of the others. We discuss some of these possibilities in more detail betow. ## 4.1. The Interaction of Techniques in the PRESS Family In my research group work has continued over a number of years on a famity of programs working on the common domain of symbolic equation solving. - As described in [Bundy &. Welham 81] and section 3.2 above, the PRESS program used the deduction technique of rewrite rules to generate solutions to equations. This deduction technique was guided by the search cantrot technique of meta­ level inference. - The LP (Learning PRESS) program (see [Silver 84] and section 3.3) used the proof analysis technique of precondition analysis to extract and conjecture new methods of solving equations which were then used by PRESS. - The IMPRESS (Inferring Meta-knowtedge about PRESS) program, [Sterling &. Bundy 82], was a theorem proving program for proving properties of togic programs. It was used to prove properlies of the Prolog code of PRESS using a modified version of recursion guidance (see section 3.2). For instance, it proved the correct­ ness of some PRESS equation solving methods, i.e. that under appropriate preconditions the methods would achieve their· goal. - As described in [Bundy et a/ 79] and sec­ tion 3.5 above, the MECHO program solved mechanics problems stated in English by extracting and solving equations using the Marples algorithm. The equation solving part was done using PRESS as a sub­ progr·am. Each of the above techniques is incomplete on its own. Meta-level inference requires a rich supply of meta-level concepts to analyse problems and bring to bear appropriate methods of solution. These meta-level concepts can be extracted from example solutions by precondition analysis. The new methods conjectured by precondition analysis can be shown to be correct using recursion guidance. The ex­ ample solutions required by preconditions can be supplied by deduction with a less constraining search control. The problems to be solved by deduction can be supplied by the Marples algorithm, but this technique requires deduction together with meta­ level inference to bridge gaps between the knowledge it requires and that provided in the problern statement. The interactions are summarised in table 4-1. 9 Table 4-1: The Interactions between the Techniques in the PRESS Family | Technique | Problem | Solution | |------------------------|--------------|---------------------------------| | deduction | search | meta-level inference | | | problems | Marples alg. | | meta-level inference | learnins | pre-condition analysis | | pre-condition analysis | verification | deduction/ recursion guidance | | | e>