Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs

1 Introduction

We investigate the improvement of theorem provers by reusing previously computed proofs, cf. [Kolbe and Walther, 1994; 1995]. Our work has similarities with the machine learning methodologies of explanation-based learning [Ellman, 1989], analogical reasoning [Hall, 1989], and abstraction [Giunchiglia and Walsh, 1992]. An ab­ stract view of our approach for reusing proofs can be sketched in the following way:

Assume that an automated theorem prover shall be supplemented by a learning component. If the prover is asked to prove a new conjecture 1/J which is similar to a previously proven conjecture 1(>, it first tries to associate each function symbol occurring in I(> with a (syntacti­ cally) corresponding function symbol from 1/J. These as­ sociations are then propagated into the proof of I(> for obtaining a proof of 1/J. But generally, there are function symbols in the proof of I(> which do not occur in the con­ jecture I(> and thus still have to be associated. If these function symbols can be associated such that the axioms used in the proof of I(> are mapped to provable formu­ las, the proof of I(> is successfully reused for proving 1/J.

1 This work was supported under grants no. Wa652/4-1,2,3 by the DFG as part of the focus program "Deduktion".

Here we are concerned with providing the associations for function symbols automatically such that verifiable proof obligations for 1/J are obtained.

We propose an indirect way of association by first generalizing the function symbols from (the proof of) I(> to function variables, i.e. we use a second-order lan­ guage. Then we instantiate the function variables occur­ ing in the generalization of I(> - the so-called bound func­ tion variables - with function symbols by second-order matching with 1/J. For providing the remaining associa­ tions a further second-order substitution has to be found which replaces the so-called free function variables, i.e. function variables which occur in the generalization of the proof of 1(>, but not in the generalization of 1(>. We call such a second-order substitution a solution (for the free function variables), if all formulas stemming from axioms in the proof of I(> are true.

As the solvability of free function variables is defined w.r.t. a set of axioms, it is undecidable in general whether a solution exists, and in the positive case the solution is not unique. Here we develop an efficient procedure for computing solutions by second-order matching "modulo evaluation". Our algorithm incorporates the underly­ ing axioms by heuristically combining the second-order matching algorithm of [Huet and Lang, 1978] with the technique of symbolic evaluation, cf. e.g. [Walther, 1994].

2 A Method for Reusing Proofs

We briefly illustrate our technique for reusing proofs, cf. [Kolbe and Walther, 1994] for a more detailed account : If the prover has computed a proof p for a conjecture 1(> , the proof is analyzed yielding a so-called proof catch c. The catch is a set of axioms providing the features of p which are relevant for reusing the proof in subsequent verification tasks. Then I(> and c are generalized by re­ placing (different occurrences of) function symbols with {different) function variables, yielding a schematic con­ jecture <1> and a schematic catch C. The latter is a set of schematic formulas which logically implies the schematic conjecture <1> . Thus C f= <1> is guaranteed by our analy­ sis and generalization method where f= denotes (first­ order) semantical entailment. Such a pair PS := (<1>, C) is called a proof shell and serves as a base for reusing the proof p if the system has to prove a new conjecture 1/J which is similar to 1(>:

If 1/J is obtained from ~ by matching, i.e. 1/J = 1r( ~) for a second-order substitution 11" (which means that 1/J is similar to It'), then the proof shell P S applies for 1/J via the matcher 11". Here 1r replaces the function vari­ ables in ~ - the so-called bound function variables of PS - by function symbols (resp. by functional terms, cf. Section 5) . Now we apply 1r to the schematic catch C obtaining the partially instantiated schematic catch 1r( C) which still may contain function variables, viz. the free function variables of PS occurring in C, but not in ~- Now a further second-order substitution p has to be found which replaces the free function variables of PS such that all formulas in the instantiated schematic catch p( 1r( C)) are provable. If successful then also 1/J is proved because p(1r(C)) I= p(1r(~)) and p(1r(~)) = p(t/J) = 1/J, which means that the proof p of It' could be reused for proving 1/J. Thus verifying the resulting proof obligations p( 1r( C)) is sufficient for guaranteeing the provability of 'if!. This approach is sound because semantical entail­ ment is invariant w.r.t. (second-order) instantiation, i.e. C I=~ implies r(C) I= r(~) for each second-order sub­ stitution T, cf. [Kolbe and Walther, 1995].

3 Matching modulo Evaluation

We investigate our proposal within the field of auto­ mated mathematical induction, cf. e.g. [Walther, 1994]. Here proofs often are similar, and consequently auto­ mated induction provides the regularity required for suc­ cessful reuses. For proving a given conjecture, an induc­ tion theorem prover computes a set of induction formu­ las whose provability imply the truth of the conjecture. Then the system tries to prove each induction formula from a set of axioms by first-order means, and the proofs obtained thereby are candidates for subsequent reuses.

We define functions like the length function len for linear lists by axioms like

Given the conjecture 1/J plus(len(z), len(y)) = len(app(z, y)), the induction theorem prover computes a base formula tPb and a step formula 1/J, as (plus denotes addition of natural numbers, app denotes list concatena­ tion, sum denotes summation over a linear list):

Assume that the following proof shell PS is provided which was obtained by analyzing and generalizing the proof of the . step formula It'· for the conjecture It', cf. [Kolbe and Walther, 1994], where

Here e.g. the function variables F 1 , F 2 , F 3 correspond to different occurrences of the function symbol plus, i.e. the schematic equation ( 4) stems from generalizing the lemma plus(plus(z, y), z):::: plus(z, plus(y, z)) which was required for proving It'·. As PS applies for 1/J, via the matcher 11", := {F 1 /plus, G 1 · 2 · 3 /len, H 1 fapp, D 1 /add}, the partially instantiated catch c; := 1r,(C,) =

is computed for the step case. The free function vari­ ables F 2, F 3 and D 4 stemming from (occurrences of) the function symbols plus and add in the catch of the original proof are not replaced by concrete function sym­ bols: Since these function variables do not occur in the schematic conjecture ~,, they cannot be in the domain of the matcher 1r,. We therefore have to compute a second­ order substitution p, for these free function variables which solves c;, i.e. we are looking for some p, such that the formulas p, ( c;) are provable. The attempt of solving F 2 in (5) by (syntactical) second-order matching fails, but we may evaluate the left hand side (lhs) of (5) by the defining axiom (len-2) yielding s(len(z)) = F 2 (n, len(z)) . Now the lhs matches the rhs via the unique matcher p1 := {F 2 /s(w2)} which means that (5) is solved be­ cause pi((5)) = (len-2). 2 We apply p1 to the remaining schematic formulas and obtain p1(C; \ {(5)}) as

We continue with the next schematic equation whose (say) lhs does not contain function variables, i.e. with ( 6) or with ( 9). Here we choose ( 6) and evaluating its lhs using a defining axiom for app yields add(n, app(z, y)) which matches the rhs via the unique matcher P2 := {D 4 /add}. Now the lhs of p2((7)) is purely first-order and can be evaluated, i.e. P3 := {F 3 js(w2)} is obtained by matching. Finally all free function variables are in­ stantiated and the remaining proof obligation P3 ( ( 9)) can be passed to the prover. As p3 ( ( 9)) is a defining axiom for plus, the prover is successful , i.e. the proof reuse· is completed. Thus the alternation of evaluation and second-order matching allows us to compute the so­ lution p, = {F 2 /s(w2), F 3 /s(w2), D 4 /add}. 3

4 Symbolic Evaluation

Let :E = uiEIN :Ei be a signature where :Ei contains (first­ order) function symbols ofarity i . We let T(:E, V) denote the set of all terms built with function symbols from :E and the set V of variables. The set of equations t1 = t2 with t 1 , t2 E T(:E, V) is denoted by E(:E, V), and formulas are defined as usual. 4 We denote the set of variables occurring in a (set of) term(s) resp. formula(s) ¢by V(¢).

2 Here w2 denotes the second argument of the binary func­ tion variable F 2 , i .e. p1 replaces F 2 basically with the func­ tion symbol s, but the first argument w1 of F 2 is ignored.

3 Note that the proposed method is more flexible than sim­ ply matching the schematic equations from c; with the defin­ ing axioms.

We assume that each function symbol from ~ is either a constructor of some data structure or a defined function symbol specified by some axioms, cf. [Walther, 1994). For instance the declaration

defines a data structure for natural numbers with the constructors 0 and s. The axioms (len-1,2) define the function symbol len, cf. Section 3. A term t E T(~, V) may be evaluated by applying the defining ax­ ioms for the function symbols contained in t . Thus e.g. len(add(len(empty), z)) is evaluated via len(add(O, z)) to s(len ( z)) by applying the defining axioms for len. This is called symbolic evaluation because the term may con­ tain variables (which are not evaluated). Note that only defining axioms are considered for the evaluation, i.e. the term s(plus(plus(z, y), z)) remains non-evaluable even if e.g. the associativity of plus is given as a lemma.

We assume that the symbolic evaluator is implemented by a terminating operation eval [Walther, 1994) which computes the normal form of a term such that

is satisfied for all l E T(~, V) and a set AX of axioms and lemmata.

5 Second-Order Matching

Let 0 = u iEN oi be a signature where oi contains func­ tion variables of arity i. Then T(~ U 0, V) denotes the set of all schematic terms and £(~ U 0, V) denotes the set of all schematic equations built with function sym­ bols from ~, function variables from 0, and variables from V. Schematic formulas are built as usual, 5 and 0( ¢) denotes the set of all function variables occurring in a (set of) schematic term( s) resp. formula( s) ¢. Func­ tion variables are treated like function symbols except for the application of second-order substitutions.

For defining second-order substitutions we represent functions by terms with special argument variables from the set W := {w1 , w2, ... } where W n V = 0. Thus T(~, W) is the set of functional terms and we define a family (Wi)iEIN" of subsets of W by Wo := 0 and wi := { Wt, ... , Wi}· A (restricted) second-order substitution 1r := { ... , F / s, ... } is a finite set of pairs such that the domain dom( 1r) := { ... , F, ... } ~ 0 contains (distinct) function variables and FE Oi entails sET(~, Wi), i.e. a function variable F of arity i is replaced by a func­ tional term s with at most i argument variables. The application of a restricted second-order substitution 1r to a schematic term is inductively defined by

4 0ur logic is many-3orted in general, but for the sake of readability we usually omit all sort information.

~Note that only first-order variables may be quantified.

where z E V, X E ~nU(On \dom(1r)), FE Onndom(1r), 1r(F) = s and P1, ... , Pn E T(~ u 0, V) . E.g. the ap­ plication of 1r := {F/Ien(w2), G/plus(wl, s(wt))} to the schematic term P := G(F(app(z, y), z), v) yields 1r(P) = plus(len(z), s(len(z))) . For f E ~n and F E On we use 1r(F) = f as an abbreviation of1r(F) = f(wt, ... ,wn)· Restricted second-order substitutions are applied to sets of terms or (sets of) formulas as usual. Note that V(1r(t)) <;;; V(t) and 0(1r(t)) <;;; O(t) fortE T(~ u 0, V), i.e. no first-order variables or function variables are in­ troduced by restricted second-order substitutions. Fur­ thermore dom(1r) <;;; 0, i.e. no (first-order) variables are replaced. These restrictions (compared to general second-order substitutions, cf. [Goldfarb, 1981)) are nec­ essary to ensure the soundness of our method for reusing proofs, cf. Section 3. As a consequence the subsumption quasi-ordering ::5 on general second-order substitutions from [Huet and Lang, 1978) corresponds to the subset relation <;;; in our context: ::5 is defined by 1r ::5 1r 1 iff 3p 1r 1 = p o 1r where o denotes the composition of gen­ eral second-order substitutions. But as F E dom( 1r) im­ plies p(1r(F)) = 1r(F) for restricted second-order sub­ stitutions p, 1r we have ::5 = <;;; here. Subsequently we simply say "second-order substitution" instead of "re­ stricted second-order substitution".

A target term t E T(t, V) matches a pattern P E T(~ U 0, V) iff there is a second-order substitution 1r with t = 1r(P). E.g. the target t = s(sum(z)) matches the pattern P = F(z, sum(z)) because the required matcher exists, viz. 1r = {F/s(w2)} or 1r = {F/s(sum(wt))}. Second-order matching is decidable and we can adapt the algorithm from [Huet and Lang, 1978) for comput­ ing a finite set II := match(t, P) of matchers satisfying the following conditions:

6 Solving a Proof Catch

We present the algorithm solve_catch which implements the second-order matching "modulo evaluation" illus­ trated in Section 3. We assume a fixed set of (implic­ itly universally quantified) axioms AX <;;; £(~, V) in the remainder of this section. The algorithm solve_catch has two input arguments, viz. a partially instantiated schematic catch C' <;;; £(~ U 0, V) and an auxiliary set of schematic equations X ~ £(~ U 0, V) which ini­ tially is empty. The call sol ve_catch( C', 0) fails if no matcher solving C' has been found. Otherwise it yields a pair (p, E) where p is a second-order substitution and E <;;; £(~, V) is a set of (first-order) equations such that

This means that the schematic catch C' is solved by the matcher p, if the call solve_catch(C', 0) yields a pair (p, E) such that the remaining proof obligations in E can be verified. We start with the algorithm for solve_catch and then discuss the used auxiliary functions: 6

6 The special value A indicates that it has been tried to select a member from an empty set, see below.

The function choose_eq selects some equation l =: R from C', whose (say) lhs l does not contain function vari­ ables, but whose rhs R does contain function variables. 7 We demand that for all A ~ £(:E U 0, V)

where MA := {l = R E A I O(l) = 0, O(R) # 0}. The heuristic used by choose_eq for selecting the equa­ tion l = R E Me· is discussed in the next section. The term l is evaluated by applying one or more defining ax­ ioms from AX until a term l' := eval(l) is obtained, cf. (10). Then the second-order matching algorithm match is called for l' and R, and all computed matchers are collected in a set II. Of course we require that this set of matchers II:= match(l', R) is consistent, cf. (11), but we do not demand completeness as we later select only one matcher from it anyway. Instead of (13), however, we now request a stronger form of minimality which takes the lack of completeness into account:

From the computed set of matchers II, choose_matcher selects one matcher (if II is non-empty) due to some heuristic, cf. the next section.

If II = 0, no solution for the free function variables in R was found by matching modulo evaluation. Then l = R is inserted into the so-called remainder set X (which initially is empty) and we continue by solving the remaining part ofthe catch C'\{l = R}. We will not try to solve the equations collected in X by matching again (as this must fail), but we hope that the function vari­ ables occurring in X are instantiated while solving the remaining catch such that a set of first-order proof oblig­ ations is obtained from X. Then the desired matcher p and the set of first-order proof obligations E is returned, cf. (14). Otherwise the recursive call (and thus the whole procedure) fails.

If some 1r E. II is selected, we apply 1r to the remaining part of the catch C' \ {l =: R} as well as to the remainder set X and recursively call solve_catch. If the recursive call does not fail, we obtain a matcher panda set of first­ order proof obligations E. Then 1r Up is the resulting matcher for solving the catch C' (note that dom( 1r) n dom(p) = 0 as 1r is applied before the recursive call) which is returned together with E.

7 Without loss of generality we assume that the equations are oriented such that there is no equation L = r with !1( L) # 0 and O(r) = 0.

If a recursive call of solve_catch is reached where choose_eq yields A, i.e. all equations in C' \ £(:E, V) (if any) contain function variables on both sides, cf. (15), then the alternating process of matching modulo eval­ uation and instantiating the catch terminates. Now if 0( C' U X) = 0 then the catch is solved by the identity substitution {}, and C' U X is returned as the set of first-order proof obligations. In this case also the initial call of solve_catch is successful by collecting the match­ ers which have been computed in the respective recur­ sive calls. Otherwise there is an equation in C' with function variables on both sides (which has not yet been processed) or there is an equation in X with function variables on one side (where the matching failed). We regard the catch as unsolvable then and solve_catch fails, although one can think of several alternative heuristi­ cally motivated attempts ( cf. Section 7) of solving the remaining function variables. We summarize these con­ siderations with the following theorem:

Theorem 6.1 (soundness of solve_catch) Let AX ~ £(:E, V) be a set of axioms. If the conditions (10), {11), (15} and (16} are satisfied, then for all schematic catches C' and X ~ £(:E U 0, V) the call solve_catch( C', X) ei­ ther fails or it terminates with result (p, E) such that

The function solve_catch is designed for an efficient computation of a solution for a partially instantiated schematic catch 1r(C). If there is no such solution, i.e. the reuse attempt fails, this might lead to backtracking in the calling procedure, e.g. for choosing a different 1r or C. Hence we are interested in an early failure recog­ nition within solve_catch. This can be achieved if we try to disprove those equations e E C' U X which do not contain function variables by searching for a coun­ terexample, cf. [Protzen, 1992], yielding one of the re­ sults disproved, proved or unknown. If e is disproved, then solve_catch fails as the matcher computed so far yields unprovable proof obligations, i.e. we can save any effort for solving the remaining function variables. If e is proved, it can be removed (this might happen for some "simple" equations e), and otherwise e has to be verified after all function variables are solved.

7 Heuristics

The function solve_catch has two indeterministic branch­ ing points, viz . the calls of the functions choose_eq and choose_matcher, and some heuristic guidance is required for making a good choice. We have developed heuristics with empirical data obtained from several experiments. Although the branching points define an entry for back­ tracking whenever a failure in some recursive call occurs, we avoid backtracking as we believe that only a non­ expensive solution procedure leads to useful proof reuses. Hence the success of our proposal depends on the quality of the developed heuristics.

The heuristic for choose_eq selects a schematic equa­ tion l = R E Me· which has probably the least num­ ber of matchers 1r solving eval(l) = 1r(R), i.e. the most "difficult" of the equations (without function variables on the lhs) is chosen. This choice has two advan­ tages: (i) the possibility for selecting a "wrong" matcher by choose_matcher is decreased because a point of the search space with a small branching rate is reached where it is more likely to find a good path, and (ii) the solvabil­ ity of the "difficult" equation might be lost if another, "easier" equation is chosen where it is harder to distin­ guish a successful matcher from an unsuccessful one.

As a measure for the difficulty of (solving) an equation we consider the number of function symbols and func­ tion variables occurring in it: A high number of (occur­ rences of) function symbols limits the number of possible matchers in the same way as a low number of (differ­ ent) function variables. Hence we define two mappings #r. : T(E u 0, V) --+ IN and #n : T(E u 0, V) --+ IN where #r.(t) counts the number of occurrences of func­ tion symbols and #n(t) counts the number of different function variables in a schematic term t E T(E u 0, V).

When rating the difficulty of an equation l = R we mainly have to consider the rhs R, as the lhs l is already first-order and will be evaluated yet before the matching such that it does not influence the number of solutions strongly. For the moment, we use the following heuris­ tic for choose_eq( C'): Among the candidate equations l = R E Me·, the one with the minimal value

is selected. The factor 2 serves for weighting the num­ ber of function variables higher than the number of function symbols as the former has a stronger influence on the success of the matching. For instance, given l := len(add(n, z)), R1 := P(len(G(z))) and R2 := P(G(z)), we prefer the equation l = R1 to l = R2 be­ cause hl(l = Rl) = 3 < 4 = hl(l = R2). A more sophis­ ticated rating might also consider the structure of lor R, the first-order variables in l =: R, or even the remaining equations, but we found this not necessary so far .

The heuristic for choose_matcher attempts to select the "simplest" matcher 1r E match(eval(l), R) solving the chosen equation l = R. We consider 1r as "sim­ ple" if it is "close" to replacing function variables by function symbols, e.g. 1r(P) = f(wl, ... ,wn), while e.g. 1r := {Pjplus(w2, times(w3, w2)), ... } would be consid­ ered as a more complex matcher. The underlying moti­ vation is to select a matcher which preserves the given structure of the proof being reused, because it is more likely to find a valid instance of the schematic proof in this case.

As a measure for simplicity we consider two features of a matcher: (i) a small domain and (ii) a small num­ ber of introduced function symbols. Concerning (i), we demand that the function match satisfies requirement (17), i.e. no function variables are replaced unnecessar­ ily (though this is not demanded in Theorem 6.1). The introduced function symbols (ii) are those occurring in the functional terms of 1r counted by

where we prefer matchers 1r such that #E(1r) is minimal. For instance, given l' = sum ( z) and R P(z, sum(z)), we prefer the matcher 1r1 := {P/w2} to the matcher 1r2 := {P/sum(wl)} because #r.(1rl) = 0 < 1 = #r.(1r2). So among the candidate matchers 1r E match(eval(l), R), choose_matcher selects the one with the minimal value #r.(1r). For obtaining an ef­ ficient implementation we incorporate the selection of the matcher into the matching algorithm such that only matchers 1r with minimal measure #r.(1r) are computed.

Finally we sketch another heuristical extension for solve_catch, viz. how to proceed if choose_eq( C') = A but 0( C' u X) .:p 0. In this case there is an equation in C' with function variables on both sides (which has not yet been processed) or there is an equation in X with function variables on one side (where the matching failed) . Now instead of failing we might try to solve the remaining function variables in the following way: If e.g. pi and pi are free function variables from C' stemming from generalizing different occurrences of the same func­ tion symbol f in the original proof, then we instantiate pi and pi with the same functional term. Hence we stip­ ulatep(Pi) := p(Pi) if pi E dom(p) but pi rf_ dom(p) for the matcher p computed so far. If several different instantiations p(Pi'), .. . ,p(Pi~) are available we prefer the simplest one, cf. the heuristic for choose_matcher. An example for the usefulness of this heuristic is given in the next section.

8 Lemma Speculation by Reuse

Using the heuristics proposed in the previous section we can reuse the proof shell PS = (~, C,) from Fig. 1 for proving the step formulas 1/Ji,· of the conjectures 1/Ji: 8

Table 1.

For each i a matcher 11"i for 1/Ji,· and the schematic step formula ~, is selected, i.e. 11"i ( ~,) = 1/Ji,·. Then solve_catch is called with the partially instantiated schematic catch C'i := 11"i(C,), yielding some proof oblig­ ations Ei and a solution Pi for the free function variables.

Like 1r, from Section 3, the matcher 7ro replaces only function variables with function symbols, e.g. 1r0 ( P 1 ) = x and 1r0 (D 1 ) = add, whereas 1r1 with 1rt(D 1 ) = s(wz) makes use of functional terms. This allows to reuse the proof of 'f'· involving the data structure list for a con­ jecture concerning the data structure number. Similarly

8 x multiplies two numbers, prod multiplies the numbers in a list, db I( :z:) computes 2 x :z:, rev reverses a list, and exp( :z:, y) computes :z:Y.

1r2(F 1 ) = app( w2, wl) swaps the arguments of F 1 and 11'a( G 1 ) = w1 uses a projection to match the schematic step formula.

The applicability of a proof shell can be increased if we "freeze variables to constants", i.e. a (universally quan­ tified) variable z E V is regarded as a new constant z E 'Eo. Thus e.g. conjecture 1/;4, i.e. the distributiv­ ity law for x and plus, matches the schematic conjecture Cf> because now 1r4 ( G 1 · 2 · 3 ) = x ( w1 , z) E T('E, W) can be used for the matcher. 9 This yields the partially instan­ tiated schematic catch C~ = 1r4 (C,) =

and solve_catch computes the solution

In the same way the reuse is enabled for the remain­ ing conjectures 1/Js, ... ,'!/;9, where the reuse for 1/;8 (the associativity of x) succeeds only when freezing y and z using the matcher 11's = {F 1 ( x (w1, x(y,z)), G 1 lw1, G 3 I x (wl! z), H 1 I x ( w1, y), D Is( w2)}· For solving the catch C~ the heuristic "instantiate F like F 2 " given at the end of the previous section is required.

Often one of the proof obligations in Ei is a lemma, indicated by the last column in the table above("-" de­ notes that all members of Ei can be symbolically evalu­ ated to tautologies of the form t = t). Thus e.g. the as­ sociativity of plus, i.e. 1/;6, is computed as a proof oblig­ ation when proving 1/;4, by reuse, cf. the last equation of C~ above. 10 If such a lemma is not already known in advance, it is speculated by instantiating a schematic equation with the matcher Pi obtained by solving the remaining part of the catch. In a direct proof of the step formula 1/Ji,· such a useful lemma has to be generated explicitly, cf. e.g. [Walsh, 1994] for examples.

Moreover, a lemma speculated by reuse is often a gen­ eralization of a lemma which is generated in a direct proof. Thus e.g. a direct proof of 1/;4, would generate the lemma 0'(1/;6) = plus(z, plus(x(z,z), x(y,z))) := plus(plus(z, x(z,z)), x(y,z))

(where 0' = {zlz, Yl x (z,z), z/ x (y,z)}) if we proceed by using axioms for modifying the induction conclusion until the induction hypothesis is applicable. For obtain­ ing a proof of 1/;4,, this lemma is usually generalized by the inverse substitution rule, cf. [Walther, 1994], yielding 1/Js. This generalization effort is saved by our approach as 1/;6 is the lemma which is speculated for 1/;4, by reuse.

9 Conclusion and Future Work

We have developed an heuristically controlled algorithm for solving the free variables of a partially instantiated schematic proof catch. This algorithm, which is im­ plemented in our prototype of a learning prover, the PLAGIATOR-system [Brauburger, 1994], has proved suc­ cessful for many examples, including those from Table 1. Hence we are able to verify these conjectures by auto­ matically reusing the proofs of previously proved, similar conjectures. As a side effect useful lemmata are specu­ lated by our method.

9 This kind of skolemization is sound because for a skolem constant z and a formula tf>[z] with a free variable z holds: 'v'z.tf>[z] is valid iff t/>[z] is valid.

10 The proof obligation obtained for the conjecture t/>2 · is an instance of the associativity of app, viz. the lemma 0'2( t/>1)

where 0'2 = {z/add(z, empty)}.

Table 1 also suggests a recursive organization of the reuse procedure as the proof obligations returned by our solution algorithm may also be proved by reuse. The (heuristic) control of this recursion for avoiding non­ termination by cyclic reuses is subject to future work.

Another future topic is concerned with the manage­ ment of learned schematic proofs for an efficient se­ lection of the proof shell which is to be reused for a given, new conjecture. For the subtask of choosing a matcher between the schematic and the new conjecture we may adapt the above heuristics for rating second­ order matchers.

Acknowledgements. We thank J. Brauburger, S. Gerber­ ding, J. Giesl and M. Protzen for comments and discussions.