A Model of Analogy-Driven Proof-Plan Construction

1 Introduction

Theorem proving by analogy finds a proof/proof-plan for a target problem guided by a given proof/proof-plan of a source problem which is similar to the target prob­ lem. The main use of analogy consists in reducing the search (or user interactions) by suggesting target proof steps that correspond to the source case. At the same time it can propose lemmas to be used in the target case that are similar to the source lemmas. Mathematicians have clearly recognized the power of analogical reason­ ing in mathematical problem solving [Hadamard, 1945; Polya, 1957]. Hence, integrating analogy into theorem provers was pointed out as one of the challenging prob­ lems in automated theorem proving in [Bledsoe, 1986; Wos, 1988].

In this paper a new approach to theorem proving by analogy is presented that works at the proof-plan level rather than at the actual proof level. First the need for a new model is substantiated by contrasting the way mathematicians use analogy to previous techniques for analogy in automated theorem proving. Then the model is presented , and finally a small example illustrates how the analogy-driven proof-plan construction works.

*On leave from University Saarbriicken, Germany

1.1 The Need for a New Model

Kling's work [Kling, 1971] was one of the first attempts in theorem proving by analogy. His system essentially produces mappings between predicate symbols. These mappings are applied to the assumptions of the source proof to find the assumptions for the target proof.

[Munyer , 1981] focusses on the formulas derived in each proof step. Munyer applies a symbol mapping, con­ structed from the source and target theorem, to these formulas in order to obtain the derived formulas in the target proof.

[Owen, 1990] thoroughly analyzed Kling's and Mun­ yer's approaches to theorem proving by analogy and showed them inadequate even for many simple analogies. Owen's account emphasizes the matcher that recursively constructs symbol mappings and argument pairings. He transfers single calculus steps, i.e. binary resolution and paramodulation, from the source proof to provide steps in a target proof.

In [Brook et a/. , 1988] an initial symbol mapping and a pairing of definitions and lemmas of the source with those of the target is to be provided by the user. Focussing on failed constructions of analogous proofs some heuristics are used for patching target proofs. In the same intellectual tradition Bledsoe continued deal­ ing with the debugging of analogies by his precondition prover [Bledsoe, 1995].

In summary, computational accounts of theorem prov­ ing by analogy have been dominated by the idea of map­ ping symbols of the source theorem to symbols of the target theorem and employing an extended symbol map for transferring single proof steps of the source to the target 1 .

Empirical investigations, however , provided evidence that this idea does not appropriately cover many analo­ gies drawn by mathematicians, not even all the analogies of a standard textbook [Deussen, 1971] we used for an empirical study [Melis, 1993a]. I empirically analyzed mathematical theorem proving [Melis, 1994a] and found that:

1 Though Bledsoe transfers larger steps calling an auto­ mated prover but again uses symbol mapping.

• Theorem proving by analogy is embedded into proof planning: Methods, rather than just single calculus steps, are transferred analogic­ ally in mathematical theorem proving by ana­ logy.
• For many of these analogies just symbol map­ ping is insufficient. A change of a problem representation by, e.g. , unfolding a definition, can be necessary to reveal the commonality of theorems or assumptions, upon which the ana­ logical transfer is based. Other mappings of problems and proofs that go beyond symbol mapping are necessary as well. For some ana­ logies, first the right level of abstraction has to be found before transferring a proof.
• Many proofs by analogy result from transfer­ ring parts of the source proof to parts of the target proof, and some proofs by analogy trans­ fer only the proof idea, while others transfer a detailed proof.

2 The Model

Our approach takes into account the above mentioned empirical findings and incorporates

• the analogic'al transfer of proof-plans ,
• a reformulation of proof-plans that includes abstraction 2 and other reformulations that go beyond symbol mapping.
• the restructuring of proof-plans.

Proof-plans, defined below, were introduced in [Bundy, 1988]. To motivate the analogical transfer of proof-plans rather than of proofs: Proof-plans are high level representations of proofs that consist of methods. We postulate that the transfer of plans by using and transforming their methods is the right level of abstrac­ tion at which to draw analogies: If methods are named, like, e.g., the Diagonalization method [Melis, 1994b], then mathematicians claim to prove the theorem by the same method. If no name is established for the way a theorem is proved, then they just say that the proof is done analogously. Proof-plans are better suited for ana­ logical transfer than formal proofs which are often too brittle to apply a transformation in general 3 . But still proof-plans contain enough information to construct a concrete proof for a given problem. Proof-plans encode the structure of a proof because they consist of general methods encoding a proof idea and of more specific, de­ tailed methods. Hence, analogies at different levels of details can be realized by analogically transferring to the target the transferable methods of a source proof-plan. In maths, as in all complicated domains, control know­ ledge, as part of mathematician's expertise, plays an im­ portant role by drastically restricting the search and by guiding problem solving. As opposed to actual proofs, proof-plans may record justifications for the proof plan­ ning decisions , e.g. the relevant control knowledge, and this information can be reused for constructing a tar­ get proof-plan. In our derivational analogy (see below) a decision in the target is made correspondingly to the decision in the source only if the justifications of the decision hold in the target as well . Thereby the require­ ment of a semantic justification of analogical reasoning [Russell , 1988] can be met . Proof-plans may record user interactions and thus avoid the tedious user-supplied guidance in theorem proving, that is usually necessary to produce a complicated proof, 4 by reusing a great deal of the previous user decisions. We integrate the call of an automated theorem prover ( atp) into our plan oper­ ators and thus obtain another advantage of transferring proof-plans, namely the suggestion of proof steps likely to be feasible for an atp within a given time limit .

2 Including abstraction into analogy has also been pro­ posed in [Plaisted, 1981; Villafiorita and Sebastiani, 1994] .

3 Personal communication with Bob Harper concerning transformational tactics in Nuprl.

The description of the top level procedure will be gen­ eral enough to cover analogy for different proof planners. Of course, the concrete implementation depends on the respective planner and its operators. For instance, for employing the full range of reformulations, the operator representation has to be mainly declarative. Therefore we refer to the operators designed for n-MKRP (Huang et a/., 1994a]. We briefly review how these operators and plans are defined, introduce reformulation and de­ composition, and discuss the analogy procedure.

Operators

Sequents P = (L\ f- F) , are pairs of a set L\ of formulas and a formula F in an object language that is extended by meta-variables for functions, relations, formulas , sets of formulas , and terms.

Our planning operators , called methods, are frame­ like structures defined in [Huang et a/. , 1994b] with pre­ and postconditions just as the common planning oper­ ators. More specifically, methods M have the follow­ ing slots: parameter , preconditions (pre(M)) , postcon­ dition (post(M)) , constraints, proof schema and proced­ ure. pre(M) is a set of sequents from which the applic­ ation of the method derives post(M) which is a sequent as well . pre(M) and post(M) both are needed for plan­ ning. The constraints are formulated in a meta-language and serve to restrict the search during planning, e.g. , re­ strictions of pre(M) , post(M) , or of the parameters. The proof schema is a declarative schematic representation of proofs in the object logic, relying on the Nat ural Deduc­ tion (ND) calculus and on invoking automated theorem provers such as OTTER [McCune, 1990]. The standard program in the slot procedure executes the applicat ion of the proof schema.

Our methods mainly differ from those in [Bundy, 1988] in that the tactic slot is replaced by a declarative proof schema and a procedure interpreting this schema 5 . The intention behind this difference is to enable reformula­ tions of methods.

A method is verifiable if, given pre(M) , then the method yields a correct proof of post(M) for every instantiation of the meta-variables in case the constraints are satisfied. For verifying a line with an atp-call, a time limit is set for the atp to prove the sequent .

4 For instance, 17 41 lemmas had to be user supplied in Shankar's proof/verification of Godel's First Incompleteness theorem[Boyer and Moore, 1988] .

5 Besides, the slots are renamed, e.g., our preconditions are named input there.

Proof Plans

Since in general maths proofs are constructed top down and bottom up, we consider backward and forward search in proof planning and define plan operators to be an f-method or a b-method respectively. f-methods work with their preconditions as input and postcondition as output; b-methods work vice versa. For instance, the method corresponding to the ND-rule A-elimination is a typical f-method, whereas the method A-introduction is a typical b-method. f- and b-methods will be treated differently by the analogy procedure.

Goals and assumptions are sequents, and a proof-plan is a forest the trees of which consist of sequent nodes and method nodes that satisfy the "link condition": A method node M follows a sequent node g and precedes the sequent nodes g1, . . . ,gn if

<7(post(M)) = g and <T(pre(M)) = {g1, . .. ,gn} for a sub­ stitution O" of parameters.

Proof planning starts with a goal g and assumptions (0 f- F;), where F; are proof-assumptions, axioms, defin­ itions, or lemmas. The proof planning proceeds by in­ serting methods and sequents: A b-method follows a goal and yields new (sub )goals as its successors. An f­ method precedes assumptions and yields a new preceding assumption. Planning aims at reducing the gap between leaf goals and assumptions. Leaf goals that are not equal to an assumption are called open goals. As soon as a goal g; equals an assumption, the two nodes collapse. Then gi is no longer an open goal but satisfied. The planning terminates if there are no open goals.

The source proof-plans are trees with the source prob­ lem at the root, with no open goals, and with verifi­ able methods. For the analogy procedure we use lin­ earized proof-plans ordered by the sequence in which the nodes have been added to the plan. As in [Veloso, 1994] justification structures, used to encode justifica­ tions for the decision made, annotate the plan nodes. These justifications capture the subgoaling structure of a plan and point to reasons for the choice, such as ap­ plication conditions of a method, user-given guidance, or pre-programmed control knowledge.

Reformulation

Reformulations are mappings p of a proof-plan to a proof-plan which usually but not necessarily preserve the verifiability of methods in a plan. They encode mathem­ atical heuristics on how a proof-plan changes dependent on certain changes of the problem to be proved and, thus, have to be discovered empirically. Reformulations may change methods, sequents, and justifications of nodes.

Reformulations are carried out by meta-methods which are represented by data structures with the slots parameters, application-condition, effect, program. The purpose of the slots application-condition, effect is to meta-plan a sequence of reformulations. program ex­ ecutes the reformulation dependent on parameters. We empirically found several classes of reformulations:

1. Abstractions which correspond to PI abstrac­ tions in [F.Giunchiglia and T .Walsh, 1992]. An example of an abstracting meta-method is Homomorphism-Abstraction (See [Melis, 1993b]). Abstractions may change methods, sequents, and justifications but preserve the subgoaling structure.
2. Reversions are inverse abstractions. They may change methods, sequents, and justifications but preserve the subgoaling structure.
3. Normalizations that add a method M and a subgoal or assumption to the proof-plan for which pre(M) =Th post(M) for a do­ main theory Th . Usually M folds or un­ folds definitions or applies logical equivalences. An example of a normalizing meta-method is Unfold-Definitions.
4. Alterations differ from abstractions and rever­ sions. They preserve the subgoaling struc­ ture but may change methods and sequents as well as justifications. An example is Add-Arguments (See [Huang et al., 1994b; Melis, 1995]).
5. Compositions of the reformulations above.
6. The sequence of reformulations that were needed to prove theorem 5.7from the examined textbook [Deussen, 1971] by analogy is shown in Figure 1. Here the source proof-plan consists of the goal:

0 f- 'if, x(f E FAx E T1 --> ~(! * x) = f * ~(x))) 6 , assumptions, and one method Ms only. The target goal 0 f- Vx, y(x, y E H1 --> ~(x · y) = ~(x) · ~(y)) is theorem 5.7. The reformulation in Figure 1 aims at matching the

Ms D

Figure 1: Ms is changed to MT

source goal with the target goal, and this purpose guides the reformulation of the whole source proof-plan. Start­ ing with the source plan that contains the method Ms the consecutive application of reformulations eventually provides a target plan with the method MT:

post(Ms)= (01- 'Vf,x(f E Fl\x E Tt-+ <'P(f*x) = f*<'P(x)))

post(Mst) = (01- 'Vx(x EX-+ <'P(Op(x)) = Op(<'P(x))))

post(Ms2) = (01- 'Vx,y(x,y EX-+

<'P(Op'(x, y)) = Op'(<'P(x), <f:l(y))))

post(MT) = (01- 'Vx,y(x,y E H1-+ <'P(x · y) = <'P(x) · <'P(y))). Here Homomorphism-Abstraction introduces a new unary function parameter Op for f* and Add- Arguments then replaces Op by a binary function para­ meter Op' 7 , while Homomorphism-Reversion specifies Op' as ·. All these replacements require additional changes which are also realized by the mentioned meta­ methods. For the detailed reformulation see [Melis, 1993b].

6 T1 denotes an F-semimodul, H1 a semigroup

Decomposition

In addition to reformulation, the analogy-driven proof­ plan construction decomposes methods of proof-plans as well. Decomposition maps a proof-plan to a proof-plan by ireplacing a sub-plan P with one method by a sub-plan with several methods while preserving the root and leaves of P. An example is Conjunctive-Decomposition that decomposes a method M with post(M) = (~ f- F1 1\ F2) into a plan with methods M1, M2, and M" with post(M1) = (~ f- F1) and post(M2) = (~ f- F2).

Decomposition is applied at two different places in the analogy procedure for two different purposes: Firstly, decomposing a source method yields a subgoal that matches an open target goal. This is the case if only a part of the source plan can be transferred and if the source method contains a transferrable as well as a not transferrable part. Secondly, decomposition can be used if a reformulated method cannot be verified. This method is decomposed in order to find a verifiable sub­ method.

2.1 Analogy-Driven Proof-Plan Construction

Problem solving by analogy transfers the way a prob­ lem is solved (derivational analogy) or the final solu­ tion (transformational analogy). Derivational analogy in [Carbonell, 1986; Veloso, 1994] stores problem solv­ ing decisions and their justifications in the source plan and replays them for the target. Transformational ana­ logy in [Carbonell, 1983] takes the source solution and transforms it into the target solution.

Our analogy-driven proof-plan construction can be considered a combination of derivational with transform­ ational analogy. 8 Basically it is a derivational analogy, however, it also transforms the source plan. Actually, it is a control strategy for proof planning that extends the derivational analogy of [Veloso, 1994] by reformu­ lation, decomposition, and bidirectional planning. The general idea of our analogy model is to use the linear­ ized source proof-plan together with its justifications as a guide for constructing an analogous target proof-plan and to transfer methods (and sequents) of a reformulated source proof-plan to the target proof-plan.

7 Add-Arguments is applicable to a proof-plan if a func­ tion f with n arguments is to be mapped to an f' with n + m arguments, where the m arguments to be duplicated are specified out of the n arguments of f as parameters of the meta-method. The meta-method replaces the f by f' in goals, assumptions, and methods and yields additional re­ lated changes in methods.

8 For example, "initial-segment concatenation" and "final­ segment concatenation" in transformational analogy corres­ pond to some normalizing reformulations.

Table 1 shows the top-level procedure of our analogy­ driven proof-plan construction. Given a parametrized, linearized source proof-plan, target assumptions, and a target goal (the first open goal), the output of the pro­ cedure is a target proof-plan. Steps 5 - 7 are those that are relevant for a planner with backward search only. Steps 8-10 cover the transfer off-methods. The former matches a source goal and transfers a b-method whereas the latter matches as many source assumptions as pos­ sible to target assumptions and transfers an f-method. lmissing(p'M)I < n means 9 that less than n precondi­ tions of the currently treated reformulated f-method M do not match a target assumption.

input: linearized source plan, (open) target goal output: (linearized) target plan

1. while there are open target goals do
2. if source plan is exhausted, then base-level plan for the open goals.
3. Get next sequent P from source plan. The se­ quent is either an assumption or a goal. if P is an assumption, then go to 8.
4. if P is already satisfied, then go to 2.
5. ifthere is a reformulation p left, such that pP matches an open target goal YT for which the justifications hold,
6. then reformulate source plan by p and link YT to source plan.
7. else decompose source and go to 2.
8. Select for the target the b-method M chosen in reformulated source.
9. ifM'sjustifications hold for in the target,
10. then verify /modify M and go to 1.
11. else go to 5
12. Select for the target the f-method M chosen for P in the source.
13. if there is a reformulation p' left such that lmissing(p' M) I < n and that justifications hold for the matched target assumptions
14. then reformulate source plan by (best) p' and link the matched target assumptions to source plan.
15. else decompose source and go to 2.
16. ifM'sjustifications hold for p'M in the target,
17. then verify /modify p'M and go to 1.
18. else go to 9.

Table 1: Outline of the analogy-driven proof-plan con­ struction

The first goal of the linearized source plan, usually the source problem P s, is chosen in 3. If P s can be reformu­ lated by a p such that it matches the target problem PT, then p will be applied to the (current) source plan and the method M with post(M) = pP s is a candidate for the transfer to the target. If P s cannot be reformulated by a p to PT, then decomposition is applied in order to find a submethod M1 of M that can be transferred. If in 5 or 9 a decomposition is not possible, then the plan stays unchanged. After the decomposition a new reformulation p and match of post(Ml) is tried and 6. suggests pM1 as a candidate a target method. 7. checks whether the justifications of the source method hold in the target for pM1 and if so, its verifiability is checked. The latter test is necessary because reformulation does not necessarily preserve verifiability. If pM1 is not veri­ fiable, the.n a promising modification is applied (either decomposmg the method in order to obtain a verifiable submethod or calculating additional preconditions of the method yielding verifiability.). In table 1 verify/modify M abbreviates:

9 For missing(M) := set of preconditions of M that do not match a current target assumption. The sequents of missing(p'M) become new open goals if p' is an acceptable reformulation.

• test verifiability of M
• if M is not verified, then modify M to a verifiable (sub )method lO
• update open target goals and assumptions
• link the verifiable method to source plan.

.The. analogy. ~rocedure is repeated, first testing ter­ mmatwn cond1t10ns (1.,2.) . Base-level planning is ac­ tivated when the guidance by the source proof-plan is exhausted in order to prove the remaining open goals. Superfluous steps in the target plan are skipped in 4. This procedure yields a target plan with verified meth­ ods. The target plan may have open goals.

Phras.ed in the terminology of case-based reasoning, adaptatwn t~ke~ place via reformulation of proof-plans, through mod1fymg not verifiable methods, skipping su­ perfluous methods, and through closing gaps in the tar­ get plan by base-level planning.

The possible objection that every new example would need a new set of meta-method did not turn out to be true. Reformulation focussed on altera­ tion and, unexpectedly, Restricted Term-Mapping and Add-Argument were used quite often.

Controlling the Search for Reformulations

So far we have only few meta-methods available and thus search is restricted .. As the set of meta-methods expands, however , the followmg control features become more im­ portant:

• The application of meta-methods is controlled by their application-conditions.
• The reformulation of source plans is guided by the target goals and assumptions to be matched.
• The following fixed sequence of reformulations proved most useful: normalization, abstraction alteration, reversion and should thus be super~ imposed upon search.
• User-supplied correspondence tables for rela­ tions and functions in specific maths areas carry semantic information and provide addi­ tional guidance for reformulations. A corres­ pondence table helps to relate source to target assumptions and may prescribe the mapping of function or relation symbols.

With a growing variety of reformulations it will be ne­ cessary to meta-plan the application of meta-methods using the application-conditions and effect or to interact­ ively choose reformulations.

10 No result if no verifiable (sub)method exists.

3 Example

An example that illustrates all features of the approach (as, e.g., in [Melis, 1995]) needs too much space. The fol­ lowing .example does not take much advantage of proof­ plans; 1t focusses on decomposition and uses the meta­ methods Term Mapping and Symbol Mapping only. Source (sub )goals:

Target goal:

gS =even( a) 1\ even( b)--+ even( a* b), g1S = e~en(a) 1\ even(b) 1- a* b = 2 * c, assumptwns: a1S = 01- 'v'x(even(x)--+ 3y(x = 2 * y)) and a2S = 'v'x'v'y'v'z((x * y) * z = x * (y * z)) · gT =odd( a) 1\ odd(b) 1- odd( a* b) assumptions: a1T = 01- 'v'x(odd(x)--+ 3y(x = 2 * y + 1)) and . a2T = 'v'x'v'y'v' z((x * y) * z = x * (y * z)).

F1gure 2 shows how a target proof-plan is constructed incrementally guided by the source proof-plan:

• Method M1s is decomposed into Mus and M12s because gS can not be reformulated such that it matches gT.
• gOS = post(M12s) = even( a) 1\ even(b) 1- even( a* b) as well as the proof-plan is reformulated by the Symbol Mapping p1: (even ==? odd) yielding p1gOS = gT.
• p1a1S and the whole plan is further reformu­ ~ated by the Term Mapping p2: (2 *t ==? 2 *t + 1) m order to match the target assumption a1 T. The resulting method p1p2M12s is verifiable and has the precondition p1 p2glS = glT = odd( a) 1\ odd(b) 1- 3c(a * b = 2 * c + 1).
• The method P1P2M2s is not verifiable and hence, is decomposed into p1p2M21s and P1P2M22s, where P1P2M22s becomes M2r and

• post(M2T) = a3T = odd(a) 1\ odd(b) 1-­ a* b = (2 * a1 + 1) * (2 * b1 + 1).
• Since the source plan is exhausted now, the gap between the assumption a3T and the open sub­ goal g1 T has to be closed by base-level planning for g1 T using a1 T, a1S and maybe additional lemmas.

4 Conclusion and Future Work

Analogy in theorem proving does not work as a stand alone problem solver but works very much in connec­ tion with ordinary theorem proving, for instance, to val­ idate details which are left as open goals. Besides, a source proof-plan has to be provided using proof plan­ ning. There are neither guaranteed success nor com­ pleteness claims in this context because analogy is a heuristic strategy that is tentative.

Our approach combines ideas of previous systems for theorem proving by analogy with derivational and trans­ formational analogy. It works in a planning frame­ work and incorporates reformulation, and thus, it is more widely applicable than previous approaches which did not attempt to re-represent the source problem and, hence, their results were highly dependent on the actual representation of theorems and proof assump­ tions. Wider applicability is documented by several ex­ periments with the analogy-driven proof-plan construc­ tion on real mathematical theorems which succeeded in providing analogous proofs where other approaches did not. The experiments dealt with theorems from a stand­ ard text [Melis, 1993b], the pumping lemma for context free languages [Melis and Veloso, 1994], and a Reine­ Borel theorem [Melis, 1995]. These theorems provide a small but quite a representative sample. Furthermore as discussed above, the approach is cognitively more ad­ equat: Among others, [Melis, 1995] has shown that the interpretation of parameters, that might be necessary for completing an analogous proof, corresponds to situations observable for a mathematician's use of analogy.

In general there will be a tradeoff between the higher flexibility and the search needed for reformulation in automatic analogy-driven proof-plan construction. Since usually only few reformulations are needed, however, the search for appropriate reformulations is much less than the search usually needed for a proof.

Currently some reformulations are implemented but chosen by the user. The retrieval of source proof-plans has not yet been approached. Hence, up to now we model common situations in which the source is given only. Be­ sides further implementation future work is necessary to retrieve the source proof-plan automatically, to automat­ ically control the application of reformulations, and to discover more, frequently used maths reformulations.

Acknowledgements

Many thanks to Woody Bledsoe for help and encour­ agement . I would like to thank Manuela Veloso, Man­ fred Kerber, Xiaorong Huang, Dieter Hutter, and Alan Smaill.

This work was supported by a research grant of the Deutsche Forschungsgemeinschaft and HC&M contract CHBICT930806 .