Solving "How to Clear a Block" with Constructive Matching Methodology

1 Introduction

In [Franova, 85] we have developed a methodology, called Constructive Matcli.ina (CM), for proving by induction Specification Theorems, i.e., theorems of the form Vx 3z (P(x) => Q(x,z)). These theorems formalize program synthesis as follows. Given input vector x verifying the input condition P(x), find an output vector z such that the input-output relation Q(x,z) holds. Practical reasons, such as the availability of examples and implementation limitations, led us to restrict our method to particular inductively constructed sets, called Constructi6fe 'DomtJins (CD). These are specified by their constructors, enabling new elements to be built from old ones and, possibly, from elements of an already defined domain. In CD each element has a unique representation in terms of constructors. This amounts to saying that we do not allow relations among constructors.

E.g., the set of natural numbers (?bt'f) can be considered as a CD with constructors 0 and a. This gives us the domain ?(}1.'1" = {0, s(O),a(s(O)), ... } which may be identified with the familiar sequence of integers { 0, 1, 2, ... }. Each element x of $'Tis either 0 or can be written as a(y), where y is an element of ?(}1.'1". In the following, we shall call a(y), a representative of x, and y a subrepresentative of x.

More generally, we call y a subrepresentative of x if it has the form :C = Constructor(y).

1 This research has been partly supported by the Programm~~ th Recherches Coordol'lies en /fllelligence Artif~eielle from the French Ministere de Ia Recherche et th Ia Teclanologie. It is a shortened venion of [Franova UJd Kodratoff, 91a).

2 Using this problem, Manna and Waldinger show the interest of the deductive approach for the synthesis of imperative programs that may alter data structures or produce other side effecu, UJd illustrate how program synthesis CUI be carried over to the plUJning domain. Our goal is the same as theirs, i.e., illultrating that our methodology CUI be also carried over to planning.

In this paper we enlarge our methodology to well-founded domains (WFD) that are not necessarily constructed with a help of constructors, and which may introduce EQV in the definitions. We explain in [Franova, 88a] that fmding a strat­ egy for a proof of an atomic formula is one of basic problems of mechanizing inductive proofs. We therefore limit ourselves here only to this particular problem, even if the simple example we solve here (Manna& Waldinger's "How to Clear a Block" problem [87]), illustrates our overall methodology.

2 eM-methodology

One of the main differences of our method, in comparison with other approaches in inductive theorem proving [Boyer and Moore, 79; Bundy et al., 90] is actually very deep since it takes place in the basic step of any theorem proving methodology, viz. in the way atomic formulae are proven. In [Franova; 88a] we have shown the consequences of the choices done at such a low level on the way subproblems are generated during the course of a complete proof.

Classical methods for proving by induction atomic for­ mula can be classified as simplifications (or rewrite) methods, i.e., they attempt to transform the atomic formula into simpler and simpler form, until the formula TRUE is reached.

Our method for proving atomic formulae can rather be qualified as a "complication" method, stressing so that we rather progressively build more and more large sets of con­ straints describing the condition at which the formula is TRUE. The proof is completed when these conditions are proven to be implied by those of the problem.

We call our way of proving an atomic formula a Constructive 'Matcli.ina formula construction, or C'M· formula construction.

Let us give a brief motivation for this name. IfF is an n-place predicate symbol and t 1 , ·· · , t,. are terms, then F(t 1 , ··· , t,.) is an atomic formula. This definition of an atomic formula shows that an atomic formula is "constructed", or "build up", from a predicate name and terms in the following manner: We take an n-place symbol F providing the syntactical scheme F( _ , _ , ... , _ ), where "_" represent empty positions (or arguments) to be filled up by concrete terms, so that finally F(tl' ... , t,) is obtained. In classical thinking, this process of "filling up" empty argument places is mentally performed in one step, i.e., we start from F( _ , ... , _) and reach immediately F(tp ... , t,).

As opposed to this one step operation, we consider a piec~wise construction of an atomic formula. We start with the syntactical scheme F( _ , ... , _). We then take the first term t 1 and we fill up the first empty argument of our scheme by this term, so we have F(~, _ , ... , _ ). Then, we fill up the first empty argument in the last scheme by ~. obtaining F(t 1 , ~ ···· , _ ), etc.

We thus construct (purely syntactically) in n steps the formula F(tl' ... , t,). However, in theorem proving, we need to speak of the validity of a given formula in a theory T made from the axioms. This is why we will consider axioms defming the predicate F. These axioms allow us to change the above syntactical construction into a construction which, if successfully performed, provides a proof for F(tp ... , t,).

5 [Boyer and Moore, 79) is an example of a simplification method.

Let us show briefly how axioms are involved in the process of our construction of an atomic formula F(~.~. created from a predicate F and two terms ~ and ~· i.e., n = 2. The order of filling up arguments depends now on given defmitions. For simplicity, we suppose here that definitions involved indicate that ~ has to be filled up fmt The eM­ formula construction can then be briefly described as follows.

We start by building an abstract formula F(~.~) with an abstract argument ~. i.e., instead of considering an empty argument place, we take a variable which has a special character since it does not occur in F(~.~. and moreover it represents (or, equivalently, is an abstraction of) all terms which can fill up the empty argument of the scheme F(~,_) in order to obtain an atomic formula. Therefore, we call it an abstract argument in order to avoid confusing it with the quantified variables of the theorem.

Let us give a very simple example which shows also a cifference with the simplification approach, by proving the formula s(s(O)) < s(s(s(s(O)))) (written 2<4, for brevity), and using the following recursive definition of the precicate <:

The definition of · <" is recursive with respect to the first argument. This is why, in the formula 2<4, the second argument (i.e., non­ recursive) is replaced by an abstract argument~. Up to now, we have constructed purely syntactically the formula 2<~. without considering yet the vaNcity of this formula

Now, the definition of F provides conditions for the validity of the formula F(~.~). Let us denote by C the set of all~ for which F(~.~) is true, i.e., C= {~IF(~.~) is true}.

Using the definition of the predicate · <" we 2 < ~ see that any ~ that satisfies the formula 2<~ / ........_ must be of the form ~=s(u), where 1 <U, ~ = s(u) 1 < u therefore, u must be of the .form s(v) with O<v, / ........_ and therefore, using ( 1 ), v must be of the form u = s(v) 0 < v s(z). This yields the final form of ~ and so the / class of of all ~ that satisfy the formula 2~ is v = s(z) c .. {~/there exists z such that~ · S(s(s(z)))}. Note that we obtain c by unfolding [BurstaU and Darlington, 77J the formulae 2<~ , 1<u, O<v. For each of them we obtain conditions, that are collected and combined. The final step is the withdrawal of the new "abstract arguments· u, v which are recognized as being useless. This leaves ~ expressed in relation with a new variable-argument z.

In other words, we solve our problem in a top-down manner, pick up the fmalleaf {v=s(z))\ carry this bottom leaf up to the root of the tree. Durmg this Jast step, the final leaf is applied to all other leaves of the tree. The solution obtamed (in case of success) is given by the set of independent leaves in which the (mal leaf has been applied.

In our example, final leaf is V=s(z). It is applied successively to U=s(v) yielding U=S(s(z)), then to ~=·(u), yielding ~=s(s(s(z))). Therefore we have that the solution of our problem 2<~ is ~=s(s(s(z))).

We are then left with checking if the replacement of~ by ~ preserves the validity of F(tp~). i.e., we have to check whether ~e C

In our example, we have to check whether 4 belongs to c In fact, it does, since 4 = S(s(S(S(O)))), i.e., z = s(O).

The same problem is tackled by the simplification approach in a different manner:

Applying (2) to 2<4 leads to two subproblems. Firstly, it is necessary to show that there is an element b such that 4=s(b). Here, we succeed since b=3. Then it is necessary to prove 1 <3. In this step, our original problem, proving the formula 2<4- is replaced by another equivalent problem: Prove 1<3. One therefore "forgets· the original problem. Applying (2) to 1<31eads again to two similar subproblems. Firstly, it is necessary to show that there is an element b such that 3-8(b). Here, we succeed since b=2. Then it is necessary to prove Ck2. Here, once again we "forget· the fonnula 1 <3 and we concentrate our effort to the formula 0<2. Using (1) this simplifies to TRUE, because there is an element b (bz1) such that 2=8(b). This proves our original formula.

This simplification approach proves the formula in a top­ down manner, but the final leaf is TRUE in the case of success. Therefore, as opposed to our method, there are no final bottom-up steps in the simplification approach.

It may seem that our "constructive" method makes the proof more complicated (as compared to the simplification methods) without anything to gain. Recall, however, that simplification procedures have been developed for theorems without EQV. Therefore, our method which is suitable for specification theorems, is more powerful, even if it may seem more awkward and non-useful for theorems with universally quantified variables only. As compared to classical simplification thinking, it may seem also more artificial, because, by our method, we may generate an existentially quantified lemma when proving a universally quantified theorem. The simplification methods are built in such a manner that all the subproblems generated are universally quantified, while this restriction is not necessary to our eM-methodology.

Program synthesis methodologies ([Manna and Waldinger, 80; Kodratoff and Picard, 83; Bibel and HOrnig, 84; Dershowitz, 85; Smith, 85; Perdrix, 86; Biondo, 88]) do not consider the problem of strategy for proving an atomic formula as the main problem. In fact, these methods take the whole specification, say Q 1 (x,z) & ... & Qn(x,z), where Q1' ... ,QD are literals, and perform transformations on .this complex formula'. As opposed to such a treatment of a gtven specification, our method deals firstly' with Q 1 (x,z), performing the eM-formula construction it finds conditions for a validity of this formula. After this step has been completed, and assuming the conditions obtained, our method starts taking care of Q 2 (x,z), and so on, until the last literal ~(x,z) is treated.

Thus, as a summary, let us state that, in order to prove an atomic formula F(t1 .~. created from a predicate F and two term.s t 1 and tz, we start by building an abstract formula F(tp~) with an abstract argument ~. The definition ofF provides conditions for the validity of the formula F(~.~· Let us denote by C the set of all ~ for which F(~ .~) is true, i.e., C= {~IF(~.~) is true}. We are then left with checking if the replacement of~ by lz preserves the validity ofF(~.~). i.e., we have to check whether lz e C

3 eM-formula construction for WFD

In the previous section we pointed out that the main reason for performing the eM-formula construction is its suitability for }X'Oving specification theorems. We also described the way to proceed when a given specification is a conjunction of atomic formulae. Therefore, in this section, we shall concentrate on a specification theorem· Vx 3z Q(x,z), where Q(x,z) is an atomic formula Let us denote by ST 0 this theorem and by <JP the substitution {x .- p}, where pis smaller than x. Using the general induction principle and x being the induction variable, we have to prove { <JP(3z Q(x,z)) } ~ 3z Q(x,z).

' See [Franova, 91c] for more detailJ about differences between our method and the other proaram synthesis methods.

1 There are heuristics which suitably order literals in a given specification. For instance, if x is an input and z is an output, then the specification ordered(z) ol permut(x,z) is reordered to permut(x,z) ol ordered(z). Moreover, in such a reordered specificatioo, Q 1 (x,z) must be an atomic formula.

For this general induction principle scheme, we do not have a division into a base step and an induction step. From the computational point of view, however, it is interesting to "simulate" a base step for ST 0 , since we then obtain the non­ recursive parts of the desired programs.

3.1 Base step (a general outline)

One way to simulate a base step is done by using the tautology Q(x,t) => Q(x,t) as explained and exemplified in [Fmnova and Kodratoff, 91a].

Let us consider now the induction step, i.e., we try to find out recursive parts of the program.

3.2 Induction step solutions (a general outline)

During this step we shall perform the eM-formula construc­ tion presented in an intuitive way in section 2. For simplic­ ity, and in order to keep the notation of section 2, Q(x,z) will be called F(tplz)'. We suppose that F is defined in T recursively (at least) with respect to the frrst argument

As ~inted out in section 2, we start by building an abstract formula F(~.~) with an abstract argument~. Then

Step 1: We traluatt the term ~. i.e., we apply to t 1 axioms defming functions occurring m ~ until no further axioms can be applied. For brevity, we supp_ose here that t 1 is already evaluated, and that the evaluations yielded no I con_ititfon

Step 2: We evaluate F(tp~) in order to find conditions for the validity of the formula F(t.i).

With re~t to the recursive defmition ofF this step gives a composibon of the recursive call and some formul~ say G. We fiave F(tl'~) if comp(G,F(t,s)).

Here, it may hap~n that t in the recursive call is expressed in terms of new EQV 10 that do not apJ!eaf in ST. For instance, later we show that constructing the formula dear(~.b) (using the pu.t·ta6ft·cfuu axiom from section 4.2) leads to

Clear(~,b) if~= put'(w,x,table) & On(w,x,b) & Clear(w,x). This formula says that Clear(l;,b) is valid only if there is a state w and a block x sucli that l; can be written as put'(w~,table) and moreover if On(w,x,b) & Clear(w,x) holds. tnus x and ware existentially quantified, i.e., x and w are unspecified variables. The presence of such variables in a proof is not admissible, because it makes the proof to be a nonconstructive one. Therefore, during an actual proof we have to express unspecified variables m terms of variables given in ST 0 · Whenever we express a variable in terms of variables gtven in S'!P· we say that we concretize this variable, or, equivalenuy, we say that we try to make this variable more explicit. The following step is necessary only when such unspecified variables appear.

1 For simplicity, we assume here that the input condition P(x) is TRUE. ' Thus, we assume here that Q(x.z) is created from a binary predicate F ~ the terms t and 7

1 Remember /hat we call such EQV "unspecified variables" and that such variables are not possible for CD.

the atomic fonnulae of comp(�,F(t.~)). Clearly, in general, heuristics have to be developed here to choose the order in which the fonnulae from comp(�,F{t,~)) are examined. In section 4 we will follow one possible heuristic: The priority of fonnulae with a larger number of variables of ST 0 ·

This concretization of unspecified variables chariges F(t,~ to a new fonnula. say F(t',~.

Step 3: We now try to apply induction hypotheses in order to concretize 11 ·

Recall that 0'~ = { x +-- p } 1 where p is smaller than x.

The generic ronn of imfucuon hypotheses (IH) is

V'u O'PF(~(x,u),lz(X,U)).

The quantification here is due to a possible presence of universally quantified variables other than x in ST 0 · Thus, if ST 0 contains no other universally quantified variables, the fonn of IH is O'l(~(x),iz(x)). Attempting to apply IH leads to a comparison between F(t',~) and V'u 0' F(~(x,u),iz(x,u)), which, in general, yields the transfo~ational problem represented by the equations

The solution of this J>!Ublem allows the replacement of ~ by the more concrete element O'Plz(x,u). Let us denote this element by a. Therefore, the elements of the class for which the theorem is true, C are represented by a.

3u ( t' = O'Pt1(x,u)) & ( ~ = O'P~{x,u) ).

Step 4: Our goal is now to verify if tz belongs to c, i.e., we have to check if we can re lace a b

This is equivalent to J)erfonning a unification of a and tz modulo ilie theory T. Our C~-term construction perfonns this operation (see [Franova, 88b]).

I Step S: We bave to perform final simplifications.

The reader can now see that our fonnula construction is an algorithm which mechanizes a proof of an atomic fonnula, beCause a successfully completed construction provides a proof. On the other hand, thts construction is an algorithm, because we know what we want to obtain and how to obtain it.

• Cl Clearly, in order to fmd conditions for the validity of F(tp~) we evaluate F(~.~) using the definition ofF in the same way as the unfold operation [Burstall and Darlington, 77].
• Cl We know then that we have to awly induction hypotheses, so we generate equations comparing IH and the previously obtained expansion.
• Cl The success of the last equation solving problem allows the concretization of ~ by a more concrete a and allows at least the most trivial simplification, which is here eliminating recursion formulae from the obtained expansion.
• Cl We have then to replace a hx. tz, so we generate an equation between a and t 2 ·

4 Example: How to Clear a Block (HCB)

Here a plan for the problem 12 is specified as follows. The probiem is to clear a given block, where we are not told whether the block is already clear or, if it is known not to be clear, how many blocks are above it. We adopt here the plan theory develoPed by Manna and Waldinger [87] (fuither referred to as the mw-plan theory) for describing situational logic events in tenns of classical logics, and their notation.

11 Thus, in this step we try to concretize the abstract argument by expressing it in terms of variables of the theorem under consideration and/or of induction hypotheses corresponding to this theorem. It may happen that a given theory allows a direct replacement of ~ by something more explicit provided some condition C is verified. H C is TRUE and we succeed in petforming steps 4 and S of our procedure, then it means that the given theorem is provable without the use of induction. H Cis not TRUE, then we obtain a conditional solution which, in the case of specification theorems, provides non-recursive pf,rtl of programs (u illustrated in section 4).

a It is usumed that we are in a world of blocks in which objects are a table and blocks. These blocks are all the same size, so that only one block can fit directly on top of another. It is also a11umed that the robot ann may lift only one block at a time.

4.1 Notations

For a given blocks a, u and v

clear(a) is true if the block a is clear

on ( u, v) is true if the block u is on the object v

hat( a) is the block directly on a, if it extsts

put ( u, v) is the action which places block u on top of v

In situational logic we have to consider the value of a func­ tion or a predicate with respect to a state, i.e., we have to introduce an explicit state argument w for them. For example, f<r the predicate clear an<l the function hat we have

Clear(w a) is true if the block a is clear in state w

hat'(w,a) is the block on top of the block a in state w Actions are represented as functions that yield states; for example put'(w ,u,v) is the state obtained from state w by putting block u on object v.

4.2 Axioms for mw-plan theory

THE FUNCTION ":"

If s is a state and e an object, then s:e denotes the object designated by e in state s.

To any n-ary function symbol fa new n+1-ary symbol f is associated with the property

w:f(u 1 , ... ,u.) = f'(w,w:ul' ... , w:u.) {o6ju:t {in(_age) for example, a fixed block w:hat(u) can be expressed equivalently by hat'(w,w:u).

THE RELATION"::"

This relation is analogous to":", but the relation :: is for predicates. If sis a state and e is a propqsition, then s::e is a proposition denoting the truth-value designated by e in state s. E.g., s::clear(d) is true if the block s:d is clear in state s.

Analogously to the o6ju:t {in~e, the propositional Cin(..age linkage axtom IS introduced. To any n-ary predicate symbol r a new n+ 1-ary symbol R is associated with the property

w: :r(u 1 , ... ,u 8 ) = R(w, w: u 1 , ... ,w:u.) {propositionaC {in(_age) for example, s::clear(d) = Clear(s,s:d), i.e., s::clear(d) is true if the block s:d is clear in state s.

THE EXECUTlON FUNCTION ";"

If s is a state and p a plan, s;p denotes the state obtained by executing plan p m state s. E.g., s;put(a,d) is the state obtained by putting block a on _object d m state s.

Analogously to the above finl<Pgt axioms, the p!an. un(..age linkage axiom ts introduced. To any n-ary plan symbol g a new n+ 1-ary symbol g' is associated with the property

w;g(u 1 , ... ,u.) = g'(w,w:ul' ... , w:un) {pUi.n fi.n(..age) for example, w;put(u,v) = put'(w,w:u,w:v).

The empty plan A is talCen to be a right iientity under the execution function. This is fonnalized by the axiom.

{empty p!an.)

w;A = w

There are objects that do not depend on states considered. For instance, the constant table always denotes the same object. These objects are called rigid designators, i.e., an object u is a ritJii tksitJnator, if for all states w w:u = u {riaii le.sitfn.ator)

THE PLAN COMPOSITION FUNCTION ";;"

This notion of composing plans is introduced in the following way. If p 1 and p 1 are plans, p 1 ;; p is the composiuon of Pt. and p~ where it is understOOd tfiat p 1 is executed ftrst and men omy p 2 is executed. This is expresSed by the pCan. composition axiom

{plan. composition)

w;(pl;;pz) = (w;pl);pz for all states w and plans p 1 and p,.. For simplicity, the distinction between the composition function ;; and the execution function ; is ignored. We will write ; fot both and rely on context to malce the meaning clear.

Th1s composition is assumed to be associative.

(pl;pz);p3 =Pt;(pz;p3) (associatifJity) The empty p[an A is taken to be the identity under composition, 1.e., for all plans p A ;p = p ;A =P {U[entity)

4.3 Axioms for the blocks world

Facts about the block world and effects of actions are expressed as plan theory axioms. For simplicity, sort conditions sucb as state{w) are omitted. Variables are understood to be universally quantified.

If not Clear(w,y) then On(w,hat'(w,y),y) (hat) The hat axiom describes the following situation: If (in the state w) the blocky is not clear then theze is a block directly on{;

Clear(w ,x)

(pu.t·ta6u·on)

then On(put'(w,x,table),x,table)

The pu.t·ta6u·on axiom allows to put a block x (in the state w) on the table whenever xis a clear block, i.e., if there is no block directly on x.

If On(w,x,y) & Clear(w,x) (pu.t·ta6u-cuar) then Clear(put'(w,x,table),y)

The pu.t·ta6u-ckar axiom describes the following situation: If (in the state w) the block xis directly on the blocky and if x is a clear block, then y becomes a clear block when we put x on the table.

Even if the given axioms could suggest that we might defme constructors hat (for objects) and put (for actions), the given domain is nonconstrucuble~ because the ~ven axioms mtroduce new EQV (see section 1,, such as w arid x.

4.4 Specification Theorem for HCB

The problem to clear a given block is expressed as: 'Vs 0 'Vb 3z 1 Clear(s 0 ;zl'b).

As in [Manna and Waldinger, 87], we denote the Skolem function corresponding to this ST by malceclear,. i.e., we try to find a function rnakeClear such that z 1 = makectear(s 0 ,b).

4.4.1 Choice of induction variable

The variable b is chosen as the induction variable.

4.4.2 Generating IH

Using the general induction principle scheme, we generate the induction hypothesis in the state s 0

Here L is an uns~ified yet well-founded ordering. During the actual proof, we shall need to assert that tlie objects are indeed in such a relation, thus defining the well­ founded ordering, on the fly, so to speak. If the recursive functions we start from are really computable, they should be associated to an existing well-founded ordering, which is exactly the one we are thus discovering.

Now, we will follow the algorithm described in section 3. To Fin the scheme corresponds Clear, to t 1 corresponds b, to tz corresponds s 0 ;z 1 ·

4.4.3 eM-construction of Clear(s,;z 1 ,b)

4.4.3.1 Base step solutions

This means that we try to construct the formula Clear(~;z1,b) (i.e., find a valu~-~J. for which the last formula is true) usmg the tautology Cleaf\~,b)~Clear(~,b). The part of code we extract in this step [Franova and Kodratoff, 9la] is makeclear(So,b) =A, if Clear(s 0 ,b).

4.4.3.2 Induction step solutions

We try to construct the formula Clear(s 0 ;z 1 ,b) (i.e., find a value z 1 for which the last formula is true) usmg fH.

Step 1: The term b is already evaluated.

~teP 2: The definition of Clear gives conditions or the validity of the formula Clear(~.b) (1)

The only axiom which leads to a formula of the form Clear( ... ) is pu.t·ta6u-ckar. In order to be able to apply it, we have to compare (1) and Clear(out'(w,x,table),y), where w, x, y_ are umversally quantified. Companng (1) and Oear(put'(w,x,table),y) feads to the equation solvmg

~ = put (w,x,table), b = y. Let us denote by PreCondAx the precondition of the ]Jift·taDU· ckar axiom in which the variable y is replaced by b, i.e., the foonula

Thus, using the pu.t·ta6u-cuar axiom, the class of all ~ for which Clear(~.b) holds is determined by

This reads: Any element ~ satisfying the formula Clear(c,b) must have the form J>Ut'(w,x,table), for any w and x satisfying (2). Nevertheless, variables w, x are still unspecified. Next steps will deal with that.

~e.p r= Let us consider PrecondAx, i.e., formula (2). we ave ex_l?lained in section 3, we will try to concretize w and x in (2) exploring where the atomic formulae of PrecondAx may come from. Thus, we have to apply our C'M· formula construction to (some of) the atomic formulae of (2). The formula On(w,x,b) contains a known value, namely b, this is why this formula is first examined. The application of pu.t·ta6[e-on is not J>OSSible, if we sup~se that we cannot 1dentify the table and an object, which 1s here the element b. The only axiom we can apply is therefore the hat axiom. The application of this axiom rt?Quires comparing On( w ,x,b) and Ori(v,hat'(v,q),q). The solution we obtam is

v ~ w, q ~ b, x ~ hat'(w,b).

The precondition of the hat axiom reads then not(Clear(w,b)). (3) changes here to .

C={ ~I~= put'(w,hat'(w,b),table) & Clear(w,hat'(w,b)) & ( 4 ) not(Clear(w,b))}.

Next step will concretize w.

Step 3: As we have mentioned already in footnote 11, this step consists of two subproblems:

Step 3.1: Trivial Transformations

In [Franova and Kodratoff, 91a] we explain in detail that this step succeeds to find the foflowing conditional non­ recursive part of the prOSfclD! we want to synthesize:

if Clear(s 0 ,hat'(So.h)) & not(Clear(s 0 ,b))

makeclear(s 01 b) = J!Ut(.hat(b),table)

Step 3.2: Non - trivial Transformations

We try to apply induction hypotheses to (4). Comparing IH and formulae in (4) we can see that Ili (with z = makeclear(s 111 ,u)) can be compared to the formula Oear( w ,hat'( w ,o J ). This leads to the equations

w = s 0 ;makeclear(sll'u), u = hat(b) However, the aJ>Plication of IH IS justified only if we are able to prove thathat(b)Lb." Let us assume that we have means to confmn this refation. This leads to w +--- s 0 ;makeclear(s 0 ,hat(b )).

11 Scme complementary knowledge is necessary to establish this relation. Presently, when we check that such a relation holds during the application of the induction hypothesis, we asswne a priori that thiJ relation holds, in order to avoia interrupting the theorem proving process. The validity of such an assumption can be verified by the user. We are plannmg to automatize this process. This problem is

Using p{an {inK.Pge, we have put'(w,hat'(w,b),table) = w;put(hat(b),table). Finally, the class Cchanges to

C =( l; ll; = s 0 ;makeclear(s 0 ,hat(b));put(hat(b),table) & (S)

not(Clear(s 0 ;makeclear(s 0 ,hat(b )),b))),

i.e. , we can replace the abstract argument 1; by the more concrete one

s 0 ;makeclear(s 0 ,hat(b));put(hat(b),table).

We denote it, as in the general scheme, by a.

Our goal is now to verify if s 0 ;z belongs to C in we hav~ to check if we can replace a by s 0 ;z 1 · ally, we obtam

z 1 +--- makeclear(s 0 ,hat(b));put(hat(b),table).

Ste~ 5: No simplifications are necessary.

In conclusion, we have the program

makeclear(So,b) =

A, if Clear(s ,b)

put(hat(b ),tagle ), if Clear(s 0 ,hat'(sQ.,b ))&not(Clear(s 0 ,b )) inakeclear(s 0 ,hat(b) );put(hat(b ),table).

5 Conclusion

In all our previous work we presented the eM­ construction of atomic formulae as a method which helps to solve strategic aspects of inductive theorem proving applied to program synthesis. This paper shows that our Constructive Matcliing methodology can be applied and adapted to other well-founded theories, not only to CD, even though the present implementation works only for CD.

Summarizing, we have illustrated in this paper the following characteristic features of our C'M methodology:

D It provides a couple (what has to be achieved; what ~ has to be achieved from) at any step of an inductive proof. This is the main characteristic. Note that this feature reduces the search space of a proof, the last is the main problem of deductive approach to program synthesis.

D For the induction step, ~ uses the general induction scheme and a kind of "forced" application of this scheme (more details are given in section 4).

D If necessary, ~ applies the 0\£-formula construction to formulae obtained as cond~ions for the valid~y of F (see step 2*).

C'M methodology can be compared to the notion of a plan in Bundy's reconstruction [Bundy, 88] of Boyer&Moore methodology. Our methodology could create one of the most general plans in Bundy's reconstruction, because it comprises most of Bundy's "reconstructed" tactics··. A deep analogy between Bundy's approach and our methodology is illustrated by the importance of universally quantified induction hypotheses acknowledged by both approaches [Franova, 85; Bundy et al., 90].

similar to verifying the correctness of the given axioms. Besides, the relation hat(b) < b seems to be a reasonable well-founded relation for induction proofs in blocks world problems. However, analogously to constructible domains, for particular problems, how the well-founded relation looks, depends always on the given axioms (or the given theory). In other words, we cannot know in advance the well-founded relation which is to be used in blocks world problems, since it depends pp the available definitions.

For instance, all examples presented in [Bundy et al., 90] are successfully solved by our methodology. This shows that our way of constructing a formula provides a solution for the problem of making possible the application of induction hypotheses, this problem being the topic of Bundy's "rippling-out" tactics. Since we prove also theorems containing existential quantifien, our approach is clearly more general than Bundy's.

Moreover, a "rational reconstruction" of our methodology would allow the introduction of existential quantifiers into Bundy's improved system, thus recognizing program synthesis as an inductive theorem proving problem, or, in other words, bringing program synthesis back where it belongs classically - inductive theorem proving.

In [Franova, 91c] we describe in detail the strengths and weaknesses of our methodology viewed as a program synthesis methodology.

Acknowledgments

We express our thanks to an anonymous referee for many constructive critics.