Application of Theorem Proving to Problem Solving

Abstract

This paper shows how an extension of the resolution proof procedure can be used to con­ struct problem solutions. The extended proof procedure can solve problems involving state transformations. The paper explores several alternate problem representations and provides a discussion of solutions to sample problems including the "Monkey and Bananas" puzzle and the "Tower of Hanoi" puzzle. The paper exhibits solutions to these problems obtained by QA3, a computer program based on these theorem-proving methods . In addition , the paper shows how QA3 can write simple computer programs and can solve practical problems for a simple robot.

Cordell Green Stanford Research Institute Menlo Park, California

twofold: (1) to explore the question of predi­ cate calculus representation for state­ transformation problems in general, and (2) to elaborate upon robot and program-writing appli­ cations of thi s approach and the mechanisms underlying them.

Key Words: Theorem proving, resolution, problem solving , automatic programming, pro­ gram writing , robots, state trans­ formations, question answering.

Automatic theorem proving by the resolution proof procedure 1 § represents perhaps the most powerful known method for automatically determin­ ing the validity of a statement of first-order logic. In an earlier paper Green and Raphael 2 illustrated how an extended resolution procedure can be used as a question answerer--e.g. , if the statement ffix)P(x) can be shown to fo llow from a set of axioms by the resolution proof procedure, then the extended proof procedure will fi nd or construct an x that satisfies P(x). This earlier paper (1) showed how one can axiomatize s imple question-answering subjects, (2) described a question-answering program called QA2 based on thi s procedure, and (3) presented examples of simple question-answering dialogues with QA2 . In a more recent paper 3 the author (1) presents the a nswer construction method in detail and proves its correctness , (2) describes the latest version of the program, QA3 , and (3) introduces state-transformation methods into the construc­ tive proof formalism. In addition to the question-answering applications illustrated in these earlier papers, QA3 has been used as an SRI robot 4 problem solver and as an automatic program writer. The purpose of this paper is Exactly how one can use logic and theorem proving for problem solving requires careful thought on the part of the user. Judging from my experience , and that of others using QA2 and QA3, one of the first difficulties encountered is the representation of problems, especial l y state­ transformation problems, by statements in formal logic. Interest has been shown in seeing several detailed examples that illustrate alternate meth­ ods of axiomatizi ng such problems--i.e., tech­ niques for "programming" in fir s t-order logic. This paper provides detailed examples of various methods of representation. After presenting methods in Sees. I and II, a solution to the classic "Monkey and Bananas" problem is provided in Sec . III. Next, Sec. IV compares several al­ terna te r epresentations for the "Tower of Hanoi puzzle. Two applications , robot problem solving and automatic programming, are discussed in Sees. V and VI, respectively.

* This research i s a part of Project Defender and was s upported by the Advanced Research Projects Agency of the Department of Defense and was monitored by Rome Air Development Center under Contracts AF 30(602)-4147 and F30602- 69-C-0056.

t This preprint is a preliminary version and is subject to modification prior to publica tion.

§ References are listed at the end of thi s paper.

I. An Introduction to State-Transformation Methods

The concepts of states and state transforma­ tions have of course been in existence for a long time , and the usefulness of these concepts for problem solving is well known. The purpose of this p aper is not to discuss states and state transformations as such, but instead to s how how these concepts can b e used by an a utomatic resol u­ tion theorem prover. In practice , the employment of these methods has gr eatly extended the problem­ sol ving capacity of QA2 and QA3. McCarthy and Hayes 5 present a relevant di scussion of philosophi­ cal probl ems involved in attempting such formali­

zations .

First we wi ll present a simple example . We begin by conside ring how a particula r universe of discourse might be described in logic .

Facts describing the unive r se of discourse are expressed in the form o f s t atement s of mathe­ matical l ogic . Questions or problems ar e stat ed as conjectures to be proved. If a theorem is proved, then the nature of our extended theorem prover is such that the proof is "constructive"-­ i.e ., if the theorem asserts the existence of an object then the proof f inds or constructs such an object.

At any given moment the universe under con­ s ideration may be said to be in a given state .

We wi ll represent a particular state by a subscripted s--e.g., s 17 · The letters, with no subscript , will be a variable, ranging over states. A state is described by means of predi­ cates. For example , if the predicate AT(object 1 ,b, s 1 ) is true, then in state s 1 the object, object 1 , is at position b. Let this predicate be axiom Al:

The question "where is object1 in state s 1 ?" can be expressed in logic as the theorem {3x)AT(object 1 ,x,s 1 ). The answer found by using s ystem QA3 to prove this theorem is "yes, x =b ."

Changes in states are brought about by per­ forming actions and sequences of actions . An action can be represented by an action function that maps states into new states (achieved by executing the action) · An axiom describing the effect of an action is typically of the form

(if s)[P(s) :::l Q(f(s))]

where s is a state variable

• P is a predicate describing a state
• f is an action function (corresponding to some action) that maps a state into a new state (achieved by executing the action)
• Q is a predicate describing the new state.

(Entities such as P and f are termed "situational fl uents" by McCarthy.)

As an example , consider an axiom describing the fact that object 1 can be pushed from point b to point c. The axiom is

A2. Cifs)[AT(object 1 ,b, s) :::l

AT(object 1 ,c,push(object 1 ,b,c,s))].

The function push(object 1 ,b, c,s) corresponds to the action of pushing object 1 from b to c . (Assume, for example, that a robot is the

executor of these actions .)

Now consider the question, "Does there exist a sequence of actions such that objectt is at point c?" Equivalently, one may ask, 'Does there exist a state , possibly resulting from applying action functions to an initial state s 1 , such that object 1 is at point c?" This question, in logic, is Gs)AT(object 1 ,c,s), and the answer, provided by the theorem-proving program applied to axioms Al and A2, is "yes,

s = push(objact 1 ,b,c,s 1 )."

Suppose a third axioi indicates that object1 can be pushed from c to d:

A3. {'fs)[AT(object 1 ,c,s) :::l Together, these three axioms imply that starting in state s 1 , object 1 can be pushed from b to c and then from c to d. This sequence of actions (a program for our robot) can be expressed by the composition of the two push functions, push(object 1 ,c,d,push(object 1 ,b,c,s 1 )). The normal order of function evaluation, from the innermost function to the outermost, gives the correct sequence in which to perform the actions .

To find this solution to the problem of get­ ting object 1 to position d, the following con­ jecture is posed to the theorem prover: "Does there exist a state such that object 1 is at position d?" or, stated in logic, ~s)AT(object 1 ,d, s) . The answer returned is

"yes, s = push (obj ect 1 , c,d, push (obj ect 1 , b, c, s 1 )) · "

The proof by resolution, given below, demon­ strates how the desired answer is formed as a composition of action functions , thus describing a sequence of necessary actions. The mechanism for finding this answer is a special literal,* the "answer literal." This method of finding an answer is explained in detail in Ref. 3 . For our purposes here, we will just show how it works by example . In the proof below, each answer literal is displayed beneath the clause containing it. At each step in the proof the answer literal will contain the current value of the object being constructed by the theorem prover. In this exam­ ple the object being constructed is the sequence of actions s. So initially the answer literal ANSWER(s) is added to the clause representing the negation of the question. (One can interpret this clause, Clause 1, as "either object 1 is not at din states , or sis an answer.") The state variable s, inside the answer literal, is the "place holder" where the solution sequence is constructed. The construction process in this proof consists of successive instantiations of s . An instantiation of scan occur whenever a literal containing s is instantiated in the creation of a resolvent. Each instantiation* of s fills in a new action or an argument of an action function. In general, a particular infer­ ence step in the proof (either by factoring* or resolving*) need not necessari ly further instan­ tiate s. For example, the step might be an inference that verifies that some particular property holds for the current answer at that step in the proof. The final step in the proof yie lds Clause 7, "an answer is push(object ,c,d,push(object ,b,c,s )),"which 1 1

terminates lhe proof.

* We assume the reader is familiar with the vocabulary of the field of theorem proving by resolution as described in Refs. 1, 7, and 8.

Proof

ANSWER(s)

• 3.

Resolve 1,2

1. ~AT(object 1 ,b,s)

1. AT(object 1 ,b,s 1 )
2. Contradiction

Resolve 3,4

Axiom Al

Resolve 5,6

For the particular proof exhibited here, the order of generating the solution sequence during the search for the proof happens to be the same order in which the printout of the proof indicates s is instantiated. This order consists of working backward from the goal by filling in the last action, then ·che next-to-last action, etc. In general, the order in which the solution sequence is generated depends upon the proof strategy, s i.nce the proof strategy determines the order in which clauses are resolved or factored. The proof that this method always produces correct answers, given in Ref. 4, shows that the answers are correct regardless of the proof strategy used.

II . Refinements of the Method

The purpose of this ·section is to discuss variations of the formulation presented in the previous section and to show how other considera­ tions such as time and conditional operations can be brought into the formalism. The reader who is interested in applications rather than additional material on representation may omit Sees. II, III, and IV, and read Sees. V and VI.

A. An Alternate Formulation

The first subject we shall discuss is an alternate to the previously given formulation. We shall refer to the original, presented in Sec . I, as formulation I, and this alternate as formulation II. Formulation II corresponds to a system-theoretic notion of state transformations. The state transformation function for a system gives the mapping of an action and a state into a new state. Let f represent the state transfor­ mation function, whose arguments are an action

Negation of theorem and a state and whose value is the new state obtained by applying the action to the state. Let [ai} be the actions, and nil be the null action. Let g be a function that maps two actions into a single composite action whose effect is the same as that of the argument actions applied sequentially . For example, axioms of the follow­ ing form would partially define the state transformation function f:

The predicates P and Q represent descriptors of states. Axiom Bl describes the result of an action a 1 applied to the class of states that are equivalent in that they all have the property P(s) . The resulting states are thus equivalent in that they have property Q(s) . Axiom B2 indi­ cates that the null action has no effect. The equation in B3 says that the effect of the com­ posite action sequence g(ai,a.) is the same as that of actions ai and aj applied sequentially. The question posed in this formulation can include an initial state--e.g., a que~tion might be ~x)Q(f(x,~ )) , meaning "Does there exist a sequence of actions x that maps state % into a state satisfying the predicate Q?" Observe that we are not insisting on finding a particular sequence of actions, but any sequence that leads us to a satisfactory state within the target

class of states.

This representation is more complex, but has the advantage over the previous representation that both the starting state of a transformation and the sequence of actions are explicitly given as the arguments of the state-transformation function. Thus , one can quantify over, or specify in particular, either the starting state or the sequence, or both .

Next we shall show how other considerations can be brought into a state- transformation formal­ ism . Both the original formulation (I) and the

alternate (II) will be used as needed.

B. No Change of State

This kind of statement represent s an implica­ tion that holds for a fixed state . An axiom typical of this class might describe the relation­ ship between movable objects; e.g., if x is to the left of y and y is to the left of z, then x is to

the left of z .

C. Time

Time can be a function of a state, to express the timing of actions and states . For example, if the function time(s) gives the time of an instantaneous state, in the axiom

EQUAL(difference(time(f(s)),time(s)),T)]],

where P(s) describes the initial state and Q(s) describes the final state, the state transforma­ tion t akes T seconds to complete.

D. State-Independent Truths

An example is

illustrating how functions and predicates are explicitly made stat e independent by not taking states as argument s .

E. Descriptors of Transformations

A descriptor or modifier of an action may be added in the form of a predicate that takes as an argument the state transformation that is to be described. For example,

WISHED-FOR(f(action,state),person)

might indicate a wished-for occurrence of an action;

LOCATION(f(action,state) ,place)

indicates that an action occurred at a certain place.

F. Disjunctive Answers

Consider a case in which an action results in one of two possibilities. As an example, con­ sider an automaton that is to move from a to d.

TA- 7494-6

The above figure shows that action i leads to either b or c from a. The function f is single­ valued but we don't know its value . The goal d can be reached from b by action j, or from c by action k. In the formalization given below it is possible to prove that the goal is reachable although a correct sequence of actions necessary to reach the goal is not generated. Instead, the answer produced is a disjunction of two sequences-­ j ( i ( ~ ) ) or k ( i ( ~ ) ) , We use formulation I. Axiom Ml specifies the starting state ~ and starting position a. Axioms M2 , M3, and M4 specify positions resulting from the allowed moves.

To find if the goal d is r eachable, we ask the following question:

Question: ~ s) AT (d, s)

to which an answer is:

Answer: Yes, s = j(i(s 0 )) or s

The proof is:

Proof

1.	~AT (d, s) ANSWER(s)	Negation of theorem
2.	~AT(b,s) V AT(d,j( s) )	Axiom M3
3.	~AT(b,s)	From 1,2
	ANSWER(j (s))
4.	~AT(c,s) V AT(d,k(s))	Axiom M4
5.	~AT(c,s)	From 1,4
	~(k(s))
6.	~AT(a,s) V AT(b,i(s)) V AT(c,i(s))	Axiom M2
7.	~AT(a,s) V AT(b,i(s))	From 5,6
	ANSWER(k(i(s))
8.	~AT(a , s)	From 3,7
	ANSWER(j(i(s))) V ~(k(i(s))
		Axiom Ml
10.	Contradiction	From 8,9

Observe that clause 8 has two answers, one coming from clause 3 corresponding to the action k and one from clause 7 corresponding to the action j. This shows how an "or" answer can arise.

G. Answers with Conditionals

A conditional operation such as "if p then q else r" allows a program to branch to either opera­ tion q or r depending upon the outcome of the test condition p. By allowing a conditional operation, a better solution to the above problem is made pos s ibl e , namely, "beginning in state s 0 take action i; if at b take action j, otherwise take

action k."

Consider the problem above that yields dis­ junctive answers. The information in the above problem formulation, ax ioms Ml through M4, plus additional information allows the creation of a program with a conditional and a test operation. The fo llowing additional information is needed, which we shall furnish in the form of

axioms .

The f irst addition needed is a conditional operation, along with a description of what the operat ion does. Since our programs are in the form of functions, a conditional function is needed. One s uch possible function is the LISP conditional function "cond" which will be dis­ cussed in Sec. VI. However, another function, a simple "select" f unction is slightly easier to describe and will be used here. The function sel ect(x,y,z,w) is defined to have the value z if x equals y and w otherwise.

The second addition needed is a test operation, along with a description of what it does. Since our programs are in the form of functions, a test funct ion is needed . We shall use "atf", meaning at-function." The function "atf" applied to a state yields the location in that s tate, e.g., atf ( ~) = a . The atf function is described by

These axioms lead to the solution

meaning "if at b after applying i to s 0 , take action j other wi se action k."

Although the new axioms allow the conditional solut ion, just the addition of these axioms does not guarantee that di s junctive answers will not occur . To prevent the possibility of di s junctive answers, we simply tell the theorem prover not to accept any clauses having two answers that don't unify.

What may be a preferable problem formulation and solution can result from the use of the alterna­ tive state formulation, II, exemplified in axioms Dl , B2 1 and B3 above . Recall that f(i,s) is the state transformation function that maps action i and state s into a new state, the function g(i,j)

maps the act ion i and the action j into the sequence of the two actions--i then j. The inter­ relation of f and g is described by

Axioms Ml through M4 r emain the same but axioms M5, M6, and M7 are replaced. The new select function is described by the two axioms :

where the function test applies the test condition p (which will correspond to atf for this problem) to states. The test condition atf is defined by

The new solution is

Further discussion of program writing, including recursion, is given in Sec. VI.

Another method of forming conditional answers is possible. This involves inspecting an existence proof such as the one given in Sec. II-F above. First, such a proof is generated in which clauses having multiple answers are a llowed . The con­ ditional operation is constructed by observing the two literals which are r esolved upon to generate the two-answer clause. For example, in the above proof clauses 3 and 7 r esolve to yi e ld 8. This step is repeated be low, using the varia­ ble s' in 3 to emphasize that s' is different from

s in 7.

Clause 3 may be r ead as "if at b in state s ', the answer is to take action j when in states'." Clause 7 may be read as "if not at £in state i(s) and if at a in stat e s , the answer is to take act ion k when in state i(s) ." Observing that the resolution binds s' to i(s ) in Clause 8, one knows f rom Clauses 3 and 7 the test condition by which one decides which answer to choose in Clause 8 , "if at a in stat e s the answer depends on i ( s) ; if at b-in i(s) take action j; otherwise take act ion -k."

This discussion illustrates that the creation

of a clause with t wo answer liter als indicates that a conditional operation is needed to create a singl e conditional answer. This information pro­ vides a useful heuristic for the program-writing appl ications of QA3: When a clause having two answer literals is about to be generated, l et the proof strategy call for the axioms that describe the condit ional oper ation (s uch as MS and M6). These axioms ar e then applied to create a s ingle conditional answer.

Waldinger and Lee 6 have implemented a program­ writ ing program PROW that also uses a resolution theor em prover to create constructive proofs, but by a different method than that of QA3 . (The second method for creating conditionals by combin­ ing t wo answer s is closely relat ed to a technique used in PROW. ) Information about (l) the target pr ogr am oper at ions , (2) the general relationship of the problem statement and axioms to the a llowed target program operations including the test con­ dit i ons , and (3) the syntax of the target language , is embedded in the PROW program. In QA3 this information is all in the axioms--such as axioms M5 , M6 , and M7.

H. Acqui sition of Information

Another situat ion that arises in problem solving i s one in which at the time the problem is stated and a solution i s to be produced, there is insufficient informat ion to completely specify a solution. More precisely, the solution cannot name ever y act ion and test condition in advance. As an example , consider a robot that i s to move from a to c. The act i on i l eads f rom a to b but no path to c is known, as illustrated below.

However , once point b i s reached, more information can be acquired--for example, a guide to the area lives at b and will provide a path to point c if asked . Or perhaps once point b is reached, the robot might use it s sensors to observe or discover paths t o c.

To formalize this, assume that the action ask-path(b,c) will result in a proper path to c, when taken at b. For simplicity, ass ume that the name of the path i s equal to the state resulting f rom asking the question. Us ing formulation II, one s uit able set of axioms is:

Nl. AT(a,~) 1\ PATH(a,b,i)

where PATH( a ,b,i) means that i i s a path from a to b. The question (,[s)AT(c,s) r esul ts in the solution,

Axiom N3 illustrates an important aspect of thi s formalism for problem solving: I f a condition (such as the robot's) is made state dependent, then we must specify how this condition changes when the state i s changed. Thus in axiom N3 we must indicate that the robot's location is not changed by asking for a path. In a pure theorem­ proving forma lism, this means that if we want to know any condition in a given state, we must prove what that condition i s . If a large number of state-dependent conditions need to be known at e ach state in a solution, then the theorem prover must prove what each condition is at each state in a conjectured solution. In such a c ase the theorem prover will take a long time to find the solution. McCarthy 5 r efer s to this problem as the frame problem, where the word "frame" r efers to the f rame of reference or the set of relevant con­ ditions. Di scussion of a method for easing this problem is presented in Sec . V.

I. Ass ignment Operations

An assignment operation is one that assigns a value to a variabl e . An exampl e of an ass ign­ ment is the s tatement a - h(a), meaning that the value of a is to be changed to the value of the function h(a) · In our representation, we shall use an assignment function- -i. e., assign(a , h(a)) . Using Formulation II this function is described by the axiom

where the predicate. VALUE (a, a 0 , s) means that varia­ ble a has value a 1n states. 0

III. An Example: The Monkey and The Bananas

To illustrate the methods des cribed earlier, we present an axiomatization of McCarthy's "Monkey and Bananas" problem.

The monkey is faced with the problem of get­ ting a bunch of bananas hanging from the ceiling just beyond his reach. To solve the problem, the monkey must push a box to an empty place under the bananas, climb on top of the box, and then reach them, The constants are monkey, box, bananas , and under-bananas. The functions are reach, climb, and move , meaning the following:

reach(m,z, s ) The s t ate resulting from the action of m reaching z, start­ ing from state s

c limb(m,b,s) The s tate resulting from the action of m climbing b, start­ ing f rom s tate s

move(m,b,u,s) The s tate resulting from the action of m moving b to place u, starting from states.

The predicates are:

MOVABLE(b)

.b is movable

AT(m,u,s)

m i s at place u in s tate s

ON(m, b,s)

m is on b in s tate s

HAS(m,z,s)

m has z in state s

CLIMBABLE(m,b,s) m can climb b in state s

REACHABLE(m,b,s) m can reach bin states .

The . * ax1oms are :

MBl . MOVABLE(box)

MB2 . AT(box , placeb , s 0 )

MB3 . (rfx) ~ AT(x ,unde r-bananas ,s 0 )

MB4 . (Vb ,p 1 ,p 2 ,s) [[AT(b,p 1 ,s) A MOVABLE(b) A

(Vx) ~AT (x , p 2 , s) ] ~

[AT(b,p 2 ,move(monkey,b,p 2 ,s)) A

AT (monkey ,p 2 ,move (monkey, b, p 2 , s )) ]]

MB5 . (V s) CLIMBABLE (monkey, box, s)

MB6 . (Vm,p,b,s)[ [ AT(b,p,s) A CLIMBABLE(m,b,s) ] ~

[AT(b ,p,climb(m, b , s)) A

ON(m,b,climb(m,b,s))]]

MB7 . (Vs)[[AT(box,under-bananas,s) A

ON(monkey,box,s)] ~

REACHABLE(monkey,bananas,s)]

* The astute reader wi ll notice that the ax ioms leave much to be desired. In keeping with the "toy problem" tradition we present an unreali s ­ tic axiomatization of this unrealistic probl em . The probl em 's value lies in the fact that it is a reasonably interesting problem t h a t may be familiar to the reader.

MB8 . (Vm,z, s) [REACHABLE (m, z 1 s) ~

HAS(m,z,reach(m,z,s)) ] .

The ques tion is "noes there exist a state s (sequence of act ions) in which the monkey has the bananas?"

QUESTION: a! s) HAS (monkey, bananas , s) ·

The answer i s yes ,

s = reach(monkey ,bananas ,climb(monkey ,

box ,move (monkey , box, under-bananas , ~))) .

By executing this f unction, the monkey gets the bananas . The monkey must, of course, execut e the functions in the usual order, s t arting with the inne rmost and working outward. Thus he first moves the box under the bananas, then climbs on the box , and then r eaches the bananas.

The printout of the proof i s given in the appendix .

IV. Formalizations for the Tower of Hanoi Puzzle

The first applications of our question­ answering programs were to "question-answering" examples . Commonly used question-answe ring exam­ ples have short proofs, and us ually the r e are a few obvious formul ations for a given s ubject a rea. (The major difficulty i n question-answering problems usually is searching a large data base, r ather than finding a l ong and difficult proof.) Typically any reasonable for mulation works well . As one goes on to problems like the Tower of Hanoi puzzle, mor e effort is required to find a repre­ sentation that is suitable for efficient problem sol v ing .

Thi s puzzle has proved to be an interesting study of r epr esentation. Sever a l peopl e using QA3 have set up axi om systems for the puzzle. Appar ently , a "good" axiomat i zat i on--one leading to quick solutions--i s not entirely obvious, s ince many ax i omat i zations did not result in solutions . In this section we wil l present and compare several alternate representations, includ­ ing ones that lead to a solution.

There a r e three pegs--peg 1 , peg 2 , and peg 3 . There are a number of discs each of whose diameter is different f rom that of all the other discs. Initially a ll discs a r e stacked on peg 1 , in order of descending size. The three-disc version is illustrated below.

The object of the puzzle is to find a sequence of moves that will transfer all the discs from peg1 to peg 3 · The allowed moves consist of taking the top disc from any peg and placing it on another peg, but a disc can never be placed on top of a smaller disc .

In order to correctly specify the problem, any formalization must: (1) specify the positions of the discs for each state; (2) specify how ac­ tions change the position of the discs; and (3) specify the rules of the game, i.e., what is l egal.

Let the predicate ON specify disc positions . In the simplest representation the predicate ON specifies the position of one disc--e.g., ON(disc1 , peg ,s) says that in states disc 1 is on peg 1 · This representation requires one predi­ cate to specify the position of each disc. The relative position of each disc either must be specified by another statement, or else if two discs are on the same peg it must be implicitly understood that they are in the proper order. Perhaps the simpl est extension is to allow the predicate another argument that specifies the position of the disc--i. e .,

ON(disc 1 ,peg 1 ,positio~ ,s). Again, this requires many statements to specify a complete configura­ tion.

Since various moves are constructing stacks of discs , and since stacks can be represented as lists, consider as an alternat ive representa­ tion a list to represent a stack of discs. Let the function £(x,y) represent the list that has x as its first element (representing the top disc in the stack) and y as the rest of the list (representing the rest of the discs in the stack) · This function £ corresponds to the "cons" function in LISP. Let nil be the empty list. The state­ ment ON(£(disc 1 ,£(dis~ ,nil)),peg 1 ,s) asserts that the stack having top disc , disc 1 , and second disc, dis~, is on peg 1 · This representation illustrates a useful technique in logic--namely, the use of functions as the construction (and selection) operators . This notion is consistent with the use of action functions as constructors of sequences .

Next , consider how to express possible changes in states. Perhaps the simpl est idea is to say that a given state implies that certain moves are legal. One must then have other state­ ments indicating the result of each move. This method is a bit lengthy. It is easier to express in one statement the fact that given some state , a new state is the result of a move. Thus one such move to a new state is described by (Vs)[ON (£(disc ,nil) , peg 1 ,s) 1\ ON(nil,pe~ , s) 1\ ON(£(disc 2 , £(disc ~nil)),peg3 ,s) ~ ON(nil,peg 1 ,move(disc1 , peg 1 , p~g2 , s)) 1\ ON(£ (disc 1 ,nil) , peg 2 ,move(disc 1 , peg 1 , pe~ , s)) 1\ ON(£ (dis~ , £ (disc 3 ,nil)) , peg 3 , move(disc 1 ,peg 1 ,pe~ ,s))].

With this method it is possible to enumerate all possible moves and configuration combinations. However, it is stil l easier to use variables to represent whole classes of states and moves. Thus

(Vs ,x,y,z,pi'pj ,pk,d) [ON(£(d,x) ,pi's) 1\ ON(y,pj, s ) 1\ ON(z,pk,s) ~ ON(x,pi,move(d,pi,pj,s)) 1\ ON(£ (d,y),p.,move(d,p.,p.,s)) 1\ ON(z,pk,move(d,pi,pJ., J 1 J s))] specifies a whole class of moves. ·The problem here is that additional restrictions mus t be added so that illegal states cannot be part of a solution. In the previous formalism, one could let the axioms enumerate just the legal moves and states, thus preventing incorrect solutions.

The first method for adding restrictions is to have a predicate that restricts moves to just the legitimate states . Since the starting state is legal, one might think that only l egal states can be reached. However, the resolution process (set-of-support strategy 7 ) typically works back­ ward from the goal state toward states that can reach the goal state--such states are sometimes called "forcing states . " Thus illegal but forcing states can be reached by working backward from the goal state . This does not allow for incorrect solutions , since the only forcing states that can appear in the solution must be those reached from the starting state (which is a legal state) . The restriction of moving only to new legal states thus prevents an error. Bu~the search is un­ necessarily large, since the theorem prover is considering illegal states that cannot lead to a solution. So a better solution is to eliminate these illegal forcing states by allowing moves only from legal states to legal states. This is perhaps the best specification, in a sense. Such an axiom is (Vs,x ,y, z ,pi'pj,pk,d)[ON(£(d,x) ·Pi· s) 1\ ON(y,p.,s) 1\ ON(z,pk,s) 1\ LEGAL(£(d,x)) 1\ J LEGAL(£(d,y)) 1\ DISTINCT(pi,pj,pk) ~ ON(x,pi, move(d,pi,pj,s)) 1\ ON(£(d,y),pj,move(d,pi,pj,s)) 1\ ON(z,pk,move(d,~.,p.,s))]. _The predicate LEGAL(x) is true 1f a~d only 1f the d1scs are listed in order of increasing size. (One can "cheat" and have a simpler axiom by omitting the predicate that requires that the state resulting from a move have a legal stack of discs . Since the set-of-support strategy forces the theorem prover to work backward starting from a legal final state, it will only consider legal states. However, one is then using an axiomatization that, by itself, is incorrect.) The additional LEGAL predicate is a typical example of how additional information in the axioms results in a quicker solution. The predicate DISTINCT(pi,pj,pk) means no two pegs are equal .

The clauses generated during the search trat are concerned with illegal states are subsumed by ~LE�AL predicates such as (Vs)~LE�AL(£(disc 2 , (disc 1 ,x))). The stacks are formed by placing one new disc on top of a legal stack . If the new top disc is smaller than the old top disc then it is of course smal ler than all the others on the stack . Thus the legal stack axioms need only to specify that the top disc is smaller than the second disc for a stack to be legal. This blocks the construction of incorrect stacks .

One complete axiomatization is as follows:

AXl. (Vx,y,z,m,n,p 1 ,pj ,pk) [ON(t(d(m) ,x) ,pi ,s) 1\

ON{y,pj,s) 1\ ON(z,pk,s) 1\

DISTINCT{pi,pj,pk) 1\ LEGAL(t(d(m),x)) 1\

LEGAL(t(d(n),y)) ~

ON{x,pi,move(d(m),pi,pj,s)) 1\

ON(t(d(m) ,y) ,p. ,move(d(m) ,pi ,p. ,s)) 1\

J

J

ON(z,pk,move(d{m) ,pi,pj,s))]

• AX2. (Vm,n,x)[LEGAL(t(d(m) ,t(d(n) ,x))) - LESS(m,n)] 1\ (Vn)LEGAL(t(d(n) ,nil)) 1\ LEGAL{nil)

Instead of naming each disc, the disc number n is an argument of the function d(n) that repre­ sents the nth disc. This representation illus­ trates how the proof procedure can be shortened by solving frequent decidable subproblems with special avai lable tools--namely, the LISP pro­ gramming language. The theorem prover uses LISP (the "lessp" function) to evaluate the LESS(n,m) predicate--a very quick step. This mechanism has the effect of generating, wherever needed, such axioms as ~LESS(3 ,2) or LESS(2,3) to resolve against or subsume literals in generated clauses. Similarly , LISP evaluates the DISTINCT predicate.

Note that the move axiom, AXl, breaks up into three clauses, each clause specifying the change in the task for one particular peg. The process of making one move requires nine binary resolutions, and two binary factorings of clauses.

Still other solutions are possible by using special term-matching capabilities in QA3 that extend the unification and subsumption algorithms to include list terms, set terms, and certain types of symmetries .

In another axiomatization, the complete con­ figuration of the puzzle in a given state is specified by the predicate ON, ON(x,y,z,s) means that in states , stack x in on peg 1 , stack y is on pe~, and stack z is on peg 3 · Thus if the predicate ON{£(d 1 ,£<ctz,nil))) ,nil,£(d 3 ,nil),sk) holds, the stack d 1 - ~ is on peg 1 and d 3 is on peg 3 · The predicate LEGAL again indicates that

a given stack of discs is allowed.

1wo kinds of axioms are required--move axioms and legal stack axioms, One legal stack axiom is LEGAL(£(d 1 ,£<ctz,nil))), One move axiom is ~d,x,y,z,s)[ON(£(d,x),y,z,s) 1\ LEGAL(£(d,x)) 1\ LEGAL(£(d,y)) ~ ON(x,t(d,y),z,move(d,p 1 ,P,a,S))], This axiom states that disc d can be moved from peg1 to pe~ if the initial stack on peg 1 is legal and the resultant stack on pegz is legal.

In this last-mentioned formalization, using 13 axioms to specify the problem, QA3 easily solved this problem for the three-disc puzzle. During the search for a proof, 98 clauses were generated

buy only 25 of the clauses were accepted . Of the

25, 12 were not in the proof. The solution entails seven moves, thus passing through eight states (counting the initial and final states). The 12 clauses not in the proof correspond to searching through 5 states that are not used in the solution. Thus the solution is found r ather easily, Of course, if a sufficiently poor axiomatization is chosen--one requiring an enumera­ tion of enough correct and incorrect disc positions-­ the system becomes saturated and fails to obtain a solution within time and space constraints. An important factor in the proof search is the elimination of extra clauses corresponding to alternate paths that reach a given state. In the above problem it happens that the subsumption heuristic 8 eliminates 73 of these redundant clauses. However, this particular use of sub­ sumption is problem dependent, thus one must examine any given problem formulation to deter­ mine whether or not subsumption wil l eliminate alternate paths to equivalent states.

The four-disc version of the puzzle can be much more difficult than the three-disc puzzle in terms of search. At about this level of difficulty one must be somewhat more careful to

obtain a low-cost solution.

Ernst 9 formalizes the notion of ,.,difference" used by GPS and shows what properties these differ­ ences must possess for GPS to succeed on a problem. He then presents a "good" set of differences for the Tower of Hanoi problem. Utilizing this infor­ mation, GPS solves the problem for four discs, considering no incorrect states in its search. Thus Ernst has chosen a set of differences that guide GPS directly to the solution.

Another method of solution is possible. First, solve the three-disc puzzle. Save the solution to the three-disc puzzle (using the answer statement 4 ). Then ask for a solution to the four-disc puzzle. The solution then is: Move the top three discs from peg 1 to pe~ ; move disc 4 from peg 1 to peg 3 ; move the three discs on pe~ tope~. This method produces a much easier solution. But this can be considered as cheating, since the machine is "guided" to a solution by being told which subproblem to first solve and store away. The use of the differences by GPS similarly lets the problem solver be "guided"

toward a solution.

There is another possibly more desirable solution. The four-disc puzzle can be posed as the problem, with no three-disc solution. If the solution of the three-disc puzzle occurs during the search for a solution to the four-di sc puzzle, and if it is automatically recognized and saved as a lemma, then the four-disc solution should follow easily.

Finally, if an induction axiom is provided, the axioms imply a solution in the form of a recursive program that solves the puzzle for an arbitrary number of discs. Aiko Hormann 10 dis­ cusses the related solutions of the four-disc

problem by the program GAKU (not an automatic theorem-proving program) · The solutions by lemma finding, induction, and search guided by differences have not been run on QA3.

V. Applications to the Robot Project

A. Introduction to Robot Problem Solving

In this section we discuss how theorem-proving methods are being tested for several applications in the Stanford Research Institute Artificial Intelligence Group's Automaton (robot). We empha­ size that this section describes work that is now in progress, rather than work that is completed. These methods represent explorations in problem solving, rather than final decisions about how the robot is to do problem solving. An overview of the current status of the entire SRI robot project is provided by Nilsson 4 · Coles 11 has de­ veloped an English-to-logic translator that is part of the robot.

We use theorem-proving methods for three purposes, the simplest being the use of QA3 as a central information storage and retrieval system that is accessible to various parts of the system as well as the human users. The data base of QA3 is thus one of the robot's models of its world,

including itself.

A second use is as an experimental tool to test out a particular problem formulation. When a suitable formulation is found , it may then be desirable to write a faster or more efficient specific program that implements this formulation, perhaps involving little or no search. If the special program is not as general as the axiom system is, so that the special program fails in certain cases, the axioms can be retained to be used in the troublesome cases. Both solutions can be made available by storing, as the first axiom to be tried, a special axiom that describes the special solution, The predicate-evaluation mech­ anism can then call LISP to run the special solution. If it fails, the other axioms will then

be used,

The third use is as a real-time problem solver. In the implementation we are now using, statements of logic--clauses--are the basic units of informa­ tion. Statements are derived from several sources : teletype entries, axioms stored in memory, clauses or statements generated by the theorem prover, and statements evaluated by programs--subroutines in LISP, FORTRAN, or machine language. These programs can use robot sensors and sensory data to verify, disprove, or generate statements of logic.

The SRI robot is a cart on wheels, having a TV camera and a range-finder mounted on the cart. There are bumpers on the cart, but no arms or grasp­ ing agents, so the only way the robot can manipulate its environment is by simple pushing actions. Given this rather severe restriction of no grasping, the robot must be clever to effectively solve prob­ lems involving modifying its world. We present below some axioms for robot problem solving.

The first axiom describes the move routines of the robot :

This axiom s ays that if the robot is at p 1 and there is a path to p 2 , the robot will be at p 2 after moving along the path. The predicat e PATH indicates there exists a robot-path, path 12 , from place p 1 to place p 2 · A robot-path i s a path adequate for the robot's movement. The terms p 1 and p 2 describe the position of the robot.

In general, it may be very inefficient to use the theorem prover to find the path 1 2 s uch that PATH(p 1 ,p 2 ,path 12 ) is true. Several exist­ ing FORTRAN subroutines, having sophisticated problem-solving capabilities of their own, may be used to determine a good path through obstacles on level ground. We will show later a case where the theorem prover may be used to find a more obscure kind of path. For the less obscure paths , the axiom Rl is merely a description of the semantics of these FORTRAN programs, so that new and meaningful programs can be generated by QA3 by using the efficient path-generating programs as subprograms. The "predicate-evaluation" mechanism is used to call the FORTRAN path­ finding routines. The effect of this evaluation mechanism is the same as if the family of axioms of the form PATH(p 1 ,p 2 ,path 12 ) for all p1 and P.a such that path 12 exists, were all stored in memory and available to the theorem prover.

The second axiom is a push axiom tha t de­ scribes the effect of pushing an object. The robot has no arm or graspers, just a bumper. Its world consists of large objects such as boxes, wedges, cubes, etc. These objects are roughly

the same size as the robot itself.

The basic predicate that specifies the position of an object is ATO, meaning at-object. The predicate

indicates that object 1 , having structural descrip­ tion "descriptio~", is in position "posi tio~ ", in state "s 1 ". At the time of this writing, a particular set of "standard" structure descrip­ tions has not yet been selected, So far several have been used. The simplest description is a point whose position is at the estimated center of gravity of the object. This description is used for the FORTRAN "push in a straight line" routine. Since all the objects in the robot's world are polyhedrons, reasonably simple complete structural descriptions are possible. For example, one structural description consists of the set of polygons that form the surface of the polyhedron. In turn, the structure of the polygons is given by the set of vertices in its boundary. Connectivity

of structures can be stated explicitly or else implied by common boundaries, The position of an object is given by a mapping of the topologically­ described structure into the robot's coordinate system, Such structural descriptions may be given as axioms or supplied by the scene-analysis pro­ grams used by the robot.

A basic axiom describing the robot's manipula­ tion of an object is

R2.

This axiom says that if object 1, described by description 1, is at position 1, and object 1 i s movable, and object 1 can be theoretically rotated and translated to the new position 2, and there is an object-path from 1 to 2, then object 1 will be at position 2 as a result of pushing it along the path. The predicate

ROTATE-TRANSLATABLE(desc 1 ,pos 1 ,posG) checks the necessary condition that the object can be theo­ retically rotated and translated into the new position. The predicate

OBJECT~PATH(desc 1 ,pos 1 ,pos 2 ,path 12 ) means that pos 2 is the estimated new position resulting from pushing along push-path, path 12 ·

Let us now return to the frame problem. More specifically, in a state resulting from pushing an object, how can we indicate the location of objects which were not pushed? One such axiom is

This axiom says that all objects that are not the same as the pushed object are unmoved, The predi­ cate evaluation mechanism is used to evaluate SAME and speed up the proof. One can use this predi­ cate evaluation mechanism, and perhaps other fast methods for handling classes of deductions (such as special representations of state-dependent information and special programs for updating this information--which is done in the robot), but another problem remains. Observe that axiom R3 assumes that only the objects directly pushed by the robot move. This is not always the case, since an object being pushed might accidentally strike another object and move it. This leads to the question of dealing with the real world and using axioms to approximate the real world.

B. Real-World Problem Solving: Feedback

Our descriptions of the real world, axio­ matic or otherwise, are at best only approxima­ tions. For example, the new position of an object moved by the robot will not necessarily be accurately predicted, even if one goes to great extremes to calculate a predicted new position. The robot does not have a grasp on the object so that some slippage may occur. The floor surface is not uniform and smooth. The weight distribu­ tion of objects is not known. There is only rudi­ mentary kinesthetic sensing feedback--namely, whether or not the bumper is still in contact with the object. Thus it appears that a large feedback loop iterating toward a solution, is necessary: Form a plan for pushing the object (possibly using the push axiom) , push according to the plan, back up, take a look, see where the object is, compare the position to the desired position, start over again. The new position (to some level of accuracy) is provided by the sensors of the robot. This new position is compared to the position predicted by the axiom. If the move is not successful, the predicate (provided by sensors in the new state) that reasonably accu­ rately gives the object's position in the new state must be used as the description of the initial state for the next attempt.

This feedback method can be extended to sequences of actions. Consider the problem: Find sf such that P3 (sf) is true . Suppose the starting state is s 0 , with property P 0 (so). Suppose the axioms are as follows :

The sequence of actions f 3 (f2 (f 1 (s 0 ))) trans­ forms state s 0 with property P 0 Cs 0 ) into state sf having property P 3 (sf) ·

Corresponding to each "theoretical" predicate Pi(s) is a corresponding "real-word" predicate Pf(s). The truth value of P~(s) is determined by sensors and the robot's internal model of the world. It has built-in bounds on how close its measurements must be to the correct values in order to assert that it is true.* The proof implies the following description of the result

after each step of execution of f3Cf2Cf 1 Cs 0 ))):

* At this time, a many-valued logic having degrees of truth is not used, although this is an interesting possibility.

Actions and Successive States	Predicted Theoretical Results	Predicted Real-World Results
so	Po <so)	P~(s 0 )
sl fl (so)	pl (sl)	p~ (sl)
52 f2 (sl)	P 2 (s2)	P~(s 2 )
f3(s2) sf	P 3 (s3)	I P3(sf)

To measure progress after, say , the ith step , one checks that Pi<s 1 ) is true. If not, then some other condition P~(si) holds and a new problem is generated , given Pi(si) as the starting point. If new information is present, s uch as is the case when the robot hits an obstacle that is not in its model, the model is updated before a new solution is attempted. The position of this new object of course invalidates the previous plan--i.e., had the new object's position been known, the previous plan would not have been generated.

The new solution may still be able to use that part of the old solution that is not invali­ dated by any new information, For example, if Pi(si) holds, it may still be possible to reach the jth intermediate state and then continue the planned sequence of actions from the jth state. However, the object-pushing axiom is an example of an axiom that probably wi ll incorrectly pre­ dict results and yet no further information, except for the new position, wi ll be available. For this case, the best approach is probably to iterate toward the target state by repeated use of the push axiom to generate a new plan. Hope­ fully , the process converges.

For a given axiomatization feedback does not necessarily make it any easier to find a proof. However, knowing that the system uses feedback allows us to choose a simpler and less accurate axiom system. Simple axiom systems can then lead to shorter proofs.

One can envision forma lizing this entire problem-solving process, including the notion of feedback, verifying whether or not a given con­ dition is met, updating the model, recursively calling the theorem prover, etc. The author has not attempted such a formalization , although he has written a first-order formalization of the theorem prover's own problem-solving strategy. This raises the very interesting possibility of self-modification of strategy; however, in prac­ tice such problems lie well beyond the current theorem-proving capacity of the program.

C. A Simple Robot Problem

Now let us consider a problem requiring the use of a ramp to roll onto a platform, as illus­ trated below.

TA-7494- 5

The goal is to push the box b 1 from position x 1 to xz · To get onto the platform, the robot must push the ramp r 1 to the platform, and then roll up the ramp onto the platform.

A simple problem formulation can use a special ramp-using axiom such as

with the obvious meaning. Such a solution is quick but leaves much to be desired in terms of generality.

A more general problem statement is one in which the robot has a description of its own capabilities, and a translation of this statement of its abilities into the basic terms that de­ scribe its sensory and human-given model of the world. It then learns from a fundamental l evel to deal with the world. Such a knowledge doesn't make for the quickest solution to a frequently ­ encountered problem, but certainly does lend itself to learning, greater degrees of problem­ solving , and self-reliance in a new problem situation.

Closer to this extreme of greatest generality is the following axiomatization.

CLEAR(space(r,%) , s) A SOLID(r) ~ PATH(x 1 ,x 2 ,r)].

This axiom says that r describes a rectangle hav­ ing ends x 1 and x 2 · The maximum s lope is l ess than a constant ~ , the width of r is greater than the robot's width w 0 , the space above r to the robot's height ~ is clear, and the rectangle r has a solid surface .

Two paths can be joined as fol lows:

From these two axioms (R5 and R6), the push axiom (R2), and a recognition of a solid object that can be used as a ramp, a solution can be obtained in terms of climb, push, join, etc. This more general method of solution would of course be slower than using the special ramp axiom. On the other hand, the more general method will probably be more useful if the robot will be required to construct a ramp, or recognize and push over a potential ramp that is standing on its wide end.

The danger in trying the more general methods is that one may be asking the theorem prover to re­ der ive some significant portion of math or physics, in order to solve some simple problem.

VI . Automatic Programming

A. Introduction

The automatic writing, checking, and debug­ ging of computer programs are problems of great interest both for their independent importance and as useful tools for intelligent machines. This section shows how a theorem prover can be used to solve certain automatic programming problems. The formalization given here will be used to precisely state and solve the problem of automatic generation of programs, including recursive programs, along with concurrent generation of proofs of the correct­ ness of these programs. Thus any programs auto­ matically written by this method have no errors.

We shall take LI SP 12 ' 13 as our example of a programming language. In the LISP language, a function is described by two entities: (1) its value , and (2) its side effect. Side effects can be described in terms of their effect upon the state of the program. Methods for describing state-transformation operations , as well as meth­ ods for the automatic writing of programs in a state-transformation language, were presented in Sees . I and II. For simplicity, in this section we shall discuss "pure" LISP, in which a LISP function corresponds to the standard notion of a

function--i.e ., it has a value but no side effect .

Thus we shall use pure LISP 1.5 without the program feature, which is essentially the lambda calculus. In this restricted system, a LISP pro­ gram is merely a function . For example , the LISP function ~ applied to a list returns the first element of the list. Thus if the variable x has as value the list (abc), then car(x) =a. The LISP function cdr yields the remainder of the list, thus CDR(x) =~c) , and car(cdr(x)) =b. There are several approaches one may take in formaliz­ ing LISP; the one given here is a simple mapping f rom LISP's lambda calculus to the predicate cal­ culus. LISP programs are represented by functions. The syntax of pure LISP 1.5, is normal function composition, and the corresponding syntax for the ~ormalizati?,n is also f unction composition. LISP pred1cates are represented in LISP--and in this formalization--as functions having either the value NIL (false) or else a value not equal to NIL (true) · The semantics are given by axioms relating LISP functions to list structures, e .g ., (\fx,y)car(cons(x,y)) = x, where cons(x,y) is the list whose first element is x and whose remainder is y.

In our formulation of programming problems, we emphasize the distinction between the program (represented as a function in LISP), that solves a problem and a test for the validity of a solu­ tion to a problem (represented as a predicate in logic) · It is often much easier to construct the predicate than it is to construct the function. Indeed, one may say that a problem is not well defined until an effective test for its solution is provided.

For example , suppose we wish to write a pro­ gram that sorts a list. This problem is not fully specified until the meaning of "sort" is explained; and the method of explanation we choose is to provide a predicate R(x,y) that is true if list Y is a sorted version of list x and false otherwise , (The precise method of defining this relation R will be given later.)

In general, our approach to using a theorem prover to solve programming problems in LISP re­ quires that we give the theorem prover two sets of initial axioms:

1. Axioms defining the functions and con­ s tructs of the subset of LISP to be used
2. Axioms defining an input-output relation such as the relation R(x,y), which is to be true if and only if x is any input of the appropriate form for some LISP program and y is the corre­ sponding output to be produced by such a program.

Given this r elation R, and the LISP axioms , by having the theorem prover prove (or disprove) the appropriate question we can formulate the following four kinds of programming problems: checking, simulation, verifying (debugging), and program writing . These problems may be explained using the sort program as an exampl e as follows:

1. Checking: The form of the question is R(a,b) where a and bare two given lists. By proving R(a,b) true or false, b is checked to be either a sorted version of a o; not . The desired answer is accordingly either yes or no.
2. Simulation: The form of the question is (-[x)R(a,x), where~ is a given input list. If the question (-[x)R(a,x) i s answered yes, then a sorted version of x exists and a sorted version is constructed by the theorem prover. Thus the theorem prover acts as a sort program. If the answer is no, then it has proved that a sorted version of x does not exist (an impos s ible answer if a is a proper list) .
3. Verifying: The form of the question is (\fx) R(x,g( x)) , where g(x) i s a program written

by the user. This mode is known as verifying, de­ bugging, proving a program correct, or proving a program incorrect. If the answer to (Vx)R(x,g(x)) is yes, then g(x) sorts every proper input list and the program is correct. If the answer is no, a counterexample list c, that the program will not sort , must be constructed by the theorem prover. This mode requires induction axioms to prove that looping or recursive programs converge,

(4) Program Writing: The form of the question is (Vx)(:>!y)R(x,y). In this synthesis mode the program is to be constructed or else proved impossible to construct. If the answer is yes, then a program, say f(x), must be constructed that will sort all proper input list s. If the answer is no, an unsort­ able list (impossible, in this case) must be pro­ duced. This mode also requires induction axioms. The form of the problem statement shown here is oversimplified for the sake of c larity. The exact form wi 11 be shown later.

In addition to the possibility of "yes" answer and the "no" answer, there is always the possibil­ ity of a "no proof found" answer if the search is halted by some time or space bound. The elimina­ tion of disjunctive answers, which is assumed in this section, was explained in Sec. B.

These methods are summarized in the following table. The reader may view R(x,y) as representing some general desired input-output relationship.

	Programming Problem	Form of Question	Desired Answer
(1)	Checki ng	R(a,b)	yes or no
( 2 )	Simulation	('h )R(a ,x)	yes, X = b or no
(3)	Verifying	(Vx)R(x, g (x))	yes or no, X = C
( 4)	Program Writing	(Vx) (3"y)R(x, y)	yes, y f (x) or no, X = C

We now present an axiomatization of LISP fol­ lowed by two axiomatizations of the sort relation R (one for a special case and one more general).

B. Axiomatization of a Subset of LISP

All LISP functions and predicates wi ll be written in small letters. The functions "equal(x ,y)," "at(x) ," and "null(x)" evaluate to "nil" if fa l se and something not equal to "nil," say "T," if true. The predicates of first-order logic that are used to describe LISP are written in capital l etters . These, of course, have truth values,

The version of LISP described here does not distinguish between an s-expression and a copy of that S-expression. There is some redundancy in the following formulation, in that certain func­ tions and predicates could have been defined in terms of others; however, the redundancy allows us to state the problem more concisely. Also, some axioms could have been eliminated since thev are derivable from others, but are included for clar­ ity. The variables x, y, and z are bound by universal quantifiers, but the quantifiers are omitted for the sake of readability wherever possible. The formulation is given below:

Predicates	Meaning
NULL(x)	x = nil
LIST(x)	x is a list
ATOM(x) X = y	x is an atom x is equal to

Functions

car(x)

cdr(x)

cons (x,y)

cond(x,y,z)

Meaning

The first element of the list x. The rest of the list x.

If y is a list then the value of cons(x,y) is a new list that has x as its first element and y as the rest of the list, e.g., cons(l, (2 3)) = (1 2 3). If y is an atom instead of a list, cons(x,y) has as value a '~otted pair, " e.g., . cons ( 1, 2) = ( 1 · 2) .

The conditional statement, if x = nil then y else z. Note that the synt~f this function is slightly different than the usual LISP syntax.

nil

equal(x,y)

atom(x)

null (x)

The null (empty) list containing no elements.

Equality test, whose value is "nil" if x does not equal y .

Atom test, whose value is "nil" if x is not an atom.

Null test, whose value is "nil" if x is not equal to nil.

Axioms

Ll: x = car(cons(x,y))

L2: y cdr(cons(x,y))

L3: ~ATOM(x) ~ x = cons(car(x) ,cdr(x))

L4: ~ATOM(cons(x,y))

L5: ATOM(nil)

L6: X = nil ~ cond(x,y,z) = z

L7: xof nil ~ cond(x,y,z) y

LS: X = y = equal(x,y) of nil

L9: ATOM(x) - atom(x) of nil

LlO: NULL(x) - null (x) of nil

c. A Simplified Sort Problem

Before examining a more general sort problem, consider the following very simple special case.

Instead of a list-sorting program, consider a pro­ gr am that "sorts" a dotted pair of two distinct numbers; i.e., given an input pair the program returns as an output pair the same two numbers, but the first number of the output pair must be smal l er than the second. To specify such a pro­ gram, we must define the simple version of R, % (x,y) · Let us say that a dotted pair of numbers is "sorted" if the first number is less than the second. Thus % (x,y) is true if and only if y equals x when x is sorted and y is the reverse of x when x i s not sorted. Stated more precisely,

we have

The correspondence of the LISP "lessp" func­ tion to the "less-than" relation is provided in the following axiom:

Using the predicate fu we will give examples of four programming problems and their solutions:

1. Checking :

Q: % (cons(2,l),cons(l,2))

A: yes

1. Simulation:

Q:

(3:x)% (cons (2, 1) ,x)

1. Verifying:

A: yes

Thus the program supplied by the user is correct.

1. Program writing:

Translated into a more readable form, the program is:

Given only the necessary axioms--Ll, L2, L6, L7, Rl, and R2--QA3 found a proof that con­ structed the sort program shown above. The paramodulation 14 · 1 5 rule of inference was used to handle equality.

We now turn to a more difficult problem.

D. The Sort Axioms

The definition of the predicate R is in terms of the predicates ON and SD. The meaning of these predicates is given below:

• R(x,y) A predicate stating that if x is a list of numbers with no number occur­ ring more than once in the list, then y is a list containing the same ele­ ments as x, andy is sorted, i.e., the numbers are arranged in order of increasing size.
• ON(x,y) A predicate stating that x is an element on the list y.
• SD(x) A predicate stating that the list x is sorted.

First we define R(x,y), that y is a sorted version of x, as follows:

Thus a sorted version y of list x contains the same elements as x and is sorted.

Next we define, recursively, the predicate ON(x,y):

This axiom states that x is on y if and only if x is the first element of y or if x is on the rest of y.

Next we define the meaning of a sorted list:

This axiom states that x is sorted if and only if x is empty, or x contains only one e lement, or the first element of x is less than the second element and the rest of x is sorted.

To simplify the problem statement we assume that the arguments of the predicates and f unctions r ange only over the proper type of objects--i.e., either numbers or lists. In effect, we are assum­ ing that the input list will indeed be a properly formed list of numbers. (The probl em statement could be modified to specify correct types by using predicates such as NUMBERP(x)--true only if

x i s , say, a real number).

The problem is made simpler by using a "merge" function. This function, and a predicat e P de­ scribing the merge function are named and described

as follows:

• sort(x)

A LISP sort function (to be con­ structed) giving as its value a sorted version of x.

merge(x,u) A LISP merge function merging x into the sorted list u, such that the list returned contains the elements of u , and also contains x , and this list is sorted.

P(x,u,y)

A predicate stating that y is the result of merging x into the sorted

• list u.

We define P(x ,u, y), that y is u with x merged into it:

Thus P(x,u,y) holds if and only if the fact that u is sorted implies that y contains x in addition to the e l ement s of u, and y is sorted . One such merge function i s merge(x ,u) = cond(null(u),cons(x,u) , cond(lessp(x , car(u)) ,cons(x,u) ,cons(car(u) ,merge(x , cdr (u))))) ·

The axiom r equired to describe the merge func­ tion is:

S5 . (Vx ,u)P(x,u,merge(x,u)).

This completes a description of the predicates ON, SD , R, and P. Together , these specify the input-output relation for a sort function and a merge function . Before posing the problems to the theorem prover, we need to introduce axioms that describe the convergence of recursive functions .

E. Induction Axioms

In order to prove that a recursive function converges to the proper value, the theorem prover requires an induction axiom. An example of an induction principle is that if one keeps taking "cdr" of a finite list, one will reach the end of the list in a finite number of steps. This i s analogous to an induction principle on the non­ negative integers, i.e., l et "p" be a predicate, and "h" a f unction. Then for finite lists ,

is analogous to

for nonnegative integers.

There are other kinds of induction criteria besides the one given above . Unfortunately, for each recursive function tpat is to be shown to converge, the appropriate induction axiom must be carefully formu l ated by the user. The induction axiom a l so serves the purpose of introducing the

~of the function to be written . We wi ll now g ive the problem s tatement for the sort program, introducing appropriate induction information where necessary.

F. The Sort Problem

Examples illustrating the four kipds of prob­ lems are shown below.

1. Checking:

Q: R(cons(2,cons(l,nil)) ,cons(l,cons(2,nil)))

A: yes

1. Simulation:
2. Verifying: Now consider the verifying or de­ bugging problem. Suppose we are given a proposed definition of a sort function and we want to know if it is correct . Suppose the proposed definition is

Q: (~x)R(cons(2 ,cons(l,nil)),x)

A: yes , x = cons(l,cons(2,nil))

S6. (Vx)[sort(x) = cond(null(x) ,nil,merge(car(x),

sort(cdr(x))))] .

Thus sort is defined in terms of car, cdr, cond, null, merge, and sort. Each of these functions except sort is already described by previously given axioms. We also need the appropriate induc­ tion axiom in terms of sort. Of course, the par­ ticular induction axiom needed depends on the definition of the particular sort function given. For this sort function the particular induction axiom needed is

The following conjecture can then be posed to the theorem prover:

Q: (Vx)R(x , sort(x))

A: yes

1. Program writing: The next problem is that of synthesizing or writing a sort function . We assume, of course, that no definition such as S6 is pro­ vided. Certain information needed for this par­ ticular problem might be considered to be a part of this particular problem statement rather than a part of the data base. We shall phrase the question so that in addition to its primary purpose of ask­ ing for a solution, the question provides three more pieces of information: (a) The question assigns a name to the function that is to be constructed. A recursive function is defined in terms of itself, so to construct this definition the name of the function must be known (or else created internally) . (b) The question specifies the number of arguments of the function that is to be considered.

(c) The question (rather than an induction axiom) gives the particular inductive hypothesis to be

used in constructing the function.

In this form, the question and answer are

Q: ('fx) (3:y)[R(nil,y) 1\ [[~ATOM(x) 1\ R(cdr(x),sort(cdr(x)))] ~ R(x,y)]}

A: yes, y = cond(equal(x,nil),nil,merge (car (x), sort (cdr (x)))) ·

Thus the question names the function to be "sort" and specifies that it is a function of one argu­ ment. The question gives the inductive hypothesis-­ that the function sorts cdr(x)--and then asks for a function that sorts x. When the answer y is found, y is labeled to be the function sort(x).

Using this formulation QA3 was unable to write the sort program in a reasonable amount of time, although the author did find a correct proof within the resolution formalism*. The creation of the merge function can also be posed to the theorem prover by the same methods.

G. Discussion of Automatic Programming Problems

The axioms and conjectures given here illus­ trate the fundamental ideas of automatic program­ ming. However, this work as well as earlier work by Simon~ 6 Slagle; 7 Floyd; 8 Manna; 9 and others pro­ vides merely a small part of what needs to be done. Below we present discussion of issues that might profit from fruther investigation.

Loops. One obvious extension of this method is to create programs that have loops rather than recursion. A simple technique exists for carrying out this operation. First, one writes just recurs­ ive functions. Many recursive functions can then be converted into iteration--i.e., faster-running loops that do not use a stack. McCarthy 20 gives criteria that determine how to convert recursion to iteration. An algorithm for determining cases in which recursion can be converted to iteration, and then performing the conversion process is embedded in modern LISP compilers. This algorithm could be applied to recursive functions written by the theorem-proving program.

Separation of Aspects of Problem Solving. Let us divide information into three types: (1) Infor­ mation concerning the problem description and semantics, An example of such information is given in the axiom AT(a,~), or axiom Sl that defines a sorted list. (2) Information concerning the target programming language, such as the axiom [x = nil ~ cond(x,y,~) = z]. (3) Information concerning the interrelation of the problem and the target lan­

guage, such as [LESS(x,y) = lessp(x,y) f nil].

* After this paper was written the problem was re­ formulated using a different set of axioms. In the new formulation QA3 created the sort program

"sort(x) = cond(x,merge(car(x),sort(cdr(x))) ,nil).

These kinds of information are not, of course, mutually exclusive.

In the axiom systems presented, no distinction is made between such classes of information. Con­ sequently, during the search for a proof the theorem prover might attempt to use axioms of type 1 for pur­ poses where it needs information of type 2. Such attempts lead nowhere and generate useless clauses. However, as discussed in Sec. II-G, we can place in the proof strategy our knowledge of when such infor­ mation is to be used, thus leading to more efficient proofs. One such method--calling for the conditional axioms at the right time, as discussed in Sec. II-G-­ has been implemented in QA3.

The PROW program of Waldinger and Lee 6 provides a very promising method of separating the problem of proof construction from the problem of program construction. In their system, the only axioms used are those that describe the subject--i.e., state the problem. Their proof that a solution exists does not directly construct the program. Instead, information about the target programming language, as well as information about the relation­ ship of the target-programming language to the problem-statement language, is in another part of the PROW program--the "post-processor." The post­ processor then uses this information t·o convert the completed proof into a program. The post­ processor also converts recursion into loops and allows several target programming languages.

If our goal is to do automatic programming involving complex programs, we will probably wish to do some optimization or problem solving on the target language itself. For this reason we might want to have axioms that give the semantics of the target language, and also allow the intercommunica­ tion of information in the problem-statement lan­ guage with information in the target language. Two possibilities for how to do this efficiently suggest themselves: (a) Use the methods presented here in which all information is in first-order logic. To gain efficiency, use special problem­ solving strategies that minimize unnecessary inter­ action; (b) Use a higher-order logic system, in which the program construction is separated from the proof construction, possibly by being at another level. The program construction process might then be described in terms of the first­

order existence proof.

Problem Formulation. The axiomatization given here has considerable room for improvement: Missing portions of LISP include the program features and the use of lambda to bind variables. The functions to be written must be named by the user, and the number of arguments must also be specified by the

user.

Heuristics for Program-Writing Problems. Two heuristics have been considered so far. The first consists of examining the program as it is con­ structed (by looking inside the answer literal). Even though the syntax is guaranteed correct, the answer literal may contain various nonsense or

undefined constructions (such as car(nil)). Any clause containing such constructed answers should be eliminated . Another heuristic is to actually run the partial program by a pseudo-LISP inter­ preter on a sample probl em. The theorem prover knows the correct performance on these sample problems because they have either been solutions or else counterexamples to program- simulation questions that were stored in memory , or else they have been provided by the user. If the pseudo­ LISP interpreter can produce a partial output that i s incorrect, the partial program can be eliminated. If done properly, such a method might be valuable , but in our limited experience, its usefulness is not yet clear.

Higher- Level Programming Concepts. A necessary requirement for practical program writ­ ing i s the development of higher-level concepts (such as the LISP "map" function) that describe the use of frequently employed constructs (func­ tions) or partial constructs.

Induction. The various methods of proof by induction should be studied further and related to the kinds of problems in which they are useful. The automatic selection or generation of appro­ priate induction axioms would be most helpful.

Program Segmentation. Another interesting problem is that of automat i cally generating the specifications for the subfunctions to be called before writing these functions. For exampl e , in our system, the sort problem was divided into two problems: First, speci fy and create a merge function , next specify a sort function and then construct this function in terms of the merge function. The segmentation into two problems and the specification of each problem was provided by the user.

VII . Discussion

The theorem prover may be considered an "interpreter" for a high-level assertional or declarative l anguage--logic. As in the case with most high-level programming languages the user may be somewhat distant from the efficiency of "logic" programs unless he knows something about the strategies of the system.

The first applications of QA2 and QA3 were to "question answering." Typical question­ answering applications are usually easy for a resolution-type theorem prover. Examples of such easy problem sets given QA3 include the questions done by Raphael's SIR~ 1 Slagle's DEDUCOM~ 7 and Coorer's chemistry question­ answering program . 2 Usually there are a few obvious formulations for some subject area, and any reasonable formulation works well . As one goes to harder problems like the Tower of Hanoi puzzle , and program-writing problems, good and r easonably well-thought-out representations are necessary for efficient problem solving .

Some representations are better than others only because of the particular strategy used to search for a proof. It would be desirable if the theorem prover could adopt the best strategy for a given problem and representation, or even change the representation. I don't believe these goals are impossible, but at present it is not done . However, a library of strategy programs and a strategy l anguage is slowly evolving in .QA3. To change strategies in the present version the user must know about set-of-support and other program parameters such as level bound 1 and t erm- depth bound. To radically change the strategy, the us er presently has to know the LISP language and must be able to modify certain strategy sections of the program. In practice, several individual s who have used the system have modified the search strategies to suit their needs. To add and debug a new heuristic or to modify a search strategy where reprogramming is required seems to take from a few minutes to several days, perhaps averaging one day. Ultimately it is intended that the system will be able to write simple strategy programs itself, and "understand" the semantics of its strategies.

Experience with the robot applications and the automatic programming applications emphasize the need for a very versatile logical system. A suitabl e higher-order logic system seems to be one of the best candidates. Several recent papers are relevant to this topic. A promising higher order system has been proposed by Robinson~ 3 Banerji 24 discusses a higher order language. One crucial factor in an inference system is a suitable method for the treatment of the equality relation. Dis­ cussion of methods for the treatment of equality is provided by Wos and Robinson~ 4 and Robinson and Wos~ 5 and Kowalski~ 5 McCarthy and Hayes 5 include a discussion of modal logics.

The theorem-proving program can be used as an experimental tool in the testing of problem formu­ lations. In exploring difficult problems it can be useful to write a computer program to test a problem formulation and solution technique, s ince the machine tends to sharpen one's understanding of the problem. I believe that in some problem­ solving applications the "high-level language" of logic along with a theorem-proving program can be a quick programming method for testing ideas. One reason is that a representation in the form of an axiom system can correspond quite closely to one's conceptualization of a problem. Another reason is that it is sometimes easier to reformulate an axiom system rather than to rewrite a problem­ solving program, and this ease of reformulation facilitates exploration .

Resolution theorem-proving methods are shown in this paper to have the potential to serve as a general problem- solving system. A modified theorem­ proving program can write simple robot problems, and solve simple puzzles. Much work remains to be done before such a system is capable of solving problems that are difficult by human standards.

Acknowledgment

I would like to acknowledge valuable dis­ cussions with Dr. Bertram Raphael and Mr. Robert Yates .