Meta-level inference: Two applications

Journal of Automated Reasoning 4 (1988) 15-27. (f~ 1988 by Kluwer Academw Publishers.

15

Meta-Level Inference: Two Applications ALAN

BUNDY

and L E O N S T E R L I N G *

Department of Artificial Intelhgence, Universuy of Edinburgh, Scotland (Received: 9 July 1986, Revised: 24 April 1987) Abstract. We describe two uses of meta-level inference: to control the search for a proof; and to derive new control information, and illustrate them in the domain of algebraic equation solving. The derivation of control information is the main focus of the paper. It involves the proving of theorems m the Meta-Theory of Algebra. These proofs are guided by meta-meta-level inference. We are developing a meta-metalanguage to describe formulae, and proof plans, and have built a program, IMPRESS, which uses these plans to build a proof. We describe one such proof plan in detail. IMPRESS will form part of a self-improving algebra system.

Key words: PRESS, IMPRESS, meta-level inference, proof plans, search control, theorem proving, algebra, verification, automatic programming, learning.

1. Introduction In [3] we described the notion of meta-level inference, and used it as a technique for controlling search. We also speculated about how it might be used as a technique for deriving new control information. In this paper we describe work in progress to explore this second application of meta-level inference. The domain used to illustrate these ideas is equation solving. In [3, 11] the PROLOG program, PRESS**, is described. PRESS successfully solves a wide range of equations of the difficulty of the UK GCE A-level mathematics papers. It uses meta-level inference to guide carefully the application of sets of rewrite rules. Without such guidance it would become hopelessly bogged down in a combinatorial explosion. PRESS clauses can be interpreted as axioms and theorems of the Meta-Theory of Algebra. Inference, in this mathematical theory, has the side effect of applying rewrite rules to algebraic expressions, and, hence, solving equations in the object-level domain of Algebra. We have built a PROLOG program, IMPRESS *, which proves properties of PRESS procedures by deriving theorems in the Meta-Theory of Algebra. The same technique of meta-level inference is being used to guide the search. For IMPRESS the object-level entities are PRESS clauses, and the meta-level entities are methods for proving properties of them. The PROLOG clauses which implement these IMPRESS methods can be regarded as axioms and theorems of the Meta-Meta-Theory of Algebra. * Current address: Department of Computer Engineering and Science, Case-Western Reserve University, Cleveland, OH 44106, USA. ** PRolog Equation Solving System. Inferring Meta-knowledge about PRESS.

16

ALAN BUNDY AND LEON STERLING

IMPRESS was intended as part of a larger program designed to make PRESS into a learning program. Such a program might begin by being shown examples and non-examples of rules satisfying the syntactic criteria of a particular method. It would also be shown examples and non-examples of when this method should be used, from which it would produce a PRESS clause to control the use of the method. We have experimented with a version of Winston's arch learning program for this task [13, 14, 4]. IMPRESS would then try to establish properties of this method, thereby demonstrating that the correct information had been learnt, and perhaps pointing to exceptions not covered by the examples. Finally the new method would be incorporated into PRESS. The technique of meta-level inference is perhaps best illustrated on an example. As a running example, throughout this paper, we will use the equation-solving method of I s o l a t i o n . A simplified axiomatization of Isolation will illustrate guided search when solving equations; while the correctness of Isolation, as a theorem in the Meta-Theory of Algebra, will illustrate the new control information that IMPRESS can derive.

2. A Method for Solving Equations Isolation is a method for solving equations containing only a single occurrence of an unknown. That is, Isolation can solve for x: logs,.x2 cosa

= tana

(i)

but not: e s'nx + ec~

=

5

Since the latter contains two occurrences o f x . Isolation is a key method because many solutions work by reducing equations to a form in which there is only one occurrence of the unknown, and then applying Isolation. The method consists of 'stripping off' the functions surrounding the single occurrence of x by applying the inverse function to both sides of the equation. This process is repeated until x is isolated on one side of the equation, e.g. lOgsmx2 c o s a

sin x 2 =

=

tana

(cos a) I/tana

x2 =

180n + ( - 1 ) n a r c s i n ( c o s a ) j/t~a

x =

x/180n + ( - 1)n arcsin (cos a) I/'a"a

x =

- x / 1 8 0 n + ( - 1)~ arcsin (cos a) I/ta"a

or

This stripping off is done by applying a system of rewrite rules to the equation, in this case the rules: loguv : sinu u2

=

w ~ u =

=

v ~ u =

v

u--

v ~/w

180n + ( - 1 ) narcsin(v) or

u--

META-LEVEL INFERENCE: TWO APPLICATIONS

17

All rules used by Isolation have the same general form, namely P & F(U1 . . . .

U, . . . .

U,)

=

V--* Rhs

where: P is an optional condition; and Rhs is usually o f the form U, = F , ( U I , . . . V, . . . . U,), but can also be a disjunction o f such formulae, where F, is the ith inverse function o f F.

3. The M e t a - T h e o r y o f Algebra Isolation is implemented in P R E S S by a series o f clauses defining the ternary predicate, isolate, where isolate(Posn, Lhs = Rhs, X = A n s ) means that expression X = A n s * is the result o f isolating the subterm at position Posn in expression Lhs. The position o f a subterm in an expression is a list o f numbers which specifies the arguments it lies within (see Figure 1). Interpreted declaratively, P R E S S clauses can be regarded as axioms or theorems in the M e t a - T h e o r y o f Algebra. F o r example, the clause which invokes the Isolation m e t h o d can be interpreted as the theorem: single-occ(X, Lhs = Rhs) & position(X, Lhs, Posn) & isolate(Posn, Lhs = Rhs, X = A n s ) ~ solve(Lhs = Rhs, X, X = A n s )

(ii)

where: 9 single-occ(X, Exp) means, X occurs precisely once in Exp; 9 position(X, Exp, Posn) means, X occurs at Posn in Exp; 9 solve(Eqn, X, Soln) means, Soln solves Eqn for X.

log

z

ns

con

^

a

I

2 Fig. 1.I. The posltlon of x in 1ogs,n~COSa.

* Throughout the paper we use the PROLOG convention that words beginning with capital letters denote variables. In the Meta-Theory of Algebra, algebraic (object-level) variables are represented as (meta-level) constants. Thus v is a meta-level constant representing an object-level variable, whereas V is a meta-level variable ranging over object-level variables. Note that this avoids the use/mention ambiguity, because we cannot apply meta-level substitution to object-level variables.

18

ALAN BUNDY AND LEON STERLING

As a theorem of the Meta-Theory of Algebra, (ii) asserts that when an equation contains only a single occurrence of Xthen Isolation is guaranteed to solve it. We will call this theorem The Correctness of Isolation and will use it as an example of a program property that IMPRESS can prove. Some typical axioms of the Meta-Theory of Algebra are the definitions of solve and isolate: solve(Eqn, X, X = Ans) ~-~ equiv(Eqn, X = A n s ) & free-of(X, Ans) isolate([ ], Soln, Soln) isolate([CarlCdr], L = R, Soln) ~ 3L'R'[isolax(Car, L = R, L' = R') & isolate(Cdr, L' = R', Soln)] (iii) where: 9 equiv(Forml, Form2) means, Forml and Form2 are equivalent algebraic formulae; 9 free-of(X, Exp) means, Exp contains no occurrences of X; 9 isolax(N, Lhs, Rhs) means, Lhs ~ Rhs is an Isolation rules which isolates the Nth argument position of Lhs. The definition of solve is derived from a PRESS clause, but would be available to IMPRESS. The definition of isolate is a cleaned-up and simplified version of the PRESS clauses which define the Isolation method. The simplifications are that we have decided to ignore Isolation rules with disjunctive right hand sides and those with conditions, and to assume that the single occurrence of the unknown is always on the left hand side of the equation. IMPRESS can prove (ii) from the above axioms and some lemmas stated below.

4. Using Meta-Level Inference to Control Search We now show how the clauses of the last section are used, by PRESS, to solve equations. Suppose we want to solve (i) above for x. This would be presented to PRESS as the goal: solve(log(sin(x ^ 2), cos(a)) = tan(a), x, Soln) This would be resolved against (ii) to produce the subgoals: single-occ(x, log(sin(x ^ 2), cos(a)) -- tan(a)) & position(x, log(sin(x'2), cos (a)), Posn) & isolate(Posn, log(sin(x^2), cos(a)) = tan(a), Soln) After the first two subgoals had been resolved away using the definitions of single-occ and position, and binding Posn to [1, l, 1], the last subgoal would be called. This would resolve with the recursive definition of isolate to produce the subgoals: isolax(1, log(sin(x^2), cos(a)) = tan(a), L' = R') & isolate([1, 1], L' = R', Soln) -~

META-LEVEL INFERENCE: TWO APPLICATIONS

19

The first of these subgoals would resolve with only one of the pre-stored Isolation rules, namely ~isolax(1, log(U, V) = IV, U = V^(1/W)) binding L' to sin(x ^ 2) and R' to cos(a)^(l/tan(a)). This latest meta-level resolution implicitly applies a rewrite rule to an algebraic expression, thus making a move in the object-level search space. The proving of the remaining isolate subgoal will cause two more such moves to be made, before the meta-level inference terminates, having caused the solving of the equation as a side effect.

5. Using Meta-Level Inference to Derive Control Information Following our experience with PRESS, we have adopted the technique of meta-level inference to guide the search for a proof of (ii), but in this case we have a process of meta-meta-level inference guiding a meta-level search space. The Meta-Meta-Theory of Algebra deals with the representation of the Meta-Theory of Algebra as predicate calculus formulae. In order to guide the proof, the meta-meta-theory makes crucial distinctions between the parts of(ii) and (iii). The main parts of(ii) are the antecedent,isolate(Posn, Lhs = Rhs, X = Ans), and the consequent, solve(Lhs = Rhs, X, X = Ans). The remaining parts, single-occ(X, Lhs = Rhs) & position(X, Lhs, Posn), form the preconditions. The theorem is to be seen as the antecedent implying the consequent provided the preconditions are true. We expect these distinctions to be supplied by the Winstontype concept learning program as a consequence of the task of learning the preconditions under which the antecedent part could be used to derive the consequent part. (iii) is the step case of the recursive definition of isolate. Its main parts are the head, isolate([CarlCdr], L = R, Soln), and the body, 3L'R'[isolax(Car, L = R, L' = R') & isolate(Cdr, L' = R', Soln)]. The body is divided into two sub-parts: the recursive call of isolate, isolate(Cdr, L' -- R', Soln), which we call the recursant; and the part of the body that does the work on each recursive call, isolax(Car, L = R, L' = R'), which we call the performant. To form a strategy to prove (ii), our proof plan analyses the antecedent, isolate(Posn, Lhs = Rhs, X = A n s ) . This relation is recursively defined on the list structure of its first argument, Posn. The strategy formed is to try a proof by induction on the Posn argument using the simple list induction scheme associated with the recursive definition of isolate. This reasoning is in the same spirit as that of the Boyer-Moore theorem prover [1] when proving properties of LISP functions.* * In fact, in order to make comparisons, we have built and experimented with a toy version of the Boyer-Moore theorem prover, written in P R O L O G . Both this, and our not so toy version of Winston's program, have proved easy and quick to implement in P R O L O G : the implementations being both small and fast.

20

ALAN BUNDY AND LEON STERLING

The plan involves forming two subgoals: the base and the induction conclusion of the induction, by substituting [ ] and [nlposn], respectively, for Posn in negated and skolemized versions of (ii)

B ase: single-occ(x, lhs = rhs) position(x, lhs, [ ]) --,isolate([ ], lhs = rhs, x = a n s ) solve(lhs = rhs, x, x = ans)

Induction Conclusion: --*single-occ(x, lhs = rhs) position(x, lhs, [nl posn]) isolate([nlposn], lhs = rhs, x = a n s ) solve(lhs = rhs, x, x = ans) The base subgoal is easily proved, since the precondition, position(x, lhs, [ ]), implies that lhs is x, and together with single-occ(x, lhs = rhs), that rhs is free of x. Hence lhs = rhs is already a solution for x. To prove the induction conclusion, (ii) with posn for Posn, is asserted as the induction hypothesis. T h a t is, the new t e m p o r a r y axioms are:

Induction Hypothesis: single-occ(X, Lhs = Rhs) & position(X, Lhs, posn) & isolate(posn, Lhs = Rhs, X = A n s ) ~ solve(Lhs = Rhs, X, X = A n s ) Induction Conclusion Preconditions: -,single-occ(x, lhs = rhs) position(x, lhs, [nlposn]) Induction Conclusion Antecedent: -~isolate([nlposn], lhs = rhs, x = ans) Induction Conclusion Consequent: solve(lhs = rhs, x, x = ans) In order that the induction hypothesis can be used, the plan is to unfold the induction conclusion antecedent and conclusion* into their p e r f o r m a n t s and recursants. F r o m (iii), the recursive definition o f isolate, we can see that the p e r f o r m a n t and recursant o f the antecedent are:

Performant: isolax(n, lhs = rhs, lhs' = rhs') Recursant: ~ i s o l a t e ( p o s n , lhs' = rhs', x = ans) * Strictly speaking the antecedent is unfolded but the conclusion isfolded. This is because the conclusion is negated, so the direction of inference is from performant and recursant to conclusion (see Figure 4).

META-LEVEL INFERENCE: TWO APPLICATIONS

21

There is no recursive definition of solve, but there is a lemma of the appropriate syntactic form, namely: solve(New, X, Soln) & equiv(Old, New) ~ solve(Old, X, Soln) We call this a pseudo-recursive definition, and the plan is able to use this to generate the pseudo-performant and pseudo-recursant: Pseudo-Performant: equiv(lhs = rhs, Eqn) & Pseudo-Recursant: solve(Eqn, x, x = a n s ) The plan then resolves the pseudo-recursant with the induction hypothesis to get: single-occ(x, Lhs = Rhs) & position(x, Lhs, posn) & isolate(posn, Lhs = Rhs, x = ans) & equiv(lhs = rhs, Lhs = Rhs) ~

(iv)

The plan is to prove the induction hypothesis antecedent, i.e. the isolate subgoal of (iv), with this recursant. This binds Lhs' to lhs' and Rhs' to rhs'. The plan also entails proving each of the remaining three subgoals from the performant, with the aid of the corresponding induction conclusion precondition in the case of the precondition type subgoals. These plan constraints are so strong that they can be used to conjecture the lemmas needed to complete these sub-proofs, namely: isolax(N, Lhs = Rhs, Lhs' = Rhs') & single-occ(X, Lhs = Rhs) single-occ(X, Lhs' = Rhs') isolax(N, Lhs = Rhs, Lhs' = Rhs') & position(X, Lhs, [N]Posn]) position(X, Lhs', Posn) isolax(N, Lhs = Rhs, Lhs' = Rhs') ~ equiv(Lhs = Rhs, Lhs' = Rhs') In each case these conjectures are theorems of the Meta-Theory of Algebra. We have supplied them as axioms in our IMPRESS implementation. This completes the proof. The above example illustrates the (meta-meta-level) language we have developed for describing parts of formulae, and how they can be used to guide a proof search. This parallels the (meta-level) language that we developed to describe algebraic expressions, and used to guide equation solving. Such a language is the essence of the meta-level inference search-control technique. We have introduced the concepts of: precondition, antecedent and consequent; base, induction hypothesis and induction conclusion; and performant and recursant. We have illustrated: how an induction scheme and variable are chosen using the recursive definition of the conjectures's antecedent; how the induction conclusion consequent is transformed to allow the induction hypothesis to be applied; and how, after the induction hypothesis has been applied, the remaining subgoals are proved by using either the performant or the recursant of the recursive definition of the conjectures's antecedent. Further examples can be found in [10, 2, 9].

22

ALAN BUNDY AND LEON STERLING

Thus the language enables a proof plan to be built which then supervises the search for a proof. This proof plan is so explicit that it can specify the precise form of the lemma required to enact a particular part of the proof. These terms and the proof plan were induced from a number of similar examples and consideration of the general properties of recursive definitions, inductive proofs and mathematical theorems. This proof plan is described in the next four sections: Section 6 describes what information must be given or derived about the problem for the plan to operate: Section 7 describes the overall plan; Section 8 gives more detail of the step-case of the plan; and Section 9 discusses its implementation in the IMPRESS system.

6. Prerequisites for the Plan The plan has as prerequisites the association of various pieces of meta-level information with each recursive definition, as follows.

6.1. A S S O C I A T E D I N D U C T I O N S C H E M E

Associated with each recursive definition is an induction scheme, e.g. see Figure 2. The correct association is intuitively obvious and we might hope, eventually, to automate the production of the induction scheme from the recursive definition.

6.2. P E R F O R M A N T A N D R E C U R S A N T

Identify the performant and recursant in each step-clause of the recursive definition, e.g. see Fig. 3. It may also be possible automatically to extract the performant and recursant from a recursive definition. Recursive Definition

Induction Scheme

isolate([ ], Soln, Soln)

Q([ l) & VCarCdr{Q(Cdr) ~ Q([CarlCdr]) } --*~' List Q(List)

isolate([Carl Cdr], L = R, Soln) 3L'R'{isolax(Car, L = R, L' = R') & isolate(Cdr, L' = R', Soln)} Fig. 2.

The Association between Recursion and Induction.

Step-Clause

Performant

Recursant

isolax(Car, L = R, L' = R')

isolate(Cdr, L' = R', Soln)

isolate([CarlCdr], L = R, Soln) 3L'R'{isolax(Car, L = R, L' = R') & isolate(Cdr, L' = R', Soln)} Fig. 3.

The Performant and the Recursant.

META-LEVEL INFERENCE: TWO APPLICATIONS

23

7. Overall Proof Plan We are now in a position to discuss the proof plan itself. In this section we discuss the overall proof plan including the analysis of the conjecture and the discovery of a suitable form of induction. In Section 8 we discuss the step case in detail. The overall proof plan is as follows: 1. Find a suitable structural induction scheme. 2. Prove the base case. 3. Prove the step case. This can be realized by the following meta-meta-rule: structural-induction(Conjecture, Scheme) & prove-base-case(Conjecture, Scheme) & prove-step-case(Conjecture, Scheme) prove-by-induction(Conjecture) To execute the plan this meta-meta-rule can be used backwards, just as the metarule, (ii), is in Section 4. Each of the literals to the left of the arrow is defined by further meta-meta-rules. Thus meta-level inference can be used to execute the induction proof plan. A meta-meta-rule defining the prove-step-case sub-plan is given in Section 8. The prove-base-case sub-plan is further described in [9]. The structural-induction sub-plan finds a suitable scheme to perform structural induction. A description of this induction scheme is given in [10]. This sub-plan can be summarised as follows. The conjecture is assumed to be a Horn clause, i.e. of the form: PI & . . . & P n - - * Q

(a) Let Pn be the antecedent and the remaining P,s be the preconditions. (b) Assume that Pn is defined recursively on the arguments Xl . . . . xm. (c) Find the induction scheme associated with this recursive definition. This analysis is similar to and based on the work of Boyer and Moore [1], but their analysis is more complex and handles more cases.

8. Step-Case The idea of the step-case of the plan is that the induction conclusion is negated and clausified into a set of n positive unit clauses, from the antecedent and preconditions, and 1 negative unit clause, from the consequent. This negative clause is the goal clause, and is established from the n positive clauses and the induction hypothesis.

24

ALAN BUNDY AND LEON STERLING

These are presented as the first and last rows of Figure 4, where: IH IC A P C Pf Rc

abbreviates abbreviates abbreviates abbreviates abbreviates abbreviates abbreviates

induction hypothesis. induction conclusion. antecedent. precondition. consequent. performant. recursant.

The link between the induction conclusion and the induction hypothesis consists of a single step followed by a recursion - represented by the rows marked 'step' and 'recursion', respectively. The fillers of these rows are derived clauses of the proof, e.g. the fillers of squares (antecedent, step) and (antecedent, recursion) are the result of unfolding ~ I C - A with its recursive definition. The double arrows (=~) indicate the direction of implication between the various formulae in the diagram. These implications may be performed backwards or forwards and may take 0 or more steps. They involve either rewriting or resolution. Figure 4 divides the step-case proof into the major parts listed below. The numbers labelling this list correspond to the numbers in the figure. 1. Unfold the induction conclusion antecedent into its performant and recursant. 2. Fold the induction conclusion consequent into its performant and recursant. 3. Establish the induction conclusion consequent performant from the induction conclusion antecedent performant. 4. Apply the induction hypothesis to the induction conclusion consequent recursant to produce the induction hypothesis precondition and antecedent. 5. Establish the induction hypothesis antecedent from the induction conclusion antecedent recursant. 6. Establish each induction hypothesis precondition from the corresponding induction conclusion precondition and its antecedent performant. Preconditions Induction Conclusion Step

--)IC-P 6

Consequent

1~ 3"-) IC IC-A

IC-Cc~c. -'') 2 ~j ',,I

Recursion Induction Hypothesis

Antecedent

IH-P & Fig. 4.

--~IC-A-Rc

IC-C-Rc

IH.A ~ ._~

IH.14C

Proof plan of step-case.

--~

META-LEVEL INFERENCE: TWO APPLICATIONS

25

This can be realised by the following meta-meta-rule: ind-hypothesis(Conjecture, Scheme, IH-C, IH-A, IH-P-List) & ind-conclusion(Conjecture, Scheme, IC-C, IC-A, IC-P-List) & unfold(IC-A, IC-A-Pf, IC-A-Rc) & unfold(IC-C, IC-C-Pf, IC-C-Rc) & establish(IC-C-Pf, [IC-A-Pf]) & resolve(IH-C, IC-C-Rc) & resolve(IH-A, IC-A-Rc) & V(IH-P, IC-P) e (IH-P-List, IC-P-List) establish(IH-P, [IC-P, IC-A-Pf]) ~ prove-step-case(Conjecture, Scheme) The first two literals of this meta-meta-rule identify the appropriate meta-level formulae with which to conduct the proof. The remaining six literals are in one-one correspondence to the double-arrowed steps in Figure 4 and the above list of major proof parts. 9 unfold(Lit, Pf, Rc) means that the result of unfolding the recursively defined literal, Lit, is the performant, Pf, and the recursant, Rc. It also means that the result of folding Pf and Rc is Lit.* 9 resolve(Goal, Hypothesis) means that the clause containing the literal Goal can be resolved with the clause containing the literal Hypothesis. 9 establish(Goal, Hypotheses) means that Goal can be proved from Hypotheses with the aid of axioms of the meta-level theory.

9. The IMPRESS System A simplified version of the proof plan described in Sections 7 and 8 above has been implemented to the IMPRESS program. Roughly each meta-meta-rule corresponds to a PROLOG clause; the collection of these clauses constitutes IMPRESS. This mapping of the plan directly onto PROLOG code is a natural and simple way of realising it. However, it carries the disadvantage that the execution of the plan is carried out by the PROLOG interpreter. This makes it inflexible. For instance, the steps in Figure 4 are executed in a fixed order and direction; the failure of one step causes a failure of the whole plan, with no attempt at graceful recovery, for instance, the finding of an alternative sub-proof. We are currently experimenting with more flexible representations of proof plans. In addition to the correctness of isolation ((iii) above), IMPRESS has proved a variety of other theorems. Each of them can be interpreted as describing properties of PROLOG programs. Further examples are: list(X) & list(Y) & append(X, Y, Z) ~ list(Z) length(X, M) & length(Y, N) & append(X, Y, Z) ~ length(Z, M + N) * i.e., no separate fold predicate is required since fold and unfold differ only in the direction of the meta-level implication.

26

ALAN BUNDY AND LEON STERLING

IMPRESS uses the constraints of the plan to conjecture lemmas that are needed to complete the proof. For examples of the need for this see Section 5.

10. Related Work The Edinburgh LCF program [7] and the Cornell NuPRL [5] program are computer systems for doing formal proofs interactively. These systems provide an object-level deductive system and a meta-level language, ML, for controlling it. The emphasis of both systems is to provide an interactive facility for human/computer derivation of proofs. IMPRESS, on the other hand, has no such interactive facility. Development is concentrated on generating proofs automatically, according to explicit proof plans. Our current plans are to implement our proof plan as an ML program for NuPRL and to try to extend significantly the machine contribution to the proof process in NuPRL. Other important proof strategies are contained in work on program transformations. Darlington [6] gives a meta-language vocabulary for describing and controlling such transformations. His basic manoeuvres, for example fold/unfold, have been incorporated into our proof plan. However, his program has no a priori representation of proof plans comparable to ours. We have also built on the work of Boyer and Moore [1]. The selection of a suitable induction scheme and variable by analogy with the recursion scheme and variable is based on their work. Our step-case plan extends some of the ideas embedded in the Boyer-Moore system, in particular the mechanism for controlling the proof of the preconditions and the separation of recursive definitions into performant and recursant. A more detailed comparison can be found in [2]. Much of the knowledge of the Boyer-Moore program, however, is embedded implicitly in code. For example, much implicit reference is done when type checking at an early stage of a proof. Our emphasis is more on developing a language to describe proof plans. The possibility is then open to learn new plans from worked examples (cf. [8]), to interpret these plans in a flexible way, (cf. [12]), and to prove their correctness.

11. Summary We have described two applications of meta-level inference: to control inference; and to derive new control information. We have illustrated these applications in the area of algebraic equation solving. New control information can be derived by proving theorems in the Meta-Theory of Algebra. To control the search for such proofs we are developing a meta-meta-level language, and expressing proof plans in this language. A program, IMPRESS, has been built which incorporates a simple version of this proof plan and uses it to guide the search for inductive proofs. This proof plan builds on and extends earlier work on controlling search in the proof of program properties.

META-LEVEL INFERENCE: TWO APPLICATIONS

27

Acknowledgements Early versions of this paper were presented at the Workshop of Logic Programming for Intelligent Systems, Los Angeles, 1981 and at the CAPRI-85 Conference, Capri, 1985. We are grateful to members of the audience at these conferences and to members of the mathematical reasoning group at Edinburgh for feedback and discussion. In particular, Robert Desimone commented on the final draft. This research was supported by SERC grants GR/B/29252 and GR/C/20826. References 1 Boyer, R. S. and Moore, J S., A Computattonal Logic, Academic Press, ACM monograph series (1979). 2. Bundy, A., The Impress Proof Plan Revisited, Working paper 138, Dept. of Artificial Intelligence, Edinburgh (April, 1983). 3. Bundy, A. and Welham, B., 'Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation', Artificial Intelligence 16(2), 189 212 (1981). Also available as DAI Research Paper 121. 4. Bundy, A., Silver, B, and Plummer, D., 'An Analytical Comparison of some Rule Learning Programs', Artificial Intelligence 27(2), 13~182 (1985). Also available from Edinburgh as DAI Research Paper no. 215. Earlier version in Procs. of Third Annual Technical Conference of the British Computer Society's Expert System Specialist Group (1983). 5. Constable, R. L et al., Implementing Mathematics with the NuPrl Proof Development System, PrenticeHall (1986). 6. Darlington, J., 'An Experimental Program Transformation and Synthesis System', Artifictal Intelligence 16(3), 1 46 (August, 1981). 7. Gordon, M. J., Milner, A. J., and Wadsworth, C. P., Lecture Notes m Computer Science, Volume 78: Edinburgh LCF-A mechanised logtc of computation, Springer Verlag (1979). 8. Silver, B., 'Precondition Analysis: Learning Control Information', in: Miehalski, R. S., Carbonell, J. G., and Mitchell, R. M. (eds.), Machine Learning 2, Tioga Publishing Company (1984). 9. Sterling, L., IMPRESS - Meta-level concepts in theorem proving, Working Paper 119, Dept. of Artificial Intelligence, Edinburgh (August, 1982). 10. Sterling, L. and Bundy, A., 'Meta-level Inference and Program Verification', m: Loveland, D. W. (ed.), 6th Conference on Automated Deduction, pp. 144-150, Springer Verlag (1982). Lecture Notes m Computer Science No. 138. Also available from Edinburgh as Research Paper 168 11. Sterling, L., Bundy, A., Byrd, L., O'Keefe, R., and Silver, B., 'Solving Symbolic Equations with PRESS', in: Calmet, J. (ed.), Computer Algebra, Lecture Notes in Computer Scwnce No. 144, pp. 109116, Springer Verlag (1982). 12. Wallen, L. A., Towards the Provision of a Natural Mechanism for Expressing Domain-Specific Global Strategies in General Purpose Theorem-Provers. Research Paper 202, Dept. of Artificial Intelligence, Edinburgh (September, 1983). 13. Winston, P., 'Learning structural descriptions from examples', in: Winston, P. H. (ed.), The Psychology of Computer Viston, McGraw-Hill (1975). 14. Young, R. M., Plotkm, G. D., and Linz, R. F., 'Analysis of an extended concept-learning task', m: Reddy, R. (ed.), Proceedings of IJCAI-77, International Joint Conference on Artificial Intelligence (1977).