A Paradigm for Reasoning by Analogy

A PARADIGM FOR REASONING BY ANALOGY

Robert E. Kling Stanford Research Institute Menlo Park, California U.S.A.

ABSTRACT

A paradigm enabling heuristic problem solving programs to exploit an analogy between a current unsolved problem and a similar but previously solved problem to simplify its search for a solu­ tion is outlined . It is developed in detail for a first-order resolution logic theorem prover. Descriptions of the paradigm, implemented LISP programs, and preliminary experimental results are presented. This is believed to be the first system that develops analogical information and exploits it so that a problem-solving program can

speed its search.

INTRODUCTION

An intelligent man thinks deeply and learns from his past experiences. Contemporary theorem­ proving and problem-solving systems are continu­ ally designed to think ever more deeply and to ignore their past completely . A problem solver designed in any of the contemporary paradigms (such as resolution (1), GPS (2), and REF-ARF (3)) solves the same problem the same way each time it is presented. A fortiori, they are unable to exploit similarities between new and old problems to hasten the search for a solution to the new one . ZORBA, outlined in this paper, is a para­ digm for handling some kinds of analogies.* This is the first instance of a system that derives the analogical relationship between two problems and outputs the kind of information that can be use­ fully employed by a problem-solving system to expedite its search. As such, ZORBA is valuable

in three ways:

1. It shows how nontrivial analogical reason­ ing (AR) can be performed with the tech­ nical devices familiar to heuristic pro­ grammers, e.g., tree search, matching,
2. and pruning.

* In Ref. (4), I show that there are several kinds

of analogies from an information-processing point of view. We should hardly expect one paradigm to include them all. Restrictions on the varieties of analogy handled by ZORBA are described in the section entitled "Necessary Conditions for an Analogy . "

1. It provides a concrete information­ processing framework within which and against which one can pose and answer questions germain to AR.
2. Since it is implemented (in LISP), it is available as a research tool as well as a gedanken tool.

The last two contributions are by far the most important, although our attention will focus upon the first. In the 50's and 60's, many researchers felt that analogical reasoning would be an impor­ tant addition to intelligent problem-solving pro­ grams. However, no substantial proposals were offered, and the idea of AR remained rather nebu­ lous, merely a hope. ZORBA may raise more ques­ tions of the "what if?" variety than it answers. However, now, unlike 1968, we have an elementary framework for making these questions and their

answers operational.

ZOR!li\ PARADIGI

Although prior to ZORBA there were no concrete paradigms for AR, there was an unarticulated un­ developed paradigm within the artificial intel­ ligence zeitgeist. Suppose a problem solver had solved some problem P and has its solution S. If a program is to solve a new, analogous PA, it should do the following:

1. Examine S and construct some plan (schema) s' that could be used to generate s.
2. Derive some analogy G: p .... P . A
3. Construct G- 1 (S 1 ) (3) = s' A.
4. I Execute S A to get SA' the solution to P . A

If P was solved by executing a plan, then s' would be available and step (1) could be omitted . Although nobody has explicated this idea in pub­ lications, from various conversations with workers in the field, I believe that the preceding descrip­ tion is close to the paradigm that many would have pursued. As such, it constitutes the (late-GO's) conventional wisdom of artificial intelligence. Certainly this (planning) paradigm is attractively elegant! However, in 1969, when this research was begun, it was an inappropriate approach for two reasons:

1. There are no planning-oriented problem solvers that are fully implemented and operate in a domain w~th interesting nontrivial analogies. This state of

---- * PLANNER at MIT and QA4 at SRI are two current planning-oriented problem solvers that are under development. The first is partially implemented and the second exists only on paper. It is not yet clear what problem-solving power PLA~~~R will have, and how effective it will be in domains

with interesting analogies.

R. E. KLING

affairs probably will change in the next few years, but it now renders difficult any research that depends on the existence of such a system.

(2) Given the plans generated by such a sys­ tem, it is hard to know a priori at what level of generality the derived analogy will map into an executable analogous plan. · If S~ fails, is u too strong, or wrong? Should u be modified and a variant S~ computed, or should the system keep G, and just back up its planner and gene­ rate an alternative subplan using its own planning logic? At best this is a rather complex research issue which would in­ volve a good planning-oriented problem solver as an easily accessible research tool. At worst, the preceding paradigm may be too simple and the development of a suitable u may be interactive with how much successful problem-solving has pro­ ceeded so far. (A complete u should not be attempted before some problem solving begins and is extended as needed in the course of solving PA.)

Happily, there is an alternative approach that circumvents the preceding difficulties. Consider a system that has solved some problem P and is posed with a new (analogous) P to solve. Clearly, it must operate on some large ~ata base sufficient to solve both P and PA. (See F1gure 1.) In ad­ dition to the subbase for solving P and PA there

are likely to be even more theorems. in the set D - (D 1 \., DA). Now, given P it is impossible to infer a minimal n 1 . In practice, a user may se­ lect some n 2 s . t. n 1 = D c D which the problem solver will access to so~ve P. If one studies the searches that problem solvers generate when they work with nonoptimal data bases, it is ob­ vious that many of the irrelevant inferences that are generated are derived from the data-base as­ sertions (theorems, axioms, facts) in D - n 1 (or D 2 - D 1 ). In fact, as the number of theorems ir­ relevant to the solution P becomes large, the number of irrelevant inferences derived from this set begins to dominate the number of irrelevant inferences generated within D and its descendants alone.* In fact, while a proGlem solver might solve P given an adequate and small n 1 , it may be swamped and run out of space before a solutfon given a n 2 that is much larger than needed. Clearly, one effective use of analogical informa­ tion would be to select a decent subset o 2 of D such that size [D] s size [D 2 ] <<size [D). For example, a typical theorem in algebra provable by QA3 5 --a resolution logic theorem proof--may re­ quire only 10 axioms (D 1 ) while the full alge­ braic data base has 250 axioms. If a system could select a o 2 such that size[D 2 l = 15 axioms, a massive saving in search could be had. In fact, the theorem that would be unprovable on a D with size[D] = 250 would now be provable.

· See Ref . 4 for a discussion of this issue.

A second kind of information that would be useful to help solve PA would be a set of lemmas (or subgoals) L 1 , ... L . whose analogs u(L 1 ), ... u(L_) could be solved b~ the system before at­ tem~ting P A.

At this ~oint I will not discuss h~w to recog­ nize a leiiiiiiB and generate its analog; instead, I merely want to note that lemmas may be effec­ tively used without using a planning language

· Even given an optimal data base, a problem solver will generate some irrelevant inferences.

t In general, automatic problem solvers and theorem provers run out of space rather than time when they fail to solve a problem. Ernst(2) empha­ sizes this point with regard to GPS, and I have had similar experiences with QA3(5), a resolu­ tion logic theorem prover.

* Recognizing lemmas depends upon the problemsolving system. For example, in resolution logic, some good criteria for lemmahood are:

(1) A ground unit used more than twice (or k times) in a proof.

(2) A unit that is a merge.

(3) A clause that is the "least descendant" of more than 2 (or k) units.

§ Generating a lemma depends upon the system's ability to associate variables with variables and that may be tricky when skolem functions are introduced.

R. E. KLING

that forces backup in case of failure. Suppose we somehow get u(L 1 ), ... u(Lj). A typical planner would order the u(L 1 ), e . g., u(L 1 ), u(~) ... etc., attempt to solve them in sequence, and stop if any lemma fails to be solved. In contrast, we merely need to attempt each u(L. ). If we get a solution, 1 · add u(Li) to the data base (like a theorem) and continue with the next lemma . If we fail, con­ tinue anyway. At worst, we wasted some computation time. Each useful u(Li) decreases the number of steps in the solution of PA and may decrease the depth of the solution tree . Thus, lemmas are helpful in getting a faster solution. Note, how­ ever, that a successful u(Lj) need~ be used in the solution of PA . It is merely available. Thus, we are not bound by the fail-backup orienta­ tion of sequential planning logics.

In summary, if we use analogical information to modify the environmentt in which a problem solver operates, we can effectively abbreviate the work a problem solver must perform. Of course, a well-chosen environment will always lead to a more efficient search . Usually, we have no idea how to tailor a subenvironment automatically to a par­ ticular problem. Here we do it by exploiting its analogy with a known solved problem. Now, the representations used, the analogy-generating pro­ grams, and the types of additional information output will depend upon the problem-solving system (and even the domain of application). Any further discussion needs to specify these two items.

APPLICATIONS TO RESOLUTION LOGIC

The preceding discussion referred to ~ problem solver and is just a proposal. Computer programs have been implemented to apply this para­ digm to a resolution logic theorem prover, QA3.(5) For the class of analogies these programs handle, this is an accomplishment. When we begin to focus upon a particular paradigm, two issues are more easily resolved:

· In fact, under some conditions, the axioms used to solve u(Li) may be deleted from o2 so that size [0 2 ] is decreased, and u(Li) is not at­ tempted again inadvertently during the solution of P . t A

Here environment is synonymous with data base. But it can also include permissible function orderings (in predicate calculus) and other kinds of restrictive information. Each rule restricting the "environment" could be translated into an equivalent new decision rule restricting the ap­ plication of the inference procedures of the problem solver . However, I find it easier to think of ZORBA in terms of modified environments rather than (the equivalent) modified decision rules.

1. What kinds of information are most useful to provide to the problem solver?
2. Which representations shall we use to describe the analogies and handle the necessary data?

Resolution logic is an inference rule whose statements are called clauses . *(1),(5) Thus, a resolution-oriented analogizer will deal with clauses and their descriptions. In contrast, GPS uses sets of objects to describe its states, and we would expect that an analogy system devoted to GPS would deal with (complex) objects and their attributes. Table 1 contrasts the kinds of in­ formation helpful to QA3 and GPS. An analogy facility developed for GPS would be oriented to its peculiar information structures instead of clauses and axioms indigenous to resolution.

Table 1

KINDS OF INFORMATION HELPFUL TO QA3 and GPS

QA3 (Resolution)	GPS
Relevant axioms	Relevant operators
Expected predicates	Abbreviated difference table
Lemmas	Subgoals
Admissible function nestings	Restrictions on operator applications

I want to digress briefly and describe the kinds of theorems that the implemented system, ZORBA-1 1 tackles. Briefly, they are theorem pairs in domains that can be axiomatized without con­ stants (e.g., mathematics) and that have one-one maps between their predicates. The theorems are fairly hard for QA3 to solve. For example, ZORBA-I will be given proof of the theorem

• Tl. The intersection of two abelian groups is an abelian group

and is asked to generate an analogy wjth

• T2 . The intersection of two commutative rings is a cummutative ring .

A clause is an element in the conjunctive normal form of a skolemized wff in the predicate cal­

V father [g(x); x] is the clause associated with: ~x person [x] ~ 3y father [y;x] (every person

· culus. For example: ~person [x] has a father).

t;1ven

• T3. A factor group G/ 11 1s simple iff H is a max1mal normal subgroup of G.

Generate an adequate analogy with

• T4. A quotient ring A/ C is simple iff C is a maximal ideal 1n A.

~one of these theorems arc trivial for contemporary theorem provers. (See Table 2, in a later section, for a l1st1ng of addltional theorem pa1rs.) T 1 has a 35-step proof and T 3 has a 50-step proof in a decent axiomatization. A good theorem prover (Q..\3) generates about 200 inferences in searching for either proof when its data base is minimized to the 13 ax1oms required for the proof of T 1 or to the 12 ax1oms required for the proof of T 3 . If the data base 1s 1ncreased to 20-30 reasonable ax1oms. the theorem prover may generate 600 clauses and run out of space before a proof is found. Sote also that the predicates in the prob­ lem statement of these theorems contain only a few of the predicates used in . any proof. Thus, T 1 can be stated using only L ISTERSECTION; ABELlA:>}, but a proof requires (GROL'P; l:S; TIMES; St:BSET; SL'BGROL'P; CC»Nl'TATIVE} 1n add1t1on. Thus, while the first set is kno~n to map into [INTERSECTION, CQI.t\ll'T.-\TI\t:RISG}, the second set can map into anyth1ng.

Figure 2 shows a set P including a 11 the pred1cates in the data base .

We know Pi and P;, the sets of predicates 1n the statements of the new and old theorems, TA and T. In a dd1tion, we know the predicates P1 in some proof of T (s>nce we have a proof at hand). We need to find the set P2 that contains the rela­ t>ons we expec t 1n some proof of TA , and we want a map G: G(P 1 ) P 2 .

R. E. KLING

Clearly, a wise method would be to find some G', a restriction of G toP{ such that G'<Pi> = I Ul G.' G.' P 2 . Then incrementally extend to 1 , 2> ... each on larger domains until some G'<P 1 ) = P 2 . ZORBA-1 does this in such a way that each incre­ mental extension picks up new clauses that could be used in a proof of TA. In fact, if we get no new clauses from an extended G.j, that may be rea­ son to believe that a; is faulty. The next sec­ tions will describe the generation algorithm in a little more detail.

ZORBA'S REPRESE:STATION OF AN ANALOGY

In the preceding sections I have implied that an analogy is some kind of mapping. The ZORBA paradigm--e.g., using an analogy to restrict the environment in which a theorem prover works--does not restrict this mapping very much. For differ­ ent intuitively analogous theorem pairs, this mapping would need to be able to associate predi­ cates (and axioms) in a one-one, one-many, or many-many fashion, possibly dependent upon con­ text. For other theorem pairs, one-one mappings and context-free mappings are adequate. ZORBA-1 is a particular set of algorithms that restricts its acceptable analogies to those which map predicates one-one with no context dependence. It allows one-many associations between axioms; e . g., one axiom of the proved theorem is asso­ ciated with one or more axioms that will be used to prove the new, analogous theorem. More ex­ plicitly, a ZORBA-1 analogy G is a relation GP x Gc x GV, where:

1. Gp is a one-one map between the predi­ cates used in the proof of the proved theorem T and the predicates used in the proof of the unproved theorem TA.
2. Gc is a one-many mapping between clauses. Each clause used 1n the proof of T is associated with one or more clauses from the data base D that ZORBA-1 expects to use in proving TA.
3. Gv is a many-many mapping between the variables that appear in the statement of T and those that appear in the state­ ment of TA.

D1fferent sections of ZORBA-1 use these various maps, e.g., GV and/ or GP and/ or Gc. t:sually I will drop the superscript and simply refer to "the analogy G." Thus "the analog of an axiom ax under analogy G" should be understood to mean ~c[ax 1, and will often be mentioned . .. k " s1mply as the analog of axk.

In the prev1ous section I refer to a sequence of analogies G 1 , ... Gk. ZORBA-1 usually does J;~Ot develop GC in one step. Rather, it

R. E. KLING

incrementally extends some limited analogy into one that maps a few more variables, predicates, or clauses. This process is described in full detail in the next few sections. Here, I just want to define several terms that refer to this process. When I refer to "the analogy between T and TA" I refer to a mapping that includes every variable in the statement of T, and every predicate and clause used in the proof of T. This "complete" mapping is obtained as the final step of a sequence of mappings that contain the associations of some predicates and some clauses. I refer to these incomplete mappings as "partial ana 1 og i e s · " In add i t ion, an important relationship analogies . A (partial or an extension of a Gj , e.g., �~, �~, the corresponding partial Gv . J, lS submap we are concerned with between two (partial) complete) analogy ~ is analogy Gj if some of a submap restriction of Gk to a smaller domain. Intuitively, when we add a new predicate or clause association to Gj so as to create Gk, we say that GJ has been extended to Gk. We are now ready to survey ZORBA-I.

AN OVERVIEW OF THE ANALOGY-GENERATING ALGORITHM

I want to describe the ZORBA-I algorithm in two stages, first briefly in this section and then in greater detail in the following two sections. I will precede these descriptions by some background on the representations and information available to the system.

ZORBA-I is presented with the following:

1. A new theorem to prove, TA.
2. An analogous theorem T (chosen by the user) that has already been proved.
3. Proof[T] that is an ordered set of clauses ck s . t . ~k ck is either
4. (a) A clause in~ T
5. (b) An axiom
6. (c) Derived by resolution from two clauses c and c i .i j < k and i < k.

These three items of information are problem­ dependent. In addition, the user specifies a "semantic templilte" for each predicate in h1s language. This template assoc1ates a semantic category with each predicate and predicate-place and IS used to help constrain the predicate mappings to be meaningful. For example, STR~CTVRE[SET; OPERATOR] is associated with the predicate "group . Thus, ZORBA-I knows that "A" IS :1 set and "·· is an opera tor when it sees group[A; ·]. Currently, the predicate types (for algebra) are STRL:CTL'RI:: , REl.ATIO!'\, MAP, and REL­ STRL'CTL'RJ::; the variable types :Ire SET, OPERATOR, F~SCTIOS, nnd OBJECT.

In addition, ZORBA-I can make up a description descr[c] of any clause c according to the fol­ lowing rules regarding the predicates of c.

1. V s.t. p and~ p appear inc, impcond[p] p - £ descr[c].
2. V s.t. p appears inc, pos[p] C descr(c].
3. Vp s.t . ~ p appears inc, neg[p] £Pdescr[c].

Thus, the axiom, every abelian group is a group,

is expressed by the clause

which is described by

neg [abelian], pos [group]

Each element of a description, e.g., pos[group] , is a ''feature" of the description. Each feature corresponds to one predicate, so the number of features in ·a clause equals the number of predi­ cates in the clause. The theorem, the homomorph1c image of a group is a group, e.g.,

is expressed by the clause

and is described by

'J'.o·o different clauses may have the same description. Let :

Then:

descr[c ] = descr[c ] 3 4 neg[ intersection], pos[subset] .

Clause descriptions are used to characteri ze the ax1oms whose analogs we seek. ZORBA-I selec t s as analogs clauses that have descriptions that are close to the analogs of the descriptions* of axioms in the knovm axiom set. Although in a special context ZORBA-I actually uses an ordering relation on a set of descriptions to find a "best clause ,·· it usually exploits a simpler approach . We will say that a clause c satisfies a description d iff d S descr[c]. Thus, several clauses may sat1sfy the same descr1ption.

*The "analog of a description" is defined later .

Let:

c 6 : ...., subgroup[x; y; ·J V-, subset[x; y] Then, the following statements are true :

1. [c 2 ,c 5 } satisfy impcond[group]
2. [c 1 ,c 2 ,c 5 } satisfy pos[group]
3. ~l satisfies neg[abelian], pos[group]
4. [ cJ,c 4 ,c 6 } satisfy pos[subset]
5. c 6 satisfies neg[subgroup], pos[subset]
6. No clause of these six satisfies pos[intersection]

Clearly, if a description contains only a few features, then several clauses may satisfy it.

The semantic templates are used during both the INITIAL-MAP (when the predicates and variables in the theorem statements arc mapped) as well as in the EXTE~~ER, which adds additional predicates needed for the proof of TA and finds a set of axioms to use in prov1ng TA· The clause descr1p­ tions are used only by EXTE~~ER.

intend the br1ef description that follows to provide a n overview of ZORBA-I in preview to the next two sections of text, which describe it in cons1derable detail. In addition, this preview sect ion may be a helpful ''roadmap" for reference when the rea der immerses himself in the details

that follow later on.

ZORBA-l operates in two stages. IJ\ITIAL-MAP 1s applied to the statements of T and TA to create an Ci, wh 1c h is us~d by EXTE~~ER to start its se­ quence of Gj and CJ' which terminate in a complete G. 1:'\ITI.-\.L-~IAP starts without a priori informa­ tlon about the analogy it is asked to help create. Both GP and Gv are empty ..:hen it begins. It uses the system of the wffs that express T and TA as well as the restrictions imposed by the semantic categories to generate �~ and Gl that include all the predicates and variables that appear in the two wffs. For example, the statements of T 1 - T 2 can contai n three of the nine pred1cates used in proof[T 1 ] and the statements of T 3 - T 4 can con­ ta1n five of the 12 predicates used in proof[T 3 ]. In brief, it provides a starting point from which

EXTEYDER can develop a complete G.

The INITIAL-~IAP uses a rule of inference ca lled ATCMMATCH[a tom 1 ; a tom 2 ; C], which extends analogy by adding the predicates and mapped var1ables of atom 1 and atom 2 to analogy G. Thus, ATOMM'}.TCH now llmi ts ZORBA-I to analogies where atoms in the statements of T and TA map one-one. l!'IITJAL-~IAP 1s a sophisticated search program

· Atoms, not pred1cates .

R. E. KLISG

that sweeps ATClrllt.IATCll over likely pairs of atoms, one of which is from the statement of T, the other from the statement of TA . Alternative analogies are kept in parallel (no backup), and INITIAL-~IAP terminates when it has found some analogy that in­ cludes all the predicates in the theorem state­ ments. This one is output as ui.

EXTE~~ER accepts a partial analogy generated by !1\ITIAL-MAP and uses it as the first term in a sequence of successive analogies uJ. The ax1oms used in proof(T] are few in comparison to the si~e of the large data base and compnse the "domain" for a complete uc . For each axiom used in proof[T], we want to find a clause from the data base that is analogous to it. The axioms used in proof[T] are called ~XSET and are used by EXTE~~ER in a special way. Each partial analogy Gj is used to partition ~XSET into three disJoint subsets called

ALL[GJ, S(J.IE[G,J, and :'\ONE[G 1 ] .

If all the predicates in an ax1om axk C AXSET are in GP , then ax is 1n ALL[G ]; if some of its predicat~s are in tP, then axk ls in SOME[G]; J .. p J and if none of its predicates are in GJ' then axk is in NONE[G ] , For brevity, these sets wi 11 be called ALL, Sor.~, and :'\0~~, and their dependence on GJ will be implicit. This part1tion is tnvial to compute, and initially, none or a few axk are in ALL, and most axk belong to sor.~ and NO~~ . We want to develop a sequence of analogies GJ' J = 1, . . . n, that contain an increasingly l:lrger set of predicates and their analogs. If an ax1om is con­ tained in ALL, then by definition we know the ana­ logs of each of its predicates. It cannot assist us in learning about new predicate associations , In contrast, we know nothing about the analogs of any of the predicates used in axioms contained in !\ONE. Analog clauses for these axioms are hard to deduce since we have no relevant information to start a search. Unlike these two extreme cases, the axioms in sor.~ are especially helpful and will become the focus of our attention. For each such axiom we know the analogs of some of its predi­ cates from GJ . These provide sufficient informa­ tion to begin a search for the clauses that are analogous to them . When we finally associate an axiom with its analog, we can match their respec­ tive descriptions and associate the predicates of each that do not appear on uP . We can extend GJ to Gj +l' and thus the analog~ of axioms on S~ provide a bridge between the known and the un­ known, between the current G . and a descendent J Gj+l" When EXTENDER has satisfactorily terminated, ALL = AXSET, S~ = NONE = ~. So the game becomes finding some way to systematically move axioms from NONE to S(J.~ to ALL in such a way that for I each axk moved, some analog Gj[axk] = axk is found that can be used in the proof of T A. Moreover, each new association of clauses should help us extend uj ~ uj+l by providing information about predicates not contained in u . . J

A DETAILED DESCRIPTION OF INITIAL-MAP

At heart, ZORBA-I is a heuristic program de­ siened to generate analogies between theorem pairs stated in a subset of predicate calculus. It has been designed and implemented in a fairly modular aanner to facilitate understanding and ease of generalization. Thus, much of the system can be described in algorithmic terms. In this sect ion I hope to blend some appreciation of the heuristic foundations of the program while describing its operation with algorithmic clarity. ZORBA-I uses an interesting set of searching and matching rou­ tines, which have been empirically designed, generalized, and tested on a set of problem pairs CT 1 - T 2 and T 3 - T 4 are fair representatives of this set). The control structures of INITIAL-MAP and EXTENDER have been designed to pass fairly similar structures to the various match routines (described below). Thus, the following descrip­ tions will cover cases where the structures to be mapped are fairly similar. For example, most of the routines that match sets of items assume that the sets are of equa 1 cardinality and that they will map one-one . Such assumptions are valid for a large class of interesting analogies (such as the group-ring analogy in abstract algebra) and simplify the description of the various proce­ dures. Analogies that require weaker assumptions and more compl~x procedures are described else­ where . (6)

In the previous section I motivated the design of INITIAL-MAP and EXTENDER, which generate a re­ stricted analogy and expand it to cover all the relations and axioms necessary for the new proof. ZORBA-1 can be easily expressed in terms of these two functions as follows :

· zorba 1 [newwff; oldwff;AXSET ] :

• (l) Set analogies to the list of analogies generated by initial map[neww·ff; oldwff].
• Apply extender[analogy; AXSET] to each analogy or analogies.
• Return the resultant set of analogies.

The preceding description allows that there may be more than one analogy generated by either INITIAL-MAP or EXTEJ\"DER. In practice, however, each tends to generate but one (good) ana logy . In the following paragraphs I will describe INITIAL-MAP in some detail. EXTENDER will be dis­ cussed in the next section.

· ~XSET is the set of axioms that appears in proof[T).

INITIAL-MAP is designed to take two first­ order predicate calculus wffs and attempt to gene­ rate a mapping between the predicates and variables that appear in them. The variable mapping infor­ mation is used to assist INITIAL-MAP in mapping predicates in cases of seeming ambiguity; INITIAL­ MAP outputs a set of associated predicates that appear in the statements of TA and T. This re­ stricted mapping is used as a starting analogy by EXTENDER, which finds a complete mapping for all the predicates used in proof[T]. As a byproduct EXTENDER finds analogs for each of the axioms on AXSET. INITIAL-MAP (unlike EXTENDER) does not reference AXSET, the set of axioms used to prove T, and is symmetric with respect to caring which wff represents the proved or unproved theorem. INITIAL-MAP uses atommatch[atoml;atom 2 ; u] as a rule of inference to add the predicate/ variable information to analogy G. As its name hints, ATOMMATCH matches the predicates and variables of its atomic arguments and adds the resultant mapping to the developing analogy (u) .

ATOMl~TCH is used as an elementary operation by every matching routine in the INITIAL-~~P system (Figure 3). Thus, we will discuss it first

and then consider how INITIAL-MAP is organi?cd to apply it intelligently. Consider how· we might write an ATct.II-~TCII. Suppose, atom1 and atom2 arc of the same order (same number of variables) and each variable place in each atom h.'ls the same se­ mantic type. For example, let

Clearly, we want

intersection intersection

and

So, if atom 1 p[xl;

and atom 2 q [y 1;

and p = q (thus, n = m)

we will set p q

So far ATOMMA~H is quite trivial. Suppose, however, P I q or n I m.

Clearly we want to associate the set x with the set y and the operator · 1 with either or both of · 2 and + 2 . ATOMMA~H can know which variables represent sets, etc., by checking the semantic templates associated with group and ring. Now, the template associated with group is structure [set;operator] while that associated with ring is structure[set;operator;operator]. We will map variables with each other so as to preserve predicate place ordering and semantic type. To handle the unequal number of variables, we will temporarily expand the atom group [x; · 1 1 to in­ clude a dummy variable of type operator, "dummyop," and will rewrite it as group[x,*l; dummyop]. The symbol "dummyop" is used to expand either (or both) atoms to be of the same order and a variable (possibly dummy) of the same se­ mantic type in corresponding places in each atom. Then we can map the variables one-one in order of appearance. For example we can associate

xn]

y ]

m

and

Then we can remove dummyop and rewrite

We can describe this process formally in two

stages.

1. Make the two atoms type-compatible and of the same order by adding dummy variables whenever necessary.

* I will use a double-headed arrow ...... as in "x - y" to mean "x i,; as soc ia ted with (analogous to) y."

R. E. KLING

Furthermore, suppose that the ordering of the types is the same in each template, even though the number of variables of each particular type need not be identical for corresponding "type blocks." Thus, in the preceding example, in both "group" and "ring" the type .!!! precedes the type operator. Each template has one set variable, but a differing number of operator variables. Thus, we could par­ tition the ordered set of variables in atom 1 and atom 2 by letting some xi and xi+l belong to the same partttion if type[xi = type[xi+l]. Now there are an equal number of pa~titions in both atom 1 and atom 2 . Returning to our example, we partition group[x; · 1 1 into [[x],[· 1 Jl and the ring[y ; · 2 ;+ 2 ] into [[y] 1 [* 2 ;+ 2 ]]. (The brackets indicate that the order of elements is preserved.)

1. Map the partitioned subsets into each other, preserving their order within the partitions, and map elements into elements if the two subsets have an equal number of elements.

This completes our brief description of ATOMMA~H. From now on, we will consider ATCNMA~H as an elementary operation that will expand the de­ veloping analogy to include a (possibly) new predi­ cate pair and (possibly) new pairs of variable associations. We need to know how to select pairs of atoms from the statements of T and TA to be ATCNMA~ed.

We have two wffs representing T and TA as arguments of INITIAL-MAP, and we want to find some way to slide ATOMMA~ over pairs of atoms se­ lected from the wffs. First, note that the syntax of the wffs may be a helpful guide in selecting potential matches .

where A and Bare any wffs .

We would presume that p- q (predicates)

where we expect that wffs A and B would be decom­ posed down to atoms for AT~~~H . If A and B had implication signs in them, we could decompose them similarly . There are many possibilities for the forms of T and TA. We find that if T and· TA are closely analogous, then their syntactic forms are likely to be very similar . ZORBA, considers T and TA to have the formats that can be repre­ sented by the generat i ve grammar below

INITIAL-~~P is designed to decompose the in­ put wffs T and TA into associated syntactic sub­ structures until a subwff is either an atom

p[x 1 . .. xn) or a conjunction of atoms

At this point it enters a hierarchy of selecting and matching routines (Figure 3) to decide which pairs of atoms shall be A~~~TCHed. Naturally, if the subwffs are just atoms it calls ATCII!MATCH directly . Otherwise, it enters a program hier­ archy headed by a routine named SETIMTCH, which selects appropriate atom pairs from the sets of conjuncted atoms in the subwffs.

In the following discussion, the number of atoms conjuncted in each set are assumed equal (k = l). SE'Th~TCH can be described in terms of its subfunctions as follows:

1. Partition the atoms in set 1 and set 2 into subsets that have identical semantic templates (a "semantic partition"). Thus if set 1 is group[x ; *) A abelian [y; *] A intersection[z;x; y) the se­ mantic partition will be {( intersection[z;x;yJ} {group[x; *], abelian[y; *] }} since ~ and abelian are both of type ~[set;op).
2. Select the partitions of set 1 and set 2 that have but one element and call these sing 1 and sing 2 , respectively.
3. The remaining partitions have more than one element; call them mult 1 and mult 2 , respect 1 ve ly .
4. ( 4) ~latch the a toms in sing 1 with those in sing 2 by executing singlematch[sing 1 ;
5. (S) Match the remaining atoms by executing
6. sing 2 ;ana).
7. multimatch[mult 1 ; mult 2 ; ana].

SETilATCH, SII\GLDL'ITCH, and ~1l' LTB1ATCH are all heuristically designed one-pass matching strate­ gies that make strong assumptions about the na­ ture of the theorem statements T and TA for an analogous theorem pair .

· \\'hen an ana logy G. is referenced within the description of an algorithm, it will be represented a~ a variable ana wherever that is more convenient.

SE'Th1ATCH assumes that the atoms in set 1 and set 2 will map one-one and that the serna·ntic parti­ tions will map one-one. Suppose, we have a se­ mantic partition thus:

SE'Th~TCH assumes that {atoms} and [atom 10 } will correspond, rather than [ atoms} and, say {atom 6 atom 7 }. It calls SIN�LE~~TCH to map the single­ atom partitions onto the single-atom partitions.

In addition, it calls MULTI~TCH to map , in pairs, the partitions containing several ~toms

each.

Mt:LTH~TCH assumes that the analogy will pre­ serve semantic type sufficiently well so that atoms within a particular partition will corre­ spond only to atoms in one other partition .

It forbids matches across partitions , such as

SIN�L£~1ATCH and Mt:LTBt4.TCH also share a common default condition. If all but one of the element s of a set X are mapped with all but one of the ele­ ments of a set Y, then these two elements are as­ sociated by default without any further decjsion making . In SII\�L£~1ATCH the sets X and Y are sets of atoms or partitions of atoms.

SIK�LE~LI>.TCH [set 1 ;set 2 : ana] ma y be easily de­ scribed in terms of this default condition and a function called tempsift[s 1 ;s 2 :testfn;ana ). TEMPSIFT applies ~[x; y] to the first elemen t of s 1 and ea~h successive element y of ~ 2 it finds a y t s 2 such that testfn[x;y] lt then executes until = T.

increments to the next element of x of sl, and seeks another y" t s 2 , such that testfn[x· ;y" ] = T, etc. Thus , for every x € s 1 , it finds the first y t s 2 such that testfn[x;y) = T and exe­ cutes atommatch[x;y) = T. Typical ~scheck whether x and y have the same semantic template or are analogs of each other according to the de­ veloping analogy,~ · Singlematch[set 1 : set 2 : ana]: =

1. If set 1 and set 2 have but one element ( 'terminal default condition"), go to 8 .

1. Execute tempsift[set 1 ;set 2 ;testfn 1 ;ana], where testfn 1 [x;y] is true iff x and y have the same semantic template.
2. If set 1 and set 2 are empty, go to 9. If the terminal default condition is true, go to 8.
3. Execute tempsift[set 1 ;set 2 ;testfn 2 ;ana], where testfn2[x;y] is true iff the pre­ dicate letter in atom y is the analog of the predicate letter of that in atom x according to analogy ~·
4. If set 1 and set 2 are empty, go to 9. If terminal default conditions holds, go to 8.
5. Execute tempsift[set 1 ;set 2 ;testfn 3 ;ana], where testfn 3 [x;y] is true iff the type of the predicate appearing in atom x is the same as the semantic type of the predicate appearing in atom y.
6. If set 1 and set 2 are empty, go to 9 . If the terminal default condition holds, go to 8. Otherwise print an error message and halt.
7. Apply ATCX>IMATCH to the remaining atoms of set 1 and set 2 .
8. STOP.

To illustrate the preceding algorithm with a simple example, let

Step 2 associates

intersection[x;y;z] ~ intersection[u;v;w]

and the terminal default condition associates abeliangroup[x ; *] ~ commutativering[u; *;+]

Ml'LTIMATCH is a little more complex than SI!'IGLEMATCH . First we need to decide which par­ titions are to be associated before associating atoms within partitions. Suppose we have two sets of partitions set 1 and set 2 . If both sets have but one partition each (a common case), then we expect these to be associated by default and declare them accordingly. Secondly, if in some partition of set 1 there is an atom with predicate p which is known to be analogous to predicate q, then the partition in set 2 that con­ tains q should be associated with that which con­ tains p . Remember that these partitions were constructed on the basis of semantic templates. Thus, while several atoms containing a predicate p may be in a particular partition, there will be only one partition that contains atoms with predicate p . Lastly, if in set 1 and set2 there 1s but one partition that contains atoms whose predicates have the same type, e.g . , STRUCTURE, then we expect these partitions to be associated. Let MULTIMATCHl name the function that actually associates atoms within a partition according to analogy ~·

MULTIMATCH[set 1 ;set 2 ;ana):=

1. If the terminal default condition for partitions holds, go to 7.
2. Let pred[x) = the predicate letter of atom x . For each partition y, sequence through each atom x & y. If pred[x) is on analogy ~ find the partition z t set 2 such that the analog of pred[x] ap­ pears in z. Execute MULTIMATCHl [y ; z;ana] for each such pair y,z.
3. If the terminal default condition holds, go to 7 . If set 1 and set 2 are empty, go to 8 .
4. For each partition y t set 1 , select the first atom x. Find a partition z c set 2 such that the type of predicates in z equals type [x]. If there is only one such z c set 2 , execute MULTIMATCHl[y ; z ; ana] .
5. If the terminal default condition holds , go to 7. If set 1 and set 2 are empty, go to 8.
6. If set 1 or set 2 is still not exhausted, print an error message and halt .
7. Apply MULTIMATCHl to the remaining parti­ tions in set 1 and set 2 .
8. STOP .

Each set of atoms in a partition has the same semantic template. This property defines a par­ tition. Thus, at the level of abstraction pro­ vided by the templates, all of these atoms are alike and any differences need to be discriminated by other criteria. Let us consider an example to motivate the design of MULTIMATCHl. The theorem

pair T 3 - T 4 can be written as:

leads us to deduce :

although we could have also deduced this last association by our terminal default condition. Notice that "· 1 " is not a discriminating variable ~ince it appears in both group[g ; · 1 J and simple­ group[x; · 1 ]. After each atom pair is associated, we apply AT~n~TCH to it to deduce more variable associations and update our analogy.

R. E. KLING

I I when it decomposes T 3 - T 4 into subwffs distinguished by the syntax of the implication sign. Later an application of SINGLEMATCH adds:

factorstructure factorstructure

MULTIMATCH is passed one partition from each wff. T~ contributes

and T~ contributes

If we apply the MULTIMATCH algorithm just described to each of these partitions, we find:

• Step 1. We do not satisfy the terminal de­ fault condition.
• Step 2 . None of the predicates that appear in these partitions appear on the current analogy. We gather no new
• information here.
• Step 3. We still do -not satisfy the terminal default condition .
• Step 4 . We want to use MULTIMATCHl to asso­ ciate the atoms in these partitions .

Of these two partitions, the former pair have the template structure[set;operator] and the latter pair have structure[set ; operator;operator] .

Fortunately, our analogy has variable mapping in­ formation that is quite relevant here. We know that:

We can assume that if some variable appears in only one atom in a partition, the anilogous atom is one that contains its analog variable, if it too appears in only one atom. For example, the variable "g" appears only in group[g; · 1 ], and its analog "r" appears only in ring[r ; · 2 ; + 2 J. So, we deduce:

A similar argument based upon

The preceding description of MULTIMATCHl can be simplified and generalized by reali z ing that we are just using a specialized submap of the de­ veloping analogy to extend it further. This spPcial submap is just that mapping of variables where each variable appears in only one atom of the partition . In the preceding example, the submap was just:

Multimatchl[partition 1 ;partition 2 ; ana] : =

1. Set t 1 to a list of variablP.s that appea r
2. in only one atom of partition 1 .
3. Set t 2 to similar list computed on parti tion 2 .
4. ( I I I I I (3) Set anaprs = x - y x € £ 1 , Y € 1 2 and y 1 is the analog of x 1 by ana} .
5. Execute tempsift[partition 1 ; partition 2 ; testfn4; ana], where testfn 4 [u ; v] is 1 true iff for some variable pair x 1 ~ y € anaprs variable x 1 appears in atom ~and variable y 1 appears in atom v.
6. STOP .

INITIAL-~~p has been completely described . At this point we have sufficient machinery t o generate a mapping between the predicates and variables that appear in the statements of theorem pairs such as T 1 - T 2 and T 3 - T 4 . Next we want to extend this mapping to include all the predi­ cates that appeared in the proof of the proved theorem T and are likely to appear in the proof of the new theorem TA. In addition, we would like to pick up a small set of axioms adequate for proving TA. EXTENDER performs both functions

A DETAILED DESCRIPTION OF EXTENDER

In the last section I described IJiiiTIAL-~~P in substantial detail. In comparison, EXTENDER is a far more complex and subtle system which I will explicate here less completely . I intend to accomplish several simple aims with this limited exposition:

1. Expose the reader to the motivation and rationale underlying the EXTENDER design .
2. Convey some appreciation for the flavor of some well-specified computational al­ gorithms for creating an analogy .
3. Provide an intelligible, self-contained , introductory account or EXTE~~ER adequa te for the general reader, and motivate the more sophisticated specialist to consult
4. a more complete exposit ion . ( 6)

The rationale of EXTENDER depends upon a few simple related ideas. I will begin by explicating these, then develop MAPDESCR--the clause descrip­ tion mapping operation--and conclude with a dis­ cussion of two simple versions of EXTENDER.

In the last section I suggested that our com­ plete analogy could be seen as the last map un in a series uj of increasingly more complete analogies. Although we may be developing several such series in parallel, they all begin with the same u 1 --the analogy produced by INITIAL-MAP. Each uj maps some subset of the predicates that appear in the proof of theorem T. Each distinct subset will, in general, lead to a different par­ tition of AXSET into (ALL, SO.IE, NONE}. When we search for the analog of an axiom (clause), we will look for some clause that satisfies the analog of its description under the current analogy. Each clause has a unique description, descr[c], which has been introduced in a previous section. We will denote the analog of descr[c] by some analogy G . as G . [descr[c)]. G [descr[c)] J J J . is equal to a copy of descr[c] in which every pred1cate that appears in Gj is replaced by its analogous predicate. Predicates that are absent from GJ are left untouched. For example, suppose

we have a trivial G 1 :

G 1 : abelian~ commutativering c 7 : -, abelian[x; *] '1 group[,-. ·J d 7 : neg[abelian] ,pos[group]. = descr[c 7 ] G (d) =neg commutativering],pos[group]. 1 7

Suppose we are seeking to extend Gl by finding the analog of c7 . It is quite unlikely that we wall find a clause that satisf1es this descrip­ tion , (Gl[d 7 ]), since it would be derived from some (rare) theorem that relates a condition on commutat1ve r1ngs to a group structure. In any event, it would not be an ana log of c 7 . If we sought all the clauses that satisf1ed neg[commu­ tatlverlng], we would be sure to include c 8 and c 9 , wh1ch at least include c 8 , the clause we de s 1re,

c : -, commutativerlng[x; ·; ~ 1 V r1ng[x; *; +] 8 c 9 : · commutativering[x; ·; '-] V commutative[*;x)

Thus, sometimes we want to search for clauses that satisfy descript1ons w1th features, e.g., neg[commutativerlng], that conta1n only predicates that appear on a particular analogy GJ. ~ow, what we are do1ng 1s a four-step process :

• ( 1) ~lake a descnpt 1on d for an ax 1om
• clause c, descr[c] .
• Create an analog description GJ[descr[c]] for the current analogy , G .
• J
• Delete from uj[descr[c]] any feature that contains a predicate that does not appear in uj. Denote this restriction of uj[descr(c)] to uj by uj[descr(c)].
• Search the data base for clauses that satisfy uj[descr(c)].

In our example, u 1 [descr[c 7 JJ = u 1 [d 7 J = neg(COIIIIIIutativering). U.(descr(c)) is a "restricJ tion of the analog of the description of c to ana logy u~." Since this phrase is quite cumber­ some, we will simply call it a "restricted descrip­ tion" and implicitly understand its dependence on a~.

At different times EXTENDER may seek clauses that satisfy a complete analogous description uj[descr] or just a restricted one Gj[descr]. In summary, EXTENDER relies upon four key notions:

1. An ordered sequence of partial analogies
2. Gj·
3. A partition of the axioms used in proof [T] (AXSET) into three disjoint sets: ALL, SOME, and NONE .
4. A search for clauses that satisfy the analogs of the description of the clauses
5. in proof[T).
6. A restriction of our descriptions rela­ tive to an analogy GJ by including only those features with predicates that ap­ pear in GJ.

INITIAL-MAP used an operation called ATOMMATCH in a rather clever way to extend its current analogy. Likewise, EXTE~ER uses an operation called MAPDESCR for a similar purpose. Both operations use abstract descriptions in order to associate their data: ATCMMATCH uses the se­ mantic template associated with a predicate, and ~~PDESCR uses the description of the clauses it is associating. EXTENDER and INITIAL-MAP differ in that EXTE~ER generates a new partial analogy each time it activates ~~PDESCR (and the resultant mapping is new) while INITIAL-MAP uses ATOMIIIATCH to expand one growing analogy .

Each partial analogy GJ is derived from its antecedent Gj-l by adding

1. An association of one clause axk ' SCJ.IE with one or more clauses from the data base.
2. An associat1on of the predicates in
3. those clauses.

A simple example will illustrate th1s amply. If G 1 is the initial analogy generated by INITIAL­ MAP applied to the pa1r of theorems T 1 -T 2 , its pred1cate map is to G 2 .

!'ow, we can write a version of MAPDESCR which accepts as arguments two clause descriptions and an analogy G : J

mapdescr[descr 1 ;descr 2 ;Gj] : =

1. Vx x t desc r s . t. G [x] C descr 2 , 1 j delete x from descr and G. [x] from 1 J descr 2 . Thus , we exclude all those features we know a bout from G . . J
2. Vx x c descr 1 and x C descr 2 , map the predicate that appears in x into itself and delete x from descr 1 and descr 2 .

(3) In the remnants of descr 1 and descr 2 :

• (a) If there are unique elements of descr 1 and descr 2 that have the same feature, e.g . , pos, and se­ manticall y compatible predicates, associate those terms and delete them from the remnant descriptions. Here "semantic compatibility" means "same semantic type."

abelian "conunutativering

intersection u intersection .

Suppose we know th::tt c 7 ·· c 8 . We would like to extend G 1 to G 2 by adding :

To motivate the struc ture of MAPDESCR, let us design a version of it that would enable us to extend G 1 to G 2 in this example. MAPDESCR is charged with mapping neg[abelian) , pos[group) (d 7 ) with neg [conunutativering) , pos[ring), when it knows that :

First , we can el1minate neg[abelian) from d 7 and neg[commutativering) from d 8 on the basis of G 1 , which associates "abelian '' and "commutativering ."

G 1 [neg[abelian)) = neg[commutativering]). Now we are simply left with associating pos[group] and pos[ring) . Since these are the only two elements left , have the same semantic type (STRUC~RE), and have the same feature (pos), we can map them by default and add

• (b) If more than one element of de s c r 1 and desc r 2 have the same fea ture, e . g. , pos , then discrimina te within these elements on the basis of the semantic types of their predicates .
• Return the resultant list of paired predicates .

Most often in my algebra data base a clause de­ scription consists of two, three, or four features. EXTENDER ensures that some of the predicates in any pair of clauses passed on to MAPDESCR are on Gj. Thus, by the time we reach step 3 of the MAPDESCR algorithm we often have descriptions of length one, which map trivially by default, or descriptions of length two with different features , e . g., pos and neg. Thus , step 3b, which requires disambi guation based upon predicate t ype s , occurs rarely in this domain (abstract algebra ) .

When MAPDESCR returns a list of predica tes pairs that result from mapping the de sc ription of a clause c 1 (descr 1 , above) with the description of a clause c 2 (descr 2 , above) according to anal ogy Gj' it creates ;-;;;-ana logy Gj +l ' Gj+l is the same as Gj except that

1. Its predicate map is the union of the one returned by MAPDESCR and the one appearing on G j .
2. Its clause mapping is the union of t he
3. one appearing on Gj and c 1 - c 2 .

Thus, when EXTENDER is attempting to ext end Gj, it creates a new analogy G.+l' G . 12 , etc . f or each clause pair it maps when those ~ auses we r e ;;i;cted on the basis of information in Gj . Of course, there is a procedure to see whether the predicate associations of a new analogy have ap­ peared in some previously generated analogy and thus prevent the creation of redundant analogies. In this case the two corresponding clauses are added to each existing analogy for which the predicate pairs returned by MAPDESCR are a subset

of its clause map .

After I explicate one additional idea I can describe a simple version of EXTENDER. When EXTENDER is extending Gj it is searching the large data base for some clause that is the analog of an axiom ck C SOME . Now we could search for the set of clauses that satisfy Gj[descr[ck)), but we will run into the difficulty described earlier in this section. Thus, we search for clauses that satisfy Gj[descr[ck]]. If �~ con­ tains the correct analog for each predicate that appears on it, then the set of clauses C that satisfy Gj[descr[ck)] is guaranteed to contain the desired analog of ck ("image" of ck) . We

R. E . KLI:'\G

wlll refer to C as the '"candid::tte image set. Suppose that C has know t ha t c is the should extend � . ~ J I but one member, c . analog (image) of ck G ~l by associ::tting J . ck I .. c Then and \ \.'C

When the set of clauses that satisfies a restricted description contains only one, we are guaranteed that it is the image clause we seek if Gj does not contain any erroneous associations. :'\ow, if C is empty, we have reason to suspect the correctness of GP and we ought to stop deJ veloping this tranch of the analogy search space. On the other hand, if C has more than one member, and GP is correct, we know that our des1red image is ln C. If we have a clause c with description descr[c) and some analogy Gj that contains only one of the predicates in c, then GJ[descr[c]] will have but one feature and many clauses will satisfy it. If some later analogy~ (Gj ~ �~) includes another predicate from c in addition to the one on GJ' then Ck[descr[c]) will have two features and will be satisfied by fewer clauses than G.j[descr[c)]. Thus, as sequence of analogies evolve, each clause will have decreas1ngly fewer candidate images that sat1sfy 1ts restr1cted description.

To search for the clauses that satisfy the ana log of a restricted (short) descript1on, EXTE:>.llER, invokes an opera tor shortdescr[G . ) . J SHORTDESCR is dependent on G.j in three ways :

1. It searches for the analogs of clauses that appear on SOME ("·hich is different for each GJ).
2. It generates descriptions that include only the predicates that appear expll­ citly in Gj.
3. ( 3) It uses the predicate map G . j

SHORTDESCR returns a (possibly empty) list of ax1oms (from SOME), each of which is paired with a set of clauses from the data base which satisfy the analog of its restricted description . Each ax1om is guaranteed to have its analog under Gj in its associated "candidate image set . " If we find no candidates at all , for any axk £ S~~, then we know that GJ contains some wrong predi­ cate associations, and we ought to mark it as ''infertile'' and discontinue attempting to extend 1t . Of the images we find , we prefer those axiom-ca ndidate assoc1ations with but one candidate image. If we apply MAPDESCR to each such pair, we can be sure that we have a consistent extension of Gj. Let us consider a primitive vers1on of EXTE~llER , EXTE~llERl, which exploits these few 1deas .

EXTEl\lll [G. ; AX LIST): = 1

• (l) Let analist = (G 1 ), the set of active an::tlo~,:ies .
• If G. is complete, STOP .
• Partition AXLIST into ( ALL,SOME,:'\OS!::} relative to G. .
• Set imlist to. 1 shortdescr[G ) . If --- J ~ = ~~ mark G.J as UARREN and go to 7 .
• Set unimages to the subset of imlist that has only one candidate analog for each axiom. If unimages = 0, go to 7.
• Apply MAPDESCR to each axiom and its analog that appears on unimages . If MAPDESCR adds a new analogy, add it to the end of analist.
• If analist 1s empty, STOP. Otherwise, set G. 1 to the next element on anal1st. Go to 2.

The success of EXTE:>.lll is highly dependent upon the clauses in the data base . If there are few clauses then it is likely that some axk t S~!E will have but one image under SHORTDESCR at each iteration and that EXTESDl w1ll be successful. As the data base increases in size with ever more clauses involving predicates that will appear in proof[TA], then it becomes more likely for SHORTDESCR to ~enerate several irna£es for every axk c S~~ in some iteration. At this point it w1ll fail to EXTE~ll G . and miss the analogy alJ together. To remedy this situation, we need a way for dealing with cases when SHORTDESCR returns several candidate images for each axk c SOME. ll'e need some way to select the clause from the can­ didate set that 1s most likely to be the analog we seek . When EXTENDER meets a situation of this sort, it orders all the images according to their likelihood of being analogous to the axk c AXSET with which they are paired. I will initiate the description of one such ordering relation by a simple example .

Consider, for example, the clause c 10 and an analogy G 2 that includes

d 12

R. E. KLING

We can compare cl 1 and c 12 by comparing d 11 and d12 with d 10 (re ative to G2 ) . We want a partial ordering of a set of descriptions relative to a target description and a particular analogy, e.g . , a ~d£d 1 ; d 2 ;d ; �j], that orders description d 1 with respect to d 2 . A simple ~d can be developed as follows :

I I For d 1 and d 2 compute the number of features , e.g . , pos, in common with d 1 · The description

with the most features in common is closest to d.

In our example , we have

Clearly d 1 lS closer to d 1 than d 1 , so we 12 lO and c 11 as the select d 12 our closest descr1pt1on image of c under G . After MAPDESCR m~~s c ~ C l¥ will ad~ : 10 12

A more sophisticated ~d can look at the semantic types of predicate that share common features if two descriptions are equivalent und~r th~ simpl e ~d describ~d above. EXTENDER uses an op~rator called Ml'LTIMAP to select the best image (using ~d) for a clause that has several candidates images vd th a restricted description und~r G . . J Exploiting this notion , we can write a more

powerful EXTEKDER called EXTEND2.

EXTE~~2 [G 1 ; AXSET): =

1. Let analist = <G 1 ... Gj), the list of active analogies . Start with analist = (ul) .
2. If Gj is complete, STOP.
3. Partition AXSET into (ALL, SOME , !'\ONE) relative to G j .
4. Set imlist to shortdescr[G ) . If imlist = 0, m3rk Gj as "inlertile" and go to 8 .
5. s~t unimages to the subset of ~ that has only one cand1dat~ analog for each axiom . If un1mages = 0, go to 7 .
6. Apply MAPDESCR to each axiom and its analog that appears on unimages . If MAPDESCR adds a new analogy, add it to the end of analist. Go to 8 .
7. Apply NULTIMAP to ~ to select an optimal candidate image under ~d for each axiom. Set unimages to this list of axioms paired with best candidates . Go to 6 .
8. If analist is empty, STOP. Otherwise, set Gj to the next element on analist. Go to 2 .

This version of EXTENDER is quite powerful and will handle a wide variety of theorem pairs . The reader who is interested in the behavior of EXTENDER in generating the sequency Gj is referred to a more detailed report (6) for case studies and further explication . The implemented versions ot EXTE~~ER are far more complex than these simpli­ fied tutorial versions . They (1) allow backup, (2) have operations for c·ombining a set of partial analogies into a "larger" analogy consistent with all of them, (3) have a sophisticated evaluation for deciding which particular axiom-candidate set to pass to MULTIMAP (in lieu of step 7 above) , and (4) can often localize which predicate associa­ tions are contributin~ to an infertile analogy when one is generated. Table 28 contains a bri e f summary of ZORBA-I's behavior when it is applied to five T-TA pairs drawn from abstract algebra . The number of partial analogies generated in­

cludes G 1 generated by INITIAL-MAP.

Table 2A

TiiEORD!S REFERENCED IK TABLE 28

• Tl. The intersection of two a~llan groups is an abelian group .
• T2 . Th~ intersection of two commutat 1ve rings is a cummutative ring .
• T3 . A factor group G/ H is simple iff H 1s a maximal normal subgroup of G.
• T4. A quoti~nt ring A/C is simpl~ if.f C is a maximal ideal in A.
• T5 . The intersection of two normal groups 15 a normal group .
• T6 . Th~ 1ntersections of two id~als is an idea 1.
• T7 . The homomorph1 c imag~ of a subgroup 15 a subgroup .
• Til. Th~ homomorphH' imag~ of a subring 1s a subring .
• T9 . Th~ homomorplllc illl8gc of an abelian group is an abcl1an group .
• TlO . The homomorph1c 1m:1gc oJ a commut a ti ve r1ng 1s a commut :~t 1vc r1ng .

> ... u "C ll.

"" u i 0 ~ "" ll. .... I ..: l:l 0 N ... 0 a: j <I)

., ... Cll "C ..... ~ II Ill I .... ., ~ ... ~ f 0 ..... Ill 0 CIS r:: N ... ~ ~ .8 ,t:J	Ill	1'-	Ill	N	"'
"C I r:: ... ;:1 0 0 ... ... .8 ., Ill § ., ;:1 :z: CIS .... u	Ill .....	1'- .....	.., N	1'-	"' .....
... r:: 0 .... !-< ... ., .8 5 ... 0 § ·~ 0 ... :z: < ll. .,	.., .....	M	.... N	"'	N ....
.... Ill >. 0 ... ,t:J CIS ... u "C ll. .8 ... 8.;i "C ~ Ill Q.l ... "' :z: ll. :IE	M	Ill	..,	...	N
"' I! ... Ill Ill 0 ., ... "' 0 ... u Ill .8 ~ .:: !-< § ~ c :z: Cl. ...	"'	N ....	00	Ill	1'-
* ... ... "' ll. I! Ill ... 0 Ill .s: E-o	N !-< ..... ,..	... !-< .., !-<	"' !-< Ill !-<	00 !-< ('- !-<	0 .... !-< I!!

ai bl) .. c. bl) r:: .... "C Ill u Ill ... c. Ill .:: ... r:: 0 < N Ill ..... .c r. c . ... ... "' Ill Q. Q. "' "' ... c Ill I! Ill ., "' ... "' I! u ... 0 Ill .:: *'"'

NECESSARY CONDITIONS FOR AN ANALOGY

ZORBA-I has three necessary conditions for creating an analogy. The first, created by the form of ATOMMATCH, pertains to the form of the statements of T and TA.

Notice that we do not insist that predicates map one-one. Consider an INITIAL-MAP between

Tl : The intersection of two abelian groups is an abelian group

and

R. E. KLING

ATCNMATCH can map

at different times and handle many-one predicate maps. However, the EXTENDER would need to know (and it does not yet) how to handle this ambiguous information.

The second restriction is created by the ex­ tension of the analogy by finding image clauses that satisfy the incrementally improved analogy . To state this condition on the image clauses in a formal way, I need to introduce some simple termi­ nology. Let us say that a clause c bridges a set of predicates P 1 to another set of predicates P 2 iff:

and (redundantly)

Now consider two clauses, c 1 and c 2 . W~ w~ll say that c 1 and c 2 bridge f~om P 1 to P 2 if ~ P an~ c 1 bridges fro~ P 1 to P and c 2 bridges from P to P 2 . P 1 C P C P 2 . In general, we will say that an unordered set C of k clauses bridges from P1 to P2 iff 3 P~, P~ P~-l

such that:

Now let:

preds[T] = predicates used in proof of T. Pr[T] = predicates used in statement of T.

descr[c] = description of clause c.

u(descr[c]] = analog description of the description of c under G.

AXSET = axioms used in proof of T.

TS: The intersection of an abelian group and a commutative ring is an abelian group.

R. E. KLING

1. A necessary condition for the EXTE~~ER to work is that:
2. (a) 3 c C AXSET and c bridges Pr(T) to preds [T).
3. (b) and if G[c) = (c", c" satisfies G[descr[c']] for some c' e c G[c) bridges from Pr[T) to preds[T ). A A

More verbally, some subset of the axioms in the proof of T that bridge R the domain of INITIAL-MAP to preds[TA) has a set of image clauses under G that bridge the images of INITIAL-MAP to preds[TA). Thus, the proofs need not be isomorphic, merely that some subset of the axioms have a nearly isomorphic set of image axioms, similarly restricted to the bridging condition.

This bridging condition may seem rather non­ intuitive from the vantage point of choosing a data base, but it should be clear that EXTENDER imposes this condition.

To develop analogies in domains that are de­ scribed by predicate calculus with constants would require wholly different analysis algorithms. Consider a robot that is instructed to go from SRI to (1) an office on its floor, (2) Stanford University, (3) San Francisco, (4) New York City, (5) Chicago. These five problems could be stated to QA3 as

By trivial syntactic matching we could as sociate officeS with Chicago, Stanford with San Francisco, etc. The robot's actions to get from SRI to Stanford or San Francisco, New York City, or Chicago are pairwise similar. But the INITIAL-MAP or extender would have to know the "semantics" of these (geographic) constants (with respect to SRI) and the robot's actions to assess which problems are adequately analogical and which action rules should be extrapolated to

the unsolved problem.

RELATIONSHIP BE'IWEEN ZORBA-I AND QA3

In the preceding section, I have discussed the organization and use of ZORBA-1 independently of QA3. In this section, I merely want to note how change in QA3 can affect the way in which the analogical information output by ZORBA-1 can be

used.

The present version of ZORBA-1 outputs a set of clauses that it proposes as a restricted data base for proving TA. If every clause in proof[T) has at least one image clause, then simply modi­ fying the QA3 data base is magnificently helpful. However, if the analogy is weak and we have only a partial set of images, what can we do? If every predicate used in the proof[T) has an image, we could restrict our data base to just those clauses containing the image predicates. Could we do better? And what do we do with a partial ·analogy in which some clauses and some predicates have images, but not all of either? At this point we meet limitations imposed by the design of QA3. All contemporary theorem provers, including QA3, use a fairly homogeneous data base. QA3 does give preference to short clauses, since it is built around the unit-preference strategy. But it has no way of focusing primary attention upon a select subset of axioms A*, and attending to the re­ maining axioms in D - A* only when the search is not progressing well. Orie can contrive various devices, such as making the clauses in A* "pseudo­ units" that would be attended to early. Or, with torch and sword, one could restructure QA3 around a "graded memory." (7) Basically we have to face the fact that our contemporary strategies for theorem proving are designed to be as optimal as possible in the absence of a priori problem­ dependent information. And these optimal strate­ gies are difficult to reform to wisely exploit a priori hints and guides that are problem dependent . This is not to say that various kinds of a priori information cannot be added. Rather, it is a separate and sizable research task to decide how to do it. I presume, but do not know, that these comments extrapolate to other problem-solving pro­ cedures, and a system that is organized around a. priori hints, heretofore user supplied, may look very different than one which is designed to do its best on its own. QA3 was chosen because it was available and saved years of work developing a (new) suitable theorem prover. However, further research in AR may well benefit from relating to a more flexible theorem-proving system.

WHAT'S NEW?

What does ZORBA add to our understanding of AR? What does ZORBA leave unanswered? Pre-ZORBA, most researchers believed that analogies would some sort of semantic information. ZORBA adds the

relate to plans and (possibly to probably) include following insights to our understanding of AR :

1. Some fairly interesting AR can be handled by modifying the environment in which a problem solver operates rather than forcing the use of a sequential planning
2. language .

R. E. KLING

1. Each problem solver/theorem prover will use different a priori information and consequently will require different analogy-generation programs.
2. A good analogy generator will output some information helpful to speeding up a problem search as a byproduct of a successfully generated analogy.
3. Part of the problem of AR is to specify precisely how the derived analogical in­ formation is to be used by the problem solver.
4. An effective, nontrivial analogy genera­ tor can be adequately built that uses a simple theory and primitive semantic selection rules.
5. Although analogies are nonformal and are semantically oriented, nontrivial analo­ gies can be handled by a special system wrapped around a highly· formal theorem prover.

In contrast, ZORBA neglects:

1. Methods for handling those analogies that absolutely require a planning level generalization and sequential informa­ tion.
2. Very weak analogies.
3. ( 3) V.'ha t to do with many rules of inference.
4. How to descrtbe the "structure of an analogy."

ZORBA makes a substantial contribution to our pale understanding of AR, and in the process helps articulate additional questions that reveal our vast ignorance of analogical ways of knowing.

REFERE.NCES

1. ~ . J. Nilsson, Problem Solving Methods in Artificial Intelligence (McGraw-Hill, to be publtshed 1971).
2. 2 . G. W. Ernst and A. Newell, "some Issues of Representation in a General Problem Solver," AFIPS Conference Proceedings, Vol . 30 (1967), pp. 583-600 .
3. 3 . R. E. Fikes, "REF-ARF: A System for Solving Prob.lems Stated as Procedures," Artificial Intelligence, Vol. 1, pp. 27-120 (1970).
4. 4 . R. E. Kling, "An Information Processing Ap­ proach to Reasoning by Analogy," Artificial Intelligence Group TNlO, Stanford Research Institute, Menlo Park, California (June 1969) .
5. C. Green, "Theorem Proving by Resolution as a Basis for Question Answering Systems," in Machine Intelligence, Vol. 4, D. Michie and B. Meltzer, eds. (Edinburgh Univ. Press, Edinburgh, Scotland, 1969).
6. R. E. Kling, "Reasoning by Analogy with Ap­ plications to Heuristic Problem Solving: A Case Study," Stanford University Ph.D. Thesis forthcoming.
7. R. E. Kling, "Design Implications of Theorem Proving Strategies," Al Group Technical Note 44, Stanford Research Institute, Menlo Park, California (1970).