PROW: A Step Toward Automatic Program Writing

This paper describes a program, called "PROW", which writes programs . PROW accepts the specifi­ cation of the program in the language of predicate calculus, decides the algorithm for the program and then produces a LISP program which is an im­ plementat ion of the algorithm. Since the construc­ tion of the algorithm is obtained Qy formal theorem- proving techniques, the programs that PROW writes are free from logical errors and do not have to be debugged . The user of PROW can make PROW write programs in languages other than LISP by modifying the part of PROW that translates an algorithm to a LISP program. Thus PROW can be modified to write programs in any language . In the end of this paper, it is shown that PROW can also be used as a quest ion- answering program.

Section 1: Introduction

A programmer can easily make two kinds of mis­ takes. First, the grammar of the programming lan­ guage that he uses is so complex that he easily makes syntactical errors. Second, it is not easy to always think logically, so he is liable to make mistakes in constructing algorithms, thus prod­ ucing logical errors .

Much effort has been made in simplifying the programming languages so that programmers will make fewer syntactical errors. Although one can still complain that the advanced languages avail­ able today are still not simple and natural enough, he should find comfort in noting that they are much eas i er than machine language .

As yet, not much has been done to overcome the second difficulty mentioned above . In this paper, the aut hors will describe a program called "PROW" (Program Writi ng), which is designed for this pur­ pose . PROW resembles the "state description" port ion of the heuri stic compiler (7) by Simon and is much in the spirit of Slagle (8), Raphael and Green (l) in fully using the power of formal logic .

In PROW, the instructions of LISP are axioma­ t i zed and stored as axioms . The user expresses the relationship between the input and output variables as a well- formed formula in the first order predi­ cat e calculus (2). Suppose the input and output

variables of the program are X, x 2 , .·. ,X and 1 m

Y, Y, ... , Y respectively and that the relation 1 2 n between them is R(X , ..· , X , Y , ... , Y ) · PROW 1 m 1 n then constructs the theorem:

Richard J. Waldinger Carnegie-Mellon Upiv., Pittsburgh, Pa. Richard _C, T, Lee National Institutes of Health Bethesda, Md.

PROW first calls a theorem prover to prove the theorem, thus establi shing the existence of the program. The output of the theorem prover is a "proof" of the theorem. PROW then calls another program to process the proof and gives the desired program.

Since PROW uses theorem prover to write pro­ grams, the programs that it writes are f r ee from logical errors . As shown in Section 6, PROW can also be used to aid robots, to des ign circuits as well as to write programs in languages other than

LISP.

The authors have tried hard to make this paper self- contained. However, the r eaders who want t o thoroughly understand "PROW" should be familiar with LISP (3,10) and automatic theorem proving (5,6,8).

It should be noted that the function of PROW is quite different from that of a compiler because the user of a compiler, such as a FORTRAN program­ mer , has to construct the algorithm himself, while the user of PROW has only to supply the specifica­ tions of his program and PROW i s able to decide the algorithm for him.

The proof of the correctness of the algorithm used in PROW i s omitted in this paper because of the limitation of space . It will be included in R. Waldinger 's Ph .D. thes is later .

Section 2: The Resolution Principle and Progr am Writing

The theorem prover of PROW uses Robinson 's re­ solution principle (5 , 6, 8) as its inference rule . It will be shown later t hat the or dinary resolution principle is not appropriate and adequat e for pro­ gram writing . This leads to the notion of "primitive r esolution" which will be discussed in detail in Sec~ion 3.

Example 1: The characteristic function of the predicate "Atom" in LISP.

Suppose we want to write a program whose output

is 1 if the input is an atom and 0 otherwise .

The axiom we need is

The theorem to be proven is

(X)(EY)(

(Atom(X) & Equal(Y,l))

The negation of the theorem with quantifiers removed, (see (5)), consists of the following clauses:

The proof of the theorem is

The proof can be represented b,y a tree, where every node represents a clause in the proof, and under every arc, we write down the following in­ formation:

• (a) The substitution of the variables, if there is any substitution made.
• (b) If clause N is derived from clauses Nl and N2, then on the arc from N to Nl, write down the negation of the literal deleted from clause Nl, with the appropriate substitutions made.

The proof of Example 1 can now be represented b,y the tree in Fig. 2-1.

The tree in Fig. 2-1 can be considered as the flowchart of the program. Nodes 3,1 and 4 are halt or terminal points and node 7 is the st arting point . The predicates represent testing points for tra­ versing the arcs. For instance, the arc from (5) to (3) is labelled with the test "Equal(l,l)". This means that if control is at node (5) and the predicate Equal(l,l) is true, then control passes to node (3). Since the arc is also labelled with the substitution y~l, the variable y is set to 1.

In Fig. 2-1, the arcs leading to (1) are of special interest because ~Equal(l, 1) and -Equal(O,O) can never be true. Therefore , control will never be passed to node (1). In fact, it can be shown that if a node represents an axiom or a clause which is always true, then control will never be passed to that point. We can thus safely delete node (1) from the tree and Fig.2-l is simp­ lified to Fig.2-2.

Since there is no branching out of nodes (5) and (6), no testing is necessary in those two nodes. We can therefore further simplify Fig.2-2 to The LISP program produced by PROW is the following:

(lAMBDA (A)

(PROG (Y)

(COND ( (ATCM A) (GO Al)))

(RETURN Y)

Example 2: The "Member" £unction,

The "Member" function of LISP is a widely used function. The input has two arguments: X and L, where X is any S-expression and L is a list. The output will be T if X E L and NIL if otherwise.

The axioms expressing the definition of "Member" are

The theorem to be proven is

The Negation of the theorem gives

The tree representing the proof of Example 2 l ooks like Fig.2-4.

The program represented by the tree in Fig.2-4 will necessarily involve the testing of X E L, which is not defined or primitive in LISP. There­ fore, the program is meaningless. Proofs such as the one described above which yield non-executable programs must be forbidden. This is achieved as follows: the user of PROW may declare which sym­ bols are primitive. Only primitive symbols will appear in the program.This is made possible by using a special inference rule, called "primitive reso­ lution." The proof that is obtained by "primitive resolution" is called a ":;Jrimitive proof." The program that is obtained by processing a primitive proof contains only primitive symbols. This will be discussed in the next section.

Section 3: The Primitive Proof and the Post-Proof Processor

In this section, we are going to define a new inference rule, called the "primitive resolution." The proof that is obtained by the application of the primitive resolution is called the "primitive proof." For readers who are interested only in the performance of PROW, this section can be skipped.

First of all, the user of PROW has to declare the following:

• (a) Primitive symbols: The symbols which are allowed to appear in the program.
• (b) Insipid clauses: The clauses that the user claims to be always true. (All the axioms are necessarily insipid, but whether a special hypo­ thesis is insipid or not depends on the user.)
• (c) Output variables: Suppose the theorem con­ cerning the program has the following quantifier:

Negation of the theorem will make all the variable X, 's appear in the clauses as constants (4). They ~ are called the input constants. All the Y. 1 s will ~ appear as variables in the clauses and the user has to declare some of the Y.'s as output variables, ~

We also need the following definitions:

Def.: Halt clause: the set of halt clauses is the set of all the clauses that the user pro­ vides as input.

• Def.: Vital clause: the definition of a vital clause is inductive.
• (a) A halt clause that i s not declared in­ sipid is a vital clause.
• (b) In a proof, a clause B t hat is a r esolv­ ent of clauses C and D is vital i ff one or both of C and D i s vit al .

Def.: Hot variables: the hot variables ar e al so de­ fined inductively.

• (a) Insipid clauses have no hot variables.
• (b) The hot variables of a vital halt clause are those output variables (if any), appearing in that clause.
• (c) Let B be a resolvent of clauses C and D. Sey B=(C-L) G'cU(D-M)bd

(1) If W is hot inC, then the variables which occur in both W 6 and B are hot in B. If W is hot in D, then the vari­ ables which occur in W"d and Bare hot in B.

1. If C and D are both vital, then the variables which occur in both L ~ and B are also hot in B.

Example:

Suppose that C and D are both vital and Y is the only hot variable. The resolvent of C and D is

B is vital and its hot variables are Y and X. The variable Y is hot because it occurs in a term of the form W 6:: (W=Y and ~ =the identity substitu­ tion). (Condition (1)). The variable X is hot because it occurs in a term of the form L ~c where L=P(X), 6 c = the identity substitution and because C and Dare both vital. (Condition (2)).

Def.: A proof P is said to be "primitive" if it

obeys the following restrictions:

• (a) Let clause B be a resolvent of clauses C and D, say B=(C-L) ~ U(D-M) 6d

Then if W is hot in C, all the constant and function symbols occurring in W 6c must be primitive. If W is hot in D, then all the constant and function symbols occurring in W Gd must be primitive.

• (b) If C and D are both vital, then all the constant, function and predicate sym­ bols occurring in L 6c must be primitive.

Example: The proof of the first example in Section 2 is primitive since A1Qm, a, Q,and 1 are all primitive. The predicate "Atom" is a standard LISP predicate, the constant a is the input cons­ tant and Q and l are numerals which we can use in LISP computations.

If, for some reason, l were not primitive, the deduction of clause 5 would be illegal in primitive resolution since the variable Y is hot in clause 3 and the resolution involves substituting l for Y by condition (a). On the other hand, if "Atom" were not primitive, then the deduction of clause 7 would be illegal by condition (b).

After the theorem is proved, the proof which is a sequence of clauses is fed into a post-proof processor. Before describing the processor;we first have to define the following:

Def.: Substitution: A substitution is a finite set fT 1 /v 1 , T 2 /v 2 , ··· , T~Vk}

of substitution components Ti/Vi' where Vi is a variable and T. is a term different ~ from Vi' and no two components in the set have the same variable after the stroke symbol.

Def.: Operation P( 6,X)

Let 6 be a substitution and let X be a set. of variables.

1. If 0 is the empty substitut:i_on, then P( ~,X) is empty.
2. If 6 = ~ U '(where 'C is a substitution component, and the variable of Z: does not belong to X, then P( ~,X)=P(~ 1 ,x).

For example,

The post-proof processor would first single out vital clauses of the proof and with each vital clause B, the processor associates a program as follows:

1. Suppose B is a halt clause. Suppose Y 1 , Y 2 , ··· , Yn is the complete list of output

variables, including those not appearing in B ·. The program associated with B is then

2. Suppose B is a resolvent of clauses C and D where C at least is vital, say B = (C-L)~ U (D-M)\Sd · Let H be the set of hot variables of C, and let ~ beC the set of hot variables of D. Let ProgC and ProgD be the programs associated with clauses C and D respectively.

• (a) Suppose C and D are both vital. Let GC be a label which does not appear in the program associated with any other clause in the proof. Then the program ProgB associated with B is defined by

ProgB

ProgD

ProgC}

• Then (a) Suppose C is vital, hut D is not.

constants.

Let Progn be the program associated with the empty clause in the proof. Let\' x2, ··· xj be the

complete list of variables in Progn. Then the final program that the machine produces as output is

Section 4: The Induction Axian and. Wooing in a Program

The negation of the theorem gives the following clause:

where a is the input constant and Y is the output variable. "Factrel" is not considered as primi­ tive, of course.

To prove this theorem, we need a famous in­ duction axian for natural numbers. Let R(X, Y) mean f(X)=Y where f(X) is any function of natural numbers. Then the induction axian can be ex­ pressed as follows:

Formula (7) suggests that, instead of proving

(X)(EY)Factrel(X,Y)

directly, we prove the following two sub-theorems:

and

(X~((EY 1 )Factrel(X,Y 1 )

The negation of (8) gives

The algorithm we gave in the last section will not produce any program with recursive property, i.e., the programs will not be able to call them­ selves. In PROW, the recursiveness of a program is provided by induction schema. By using an in­ duction scheme, we mean that instead of proving the main theorem, it suffices to prove sane sub-theorems. & Every proof of a sub-theorem produces a sub-program. PROW also has the ability to combine all the sub­ programs together to form the main program. We shall illustrate these procedures by an example first and give the exact algorithm at the end of this section.

Example: We want to write the program that canputes the "factorial" ·function which is defined inductively as follows:

Let predicate Factrel(X,Y) denote f(X) = Y. Then the axi oms concerning the definition of "factorial" are :

where Addl(X) and Times (X.Y) are both LISP functions . (Addl (X)=X+l and Times(X,Y)=X·Y). The theorem to prove in this case is

The negation of (9) gives

Let the programs associated with (8) and (9) be Progl and Prog2 respectively, Progl has no input parameter while Prog2 has a and b as input para­ meters.

Besides the induction axian, PROW also stores in its memory the information on how to connect Progl and Prog2 together to form the program computing f(X). For this case, the function f(X) can be expressed in terms of Progl and Prog2 in the following form:

f(X)

where Subl [x] = x-1.

Progl and Prog2 can be found by using the algorithm introduced in Section J , The r eader can easily convince himsel f that:

Prog A

• (lAMBDA ( )

(PROO (Y)

(SETQ Y l)

(RETURN Y) ) )

• (lAMBDA (B C)

(PROO (Y)

(SETQ Y (TIMES (ADDl B) C))

(RETURN Y) ) )

The program that computes "factorial" is thus

Factorial

(lAMBDA (X)

(COND ((EQUAL X 0)

(SETQ Y l)

(RETURN Y)))))

(T ((lAMBDA (B C)

(PROO (Y)

(SETQ Y (TIMES (ADDl B) C))

(RETURN Y)))

In the LISP system, we may also introduce in­ duction axioms. For example , the following axiom is a very useful one:

Again, R(X,Y) means f(X)=Y.

Roughly speaking, this means that if

(l)NIL has property P, and (2) cons(y,x) has property P, whenever X has property P, then every S-expression that is expressible in "list"

ProgB

notation has property P.

Again, the induction axiom will suggest two sub-theorems to prove:

and the negation of (16) gives

The program associated with (17), Progl, has no input arguments while the program associated with (18) & (19), Prog2, has a,b & cas input arguments. The function that computes f(x) in terms of Progl and Prog2 takes the following form:

f(x)

If there are two input variables, then the in­ duction axiom may take the following form:

Formula (20) is a very useful axiom. It can be used to write the "Member" function in LISP. We shall devote the whole next section to show how this is done.

Section 5: The "Member" function of LISP

Due to the limited capability of the theorem prover of PROW, PROW cannot prove the theorems in­ volved in the ''Member" function of LISP. The following example is a hand-simulated one.

The ''Member" function is defined as follows:

Input: X is an S-expression.

L is a list.

Output: Y = T if X E L Y = NIL if otherwise .

Let P(X,L) denote X E L, Memrel(X,L,Y) denote Member (X, L) = Y and Equal(X,Y) denote X = Y.

The axioms concerning the defini tion of

"member"·; the property of P(X,L) as well as the re­ lationshi p bet ween P(X,L) and Equal (X,Y) ar e collected as follows:

P(X,L) V Memrel(X,L,NIL)

(2)

Equal(X,Y) V P(X,L) V~P(X, cons (Y,L))

(5)

~qual(X,Y) V~qual(Y,Z) V Equal(X,Z)

(6)

-Equal(X,Y) V~qual (Z,Y) V Equal(X,Z)

(8)

The main t heor em to prove is

(X)(L)(EY)Memrel (X,L,Y)

The negati on of this theorem is

The Induction Axiom is

From (15), we have to prove the following two t heor ems :

First theor em:

The negat i on of this theorem is

Second theorem:

The above t heorem is equival ent to:

The negation of this theorem gives

The following symbols are declared "primitive . "

(A) Constants: NIL, T, a 1 ,a 2 , b 2 , c 2 .

(B) Functions : f(X), Member(X,L),cons(X,Y)

(C) Predicat es : Equal(X,Y)

The vital cl auses are (17) & (21). In each of them, the output variable Y is a hot variabl e . Let the programs associated with the first theo­ r em and the second theorem be Progl and Prog2 respectively. The function that combines Progl and Prog2 i s

To help the reader s understand the·resolution principle which i s used in PROW to prove theorems, we write (c 1 ,1 1 ,c 2 ,1 2 ) in front of clause C in case that cl ause C is a resolvent of cl auses c 1 and c2 Qy deleting the 11th literal of cl and the 1 2 th literal of c 2 . If cl ause C is a factor of clause cl by matching the 1 th and the 1 th 1 2

literals of c 1 , then we write (c 1 ,L 1 , c 1 ,L 2 ) i n

f ront of clause C.

The proof of the second theorem:

(24,3, 8,1) ~P(X,L) V ~emrel(X,L,U )

• (32,1,32,4) P(X,L) V Equal(X,Y) V ~mrel(X,L,U) V ~mrel(X,cons(Y,L),v) V Equal(V, U) (33)
• (27,1,27,2) ~(X,L) V ~mrel(X,cons(Y,L),U) V ~mrel(X,L,V) V Equal(V,U) (34)

• (35,2,35,6) Equal(X,Y 1 ) V ~mrel(X,L,U 1 ) V ~mrel(X,cons(Y 1 ,L),v 1 ) V Equal(V 1 ,u 1 ) V ~mrel(X,cons(Y 2 ,L),U 2 ) V Equal(U 1 ,u 2 ) (36)
• (36, 3,36, 5) Equal(X,Y) V ~mrel(X,L,U) V ~mrel(X,cons(Y,L),V) V Equal(V,U) V Equal(U,V) (37)

In the above proof, those cl auses t hat have "*" signs attached are vital cl auses . The pro­ grams corresponding t o t hese vital cl auses are the following:

Prog43

Prog44

(SETQ Y (MEMBER B A))

(RETURN Y)

(SETQ Y T)

(RETURN Y)

• Prog45 (COND((EQUAL B C) (GOAl)) ) (SETQ Y (MEMBER B A))

(RETURN Y)

(SETQ Y T)

(RETURN Y)

So, Prog2 corresponding to the second theorem is

Prog2 = (LAMBDA (A B C)

(PROG (Y)

( COND ((EQUAL B 6) (GO Al))

(SETQ Y (MEMBER B A))

(RETURN Y)

(SETQ Y T)

(RETURN Y))

It now remains to find the program correspond­ ing to the first theorem. The proof is much easier as compared with that of the second theorem.

Proof of the first theorem:

• (38,3,12,2) Equal(X,Y) V ~emrel(X,L,U)V Equal(V,U) The programs associated with clauses (46) and V ~qual(Member(X,cons(Y,L)),v) (39) (47) are

• (40, 3,12,1) Equal(X,Y) V ~mrel(X,L,U) V MBmrel(X,cons(Y,L),u) (41)
• (41, 2, 20,1) Equal(X,Y) V Memrel(X, cons(Y, a 2 ),f(X)) (42)

Prog47

(SETQ Y NIL)

(RETURN Y)

Al

Al is The program associated with the first theorem

Let us restate t he function combining these two programs together:

=( LAMBDA (X L)

Section 6 : The Application of PROW t o Peductiye Question-Answering

Since the output of PROW can be consi dered as a sequence of instructions, it can also be used as a question- answering program (1,8). In this section, we shall show four exampl es of how this can be done .

Example 1: The first monkey-banana problem.

The problem can be briefly stated as follows : A banana·is suspended from the ceiling of a room. A monkey is on the floor, but is too short to reach the banana . There is a chair in the room, and the monkey can walk freely in the room, carry­ ing the chair together with him. Furthermore, the monkey can climb the chair .

This problem has been solved by the programs of Slagle (8) and Green (1).

Let P{XM, ZM, XC, S) represent the sentence, "State S is attainable in which the monkey is at position XM on the floor, at height ZM while the chair is at the horizontal pos ition XC on the floor . "

We also define the following functions :

1. Walk(X,S): the state achieved if the monkey is in state S and then walks to position X.
2. Carry(X,S): the state achieved if the monkey is in state S and walks to position X, carrying the chair with him.
3. Climb(X,S): the state achieved if the monkey is in state S and climbs the chair whose horizontal position is X.

The problem can be axiomatized as below:

The theorem is

The negation of the theorem gives

All the constants as well as the function symbols are primitive . The output vari able is Y in (6) which is the final state .

PROW generates a program as below:

(LAMBDA (A B C D E H)

(PROO (23 22 2)

(SETQ 23 D)

(SETQ 22 C)

(SETQ 22 (WALK 22 23 ))

(SETQ 22 (CARRY E 22))

(SETQ 2 (CLIMB H 22 ))

(RETURN (LIST 2)) ))

The r eader can see that the program describes the solution of the problem as the following steps :

1. The monkey walks from where originally he stands to the chair .

1. The monkey walks from the position of the chair to the position of the banana, carry­ ing the chair with him.
2. (J ) The monkey climbs the chair .

In the next example, we shall show a very im­ portant feature of PROW. That is, if used as a question-answering program, it can answer questions whose answers involve "conditional expressions ." For example, it may say, "If the door is locked, use the window." This is a great improvement of the present question-answering programs. Also, in this example , the reader can see the importance of the "primitive resolution."

Example 2: There are two boxes, one and only one of which has a banana in it. The monkey can walk freely and he does not know which box contains the banana. But if the monkey is where the box is, he can look into the box and see whether the box con­ tains the banana or not. What should the monkey do to get the banana?

Let P(X, Y ,s ) mean that "the state S is attain­ able in which the monkey is at X and the banana is at Y."

Let Find(S) mean that "S is the state in which the monkey can find the banana."

Axi oms :

The theorem is

This theorem says that no matter where the banana is, the monkey can find it .

The negation of (J) is

The primitive symbols are A,B,C,D,Find, and Walk.

The vital clause i s (5) and the hot variable is S .

Proof:

Applying the algorithm given in Section 2 again, we obtain the following program:

(LAMBDA (A B C D)

(COND ((NOT (FIND (WALK D C) ))(GO Al))

(SETQ Z (WALK D C ) )

(RETURN Z)

Al (SETQ ZJ C)

(SETQ Z2 B)

(SETQ Z2 (WALK Z2 ZJ))

(SETQ Z Z2)

(RETURN Z) ) )

The program can be interpreted as :

1. Go to box B.

1. If you can find the banana in box B, then go back to the starting point and go to box B.
2. otherwise, go to box A.

The unfortunate thing is that, as one can see, the monkey has to go back to the starting point . This is simply because PROW is designed for a pro­ gram writer. Therefore it ignores the side-effect of a testing.

If we allow P(X,Y,S) to be primitive, we would get the following solution:

(LAMBDA (A B C D)

(PROG (ZJ Z2 Z)

(COND ((NOT (PAD C)) (GOAl)))

(SETQ Z2 (WALK Z2 ZJ ))

(SETQ Z Z2 )

(RETURN Z)

Al (SETQ ZJ C)

• (SETQ Z2 B)
• (SETQ I Z2 (WALK Z2 ZJ))

(10,1, 5,1) NIL

(RETURN Z) ) )

This pr ogram involves a testing of the predicate P(A,B,C) which means that the monkey should decide whether the banana is at box B or not. This is, of course , not desirable.

In the third exampl e, PROW is asked to design computer circuits .

Example 3: We have to construct an "Or" gate out of "And" and "Not" gates .

Let I(X) mean X has value T.

Let And(X,Y) = X & Y

and Not(X) =~X

The axioms for this problem are

like to write a program to reverse the contents of registers A and B.

Let P(U,X,Y,Z,S) mean that "State S in which the accumulator contains U and registers A, B and C contain X, Y, and Z respectively is attainable."

Let loada(s), loadb(s) and loadc(s) be .the states after the accumulator is l oaded with the contents of registers A, Band C in state S, respectively.

Let Storea(s ), Storeb(s) and Storec(s ) be the states after the content of the accumulator is stored into registers A, B and C in state S re­ spectively.

The entire machine can be axiomatized as follows :

The theorem is

The negation of the theorem is

The functions "And" and "Not" are de<:!lared primi­ tive and "Or" is not . Both predicates "Equal" and "I" are not primitive. Otherwise, we might be vulnerable to condit ional expressions appearing in our circuits, as if they were LISP programs.

The theorem to be proved is

The proof is omitted , B,r tracing the hot variable Z, we obtain

which is .the circuit we want.

In the present status, PROW can only write programs in LISP. Actually, the idea of PROW is general enough to write programs in any language. In the next example, we shall show how PROW can handl e problems in machine language.

Example 4: Let us imagine a machine with three registers A, B and C and one accumulator . We would

The program that PROW produces is the following:

(lAMBDA (D)

(FROG (ZJ Z)

(SETQ ZJ D)

(SETQ ZJ (LOADA ZJ))

(RETURN Z) ) )

This program, although written i n LISP, repre­ sents a machine language program. The sequence of instructions is : Load the accumulator with register A. Store it into register C. Load the accumulator with register B. Store it into regis ­ t er A. Load t he accumul ator with register C and store it into register B. The contents of regis ­ ters A and B are now r eversed .

Section 7 : Conclusions

The ultimate goal of developing PROW is to have a system such that the programmers are not required to know particular computer languages thoroughly and do not have to construct the algo­ rithms. If this goal is achieved, programming would be more delightful and less time consuming. As yet, PROW is only a step towards this goal .

At present, PROW only understands the first order predicate calculus . It is therefore some­ times more difficult to specify a program than writing the program directly . PROW would be much more improved if some easier- to- use language, such as English, replaces predicate calculus as its in­ put language .

As one can see, the efficiency of PROW depends heavily upon the efficiency of the theorem prover that PROW uses . It i s absolutely necessary to improve the efficiency of the theorem prover.

Acknowledgements

The authors wish to express their gratitude to Professor H. A. Simon of Carnegie-Mellon University, Dr. J . R. Slagle and Dr . C. L. Chang of the National Institutes of Health for their advice, guidance and constructive suggestions.