Tuning of Search of the Problem Space for Geometry Proofs

Introduction

I have been involved in research <Anderson, Greeno, Kline, & Neves, 1981 ; Neves & Anderson, 1981) to characterize the organization of various proof skills possessed by high school students in geometry and to identify bow these proof skills are acquired. In this paper I will concentrate on the skill involved 111 planning a proof to a geometry problem and, in particular, how the search for such a plan improves with practice. The direct goal in this research is to provide an accurate psychological model of bow h1gh school students learn to do geometry problems by doing geometry problems. A perhaps­ not -mcidental by-product is a set of ideas for bow learning mechamsms might be used to guide problem-solving. All this research IS done m the context of a general producllon system SimulatiOn of human cognition called ACT.

TUNING OF SEARCH OF THE PROBLEM SPACE FOR GEOMETRY PROOFS

John R. Anderson Department of Psychology Carne1pe-Mellon University Pittsburgh. Pa. 15213

Organization of the Task and the Skill

The plannmg process we are trying to model is bow students find a sequence of legal deductions that allow them to derive a to-be-proven statement from the givens. Figure I illustrates a triangle congruence problem which is simple but nonetheless is challenging for the just beginning student. It is taken from the textbook we have been studying <Jurgensen, Donnelly. Maier. & Rising, 197 5 >. Figure 2 illustrates the attempt of one of our subJects to solve this problem. First he tried to use the SSS method wh·ch worked on the previous problem. However. be noted that there seemed no way to get 'lrr ':" RK and turned to Side-angle-side. He immediately saw :!! -:' Ks would provide one side and RS ':" JB another side. He bad a little difficulty seeing the included angle. His protocol at the critical point (after identifying the two congruent segments) reads "But where would LI and L2 are right angles come in ... Ob, I see bow they work." This evidence, consistent with the rest of the protocol, shows that be did not see that right angles implied angle congruence until be needed angle congruence for the SAS postulate. At this point his plan was complete. He bad some difficulty converting lt into a legal two column proof (e.g., remembering that the reason that justified m; ~ Its was called the "reflexive property of congruence") but there was no more planning in his protocol.

Figure 2 illustrates in stmple form the backward search that IS typical of novices in geometry and other domains (Larkin, McDermott, S1mon, &: Simon. I 980). Our simulation program plans m part by generating such a planning tree. In this tree there are disjunctions of methods to accomplish a goal (e.g., either SSS or SAS to prove triangle congruence) and each method can break down into a conJUnction of subgoals (i.e.. two sides and an included angle). Novices and our simulation <with a novice knowledge base) tend to search such a proof tree m a depth-first manner.

In more expenenced students one sees forward inference from the givens. For instance, in problem I a student with some experience would likely recognize that L I and L2 are congruent before be bad consciously chosen the side-angle-side method. Potentially, geometry problems could be solved by pure forward search. but many potential forward inferences (e.g., those authorized by the reflexive rule) would be wasted. Optimal performance will anse from a mtxture of forward and backward search. Ftgure 3 gtves a problem that no cel y illustrates the trade-off between forward and backward search. The maJortty of the subjects we have looked at m solvm~ lhts problem <all at some intermediate level of skill l ftrsl reasoned forward to the mference that ~ AMC ~ ..£l BMD without knowmg how they would use the fact. Then they worked backward to a proof plan that mvolved thts forward mference. Our stmulatton at one setting did the same (see Anderson et al., 1981 for details) .

Figure 3

It has been documented 111 other domams such as physocs (Larkm. McDermott. Stmon, & Simon, 19801 that the proportoon of backward search decreases and the proporllon of forward search mcreases with experllse. In our stmulallon the amount of forward inference depends on the extstence of productton rules that will make the forward mferences. on their strength. and whether various tests on thetr applicability are mel. It is lyptcal of our simulatmn that it will generate some set of forward inferences and then settle mto a backward reasoniDf: mode to complete the proof plan. This also seems lyptcal of students who frequently starts off markmg some set of forward inferences on the diagram. Forward inferences lend to precede backward inferences in our simulatiOn because they requtre less coordinatton and can therefore be more qutckly executed.

It is clear that either in forward or backward inference mode, there IS a serious search problem for students. In forward inference mode one wants to only make those inferences that will play an essential role in the final proof. In backward inference mode one wants to pursue only those methods that lead to success. Neither our students nor the Slmulallon are always successful m thetr search. However. tl seems clear that one dtmenston of experllse IS the ability to make more JUdiCIOUS decisions about the paths to search. The mam focus of this paper ts how that expertise IS gamed. <If the reader would like a problem likely to create the experoeuce of search for his level of experllse. I suggest he constder solvmg the problem in Ftgure 4. )

The central !bests of our work on geometry is that there are certam features of a problem that are predicttve of the success of a parllcular inference path and that the student learns the correlations <through proving problems). Some correlaltons between problem features and mference rules are logocally determmed. So, for mstance, a student will learn that if he ts trytnf to prove two tnangles con~ruent and they both tnVCllve rogbt angles. 11 ts likely that he should try a rtght anf:lc postulate. Other correlations between problem features and inference rules reflect more about biases m problem construction than any logical necessity. So. for mstance. a student learns that if be sees a triangle that looks as 1f 11 is isosceles, it is likely that be will want to prove that tl tS isosceles. Whatever the reason for the correlation between features and inference methods, the student can use these feature-method correlallons as heuristics lCl ~uide search. An tmportanl task for our tunmg mechanisms ts IC1 discover and exploit these corrclatlllns. It IS clear that students hecomc more JUdiCIOUS m chotce of proof paths because they learn more and more features that are predictove of the correct scan path.

It IS the character of heunstocs that they should not always work and that tl ts possible to create problems that wtll vmlalt· these heur1s1tcs and which woll, as a consequence, create difficulttes. Ftgure 5 Illustrates such a problem whtch occurred m the textbook we were usmg. The problem appears as an exerctse 1mmedtalely after the section that presents tht: hypotenuse-leg postulate for nght-angle triangles. The maJority of the sUbJects we have given this problem to report reasonm~ from the fact that {H and {K are complementary to the fact that {A ts a nght angle. Then they can apply the hypotenuse­ leg theorem. However. a simpler proof ex1sts by simply nolm£ the two tnangles share (!\. and then applymg the stde-angle-sldt· proof. However. subjects are led by various heurisllcs such as < I) Problems tend to use the postulates mtroduced m the section: ( 2 l If right-angles are menlloned and 11 is a triangle congruence problem, use a right -angle postulate; ( 3 l Use all the givens 111 a problem. Students are generally not mstructed as to such heunsllcs; they have picked them up by example.

I wtll dtscUS$ SIX methods for usmg the expenence of past problems to tmprove search on current problems. We have worked on each method in our computer simulatiOn and have reason lor beltevmg that each is found in high school students. The f1rst . analogy to prior problems. is somewhat distinct from the rest and will therefore be treated separately. The other f1ve are pnnctples concerned with extracllng general and reliable rules from examples. They are the prmctples of rule evalualton. generalization, discrimination. composition. and forward mference formation. These last five make critical use of the produchon system architecture in which the Slmulahon ts unpleruented. The first. analogy. does nul.

Analogy

Desp1lc the fact that lis rok IS somewhat smgular m our theory. our protocols are rich 111 evidence of successful problcm-solvmg by analogy and many more less than successful allempts to use analogy. In the theory. analogy mvolves two processe~. Fust. there is the noticmg of the Similarlly between tbe specifications of a current problem and the specificatiOns of a previous problem. Second, an attempt is made to map the sol utiOn of the previous similar problem to the current problem. The f1rst process m our protocol IS sufficiently rapid that 11 cannot be decomposed mto substeps. A student will typ1cally s1mply announce after readmg the problem--"Ttus IS Similar to Problem X... We have not beeu able to idenhfy any mstances where this Problem X occurred any earlier than m the prev1ous day·s lesson. So. there appears to be important memory llmitallons to the range of s1milanty not1cmg m analogy. process.

We have Implemented a partial graph matchmg process to model th1s Slmilarlly noticmg. Th1s parhal matchmg process IS also used 111 our work on generalizatiOn. The bas1c 1dea IS an allempt to Identify subgraphs on wh1ch the problems overlap. An early version of ttus IS described m Anderson. Klme. and Beasley ( 1979. 1980 ~ and a more advanced vemon by Kline <19M ll. The 1deas are vanatwns on techniques suggested by Hayes- Roth and McDermoll ( 1'176~ and Vere ( 1977 !.

Such a smularity ddect10n mechamsm IS very much mflucnc"d by how the problems are represented. Consider hgurt· t>. In terms of many features such as shape and onentatwn. problems (al and (cl are more Similar than tal and <hi. However. II turns out that the more profitable s1milanties ex 1st between (a) and (b). Many of the unsuccessful attempts to use· analogy in our protocols cal) be accounted for by subJects being distracted by such superficial Similarities.

In contrast to the rap1d similanty-detectiOn. the efforts to map a proof from one problem to another are quite Ion!! and defmllely aJ\alyzable into substeps. It seems that the student ha!- transformed h1s 101l1al problem space mto a new problem space of fmdmg the mappmg. We have not m our s1mulatwn work modelled ttus mapping process systematically. F1gure 7 Illustrates one ·of the more striking examples of failure of the mappmg. The student noted the similarlly between the two problems and proceeded to copy the proof to one problem over to the other. The fnst line for part <a) read RO = NY so analogously he wrote AB > CD for part (b) . The second line for part (a) read ON = ON so analogously he wrote BC > BC for part < bl! His semantic sensibilities detected the problem: he abandoned the attempt to use the analogy; and proceeded to solve part (b) on its own.

While these two examples illustrate analogy by showmg how 1t can fail . it is clear that 1t succeeds more often than not. One maJor problem w1th it IS that it does not provide any permanent benefit as seen by the fact that all analogies are to pwhlems encountered m the current or previous day. It may he that formulatmg analogies causes more permanent operators to be formed. The generalization process that will be described could apply after solution by analogy although solution by analogy IS not a pre-requisite to generalization.

Rule Evaluation

The core of our simulation is a set of production rules for makmg forward and backward inferences. Below I illustrate. m mformal syntax, productions embodying the SAS rule for forward and backward inference.

Other more daborate productiOn embodiments of these rules are also possible. The s1mulat1on keeps a record of the rules 11 applied m workmg on a problem. By comparmg th1s record \nth the fmal pTl>of plan it can determme wluch chOices of proof method 111 wurkmg backwards wert· successful and wh1ch were llll~lw~cs. . A little care IS reqUITed here: Suppose a goal IS set tn prove two angles congruent by showmg IIley are correspondm~ parts of con!!rueut tnangles. Suppose all methods tncd for provmg congruent tnangles fail and the an~;le congruence 1s eventually proven by resortmg to supplementary angle postulate. The m1stake IS not in the methods attempted for provmg the tnangles congruent rather the m1stake was in settmg the subgoal of tnangle congruence. Forward mferences can be classified as successful 1f they figure in the final proof and as mistaken otherwise.

Success and error classificatiOns are used by the learning mechanisms to be described shortly, but they are also used to Simply strengthen or weaken the rules responsible for the deciSions. The mechamsms for strengthemng and weakemng a productiOn and the 1mpact of productl(ln strength on conflict resolutiOn has been described elsewhere !Anderson. Klme. & Beasley. 1979>. However. ll IS Important tn note that disastrous results will not occur if a bad rule IS formulated smce the strength evaluation mechan1sm Will separate out successful from unsuccessful rules and eventually only the former will be selected Ill conflict resolutiOn. Th1s means that we do not have to be concerned that th<.: lcarnmf mechamsms always be correct Ill the production rules they formulate.

Generalization

GeneralizatiOn attempts t0 ex tract comnH'll fcaturl's nf twn IUSlances and successfully apply the same mft'l<'ll<T mdhPd. Th1s IS done by testmf for sumlarlly hctwccn the pr·>hkm descnpt10ns before the rule of mfcrence applies. L'nns1der problems (a) and (bl of F1gure b. In both cases. the lllltlal step mvolves settmg as a subgnal to prove congruent tnanflcs that overlap with the to- be-proven- congruent tnanglcs. The representahon of the state of knowledge for problem tal at the pomt of settmg this subgoal m1ght mvolve the follow1ng clauses:

1. The goal is to prove 4::1 ABO ~A CBD
2. a ABO con tams A AEB
3. a CBD conta1ns .,.:::1 CEB
4. 0\#- 4. AE = EC
5. LBEA ~ LCEA
6. B is at top
7. A ABC contams A ABO
8. A ABC contams ~CBD
9. S1m1larly, the state of knowledge for problem ( b> when this
10. sub~oal IS set might be:
11. I . The goal IS to prove ..c:1 MQO ~ A PRN
12. .a, MQO contains A NQO
13. 4 PRN contains .AORN
14. -"'- 4. NQ = OR
15. LQNO ~ LRON
16. MP 1s a horizontal hne at the base
17. Q is at the top
18. R is at the top

These two states of knowledge can be generalized by extracting what they have m common. This generahzed s1tuat1on can be ass1gned the common action of subgoal proof of the contamed triangles by the productiOn:

and c6 XYZ contams ,d SYZ

IF the goal IS to prove a XYZ ~A uvw

and a UVW contams A TVW

and SY ~TV

and LYSZ .,_ LVTW

THEN set as a subgoal to prove CI.SYZ ':"" .c1 TVW The extrachon of such Slmilarihes IS described m Anderson. Kline, and Beasley ( 1980) and Anderson and Klme ( 1979 > and IS Similar to ideas proposed earlier by Hayes-Roth and McDermott ( 1976) and by Vere ( 1977). As noted ear her. generalization mvolves the same mechamsms used m sumlar1ty detection for analogy. The above example illustrates how 1t might be used to extract from examples the pnnc1ple of chaming the goal of provmg tnangle congruence to a subgoal of proving the tnangle congruence of overlappmg tnang les. Note that the generahzahon preserves features specif ic to the two examples that are pred1ct1ve of the method's success-­ namely. that parts of the overlapping triangles are congruent.

The evidence IS qu1te clear that subJects do ext ract from examples methods that work over a class of examples conta1nm~ the same features. The overlappmg tnangles rule above is one although 1t usually appears to be more general m that prc>blem solvers will try to cham to overlappm£ triangles whenever they contam one or tw<' rongruent pwces-- not a spcc1f1c Side and an!!le. A mPTt' !!Cn~ral pr0ducl1oll such as th1 s could der1vc from the one aho,·c hy further !!enerailzat1011 1 w1th approproak reprcs~ntat10nal assumptHmsJ .

Although students do have these general rules w1thout a doubt: it IS unclear that they emerge by the fCnerail7atlon rnechan1slm SUf!!csted ahove. As an alteruat1ve. they llllfht dcnve by a retrospective analysiS of a Slllfk problem rather than a generahzat1on between two. Our protor0l data cannot mform us on th1s 1ssue and we are toohng up In do the roght kmds of controlled e.xpenments. Wor~ on cxtractwn of oh.Ject categories <Anderson & Klme. I Q7Q; Eilo & Anderson. I flo I ) has pr<wlded !!nod cvldt·nct· for a ~enerail?.atwn process 111 that

dornam.

Discrimination

The 1111t1al rule~ that a system has cnmt· frpm more- ,n-lcss d1rect encodmp of p<>stulatcs. So. fur mstancc, the .SSS postulate can lead to a rule t>f the form

The problem w1th such productions IS that their cond1t10ns are too general and do not lead to select1v1ty of search. It IS alsP the case that the gencralllahon process itself JJJifht produce overly general pn,ductlons. Overly feneral rules can he restricted by a dlscrm11nat10n mechamsm wh1ch compares successful and unsuccessful applicahons of a production. troes to determme the features wh1ch d1stmgu1sh the successful apphcahons. and proposes new produchons denved from the old but which contam these distinguishing features 111 the1r conditions. Agam. the details of the d1scrimmat10n procedure have been described m Anderson and Klme ( 1979) , Anderson. Kline. and Beasley ( 1980) and I will Simply describe here then appilcahon to the geometry domain.

Cons1der the representation m Figure 2 of the student's plannmg for the problem m F1gure I. After completmg th1s problem the learnmg program would Identify the attempt to use SSS as a n11stake and SAS as the correct method. Companng th1s slluatwn tP th<" prcv1ous problem that was successfully solved by SS.S. the pro!!ram would note that this problt:m d1ffers only 111 the fad that Tlfht angles are mentioned. Thus.

1t could propose the followmf doscrin11nahon:

PI: lr th<.: !!oal os to prove .a XYZ = ~ UVW

and .A XYZ contams no nght angles

and A UVW contams no_!.ig~ ,!!!fles ,_ _

THEN set as suhfoals to J!!OVe XY = UV. Vz = \'W. and ZX ~ WU

The doscrmunatlllf clauses are found hy locatlnf add1t1onal clauses m the data hase that constram the vanables. The above d1scnmmat10n os probahly too spec1fic and should not be l1m1tcd only to roght angles. Through generahzat1on w1th other productiOns that d<· not involve rlfht angles. the !!(I Ub.!!J '!!l.fk requirement C<>Uld be replaced hy the reqUirement that no anfles be mentiOned.

It 1s also poss1ble to form a d1scrm11nat10n of a different varoety by embelilshmg the SAS rule to encode what 1s d1stmct1vc about the current Situation. Th1s can lead to a production of the follnwmg sort:

P2:

It- the foa l IS to prove .0 XYZ ~ ~ U\'W and A XYZ contams a nght angle triangle /X\'Z and A U\'W contams a r.!§h.!._ang..!,s Ula!!£le /U\'W THEN set as goals to prove 1:7 = UV. YZ = VW, and /XYZ 7 LUVW

Th1s type o f d1scrmunatwn was not produced 111 our onpnal ACT sunul at1on hut has proven useful 111 some of our more recent. speCial purpose sunulatwns (Anderson, I 9 81 l.

As 111 the case of generalizatmn. the fact IS md1sputable that subJects form d1scnminations on their or1gmal rules. Indeed, one subject arllculated a rule essenllally Idenllcal to PI after the lustory Illustrated in F1gure 2. However. agam as m the case of generalization, what IS unclear IS whether these d1scnmmatmns are achieved by the mechamsms descnbed here. Agam, that issue awaits more detailed expenmental research.

Composition

Neves and Anderson ( 1981 ). developmg Ideas put forth by Lewis ( 1978), applied a learning mechamsm called composihon to proof generatiOn Ill geometry. The basic 1dea behind the compos1llon mechamsm IS to package sequences of production steps mto smgle operators. A somewhat Similar idea 10 the domam of logic proofs has been advanced by Smith ( 19801 . F1gure 8 illustrates one of the problems where we applied this mechamsm. The first pass of this system over the problem was accomplished by a sequence of five producllons. The first production to apply m solving th1s problem was:

p 1: IF the goal is to prove LX ':' LU and LX IS part of Ll. XYZ and /U IS part of .A UVW

IF the ~I IS to prove Ll. X\'Z--; A UVW and~"': m

THEN the ;ubgoal IS to prow A X\'Z ~A UVW .­ Th·~ production would set as a suhgoal to prove A ABC .A DBC. At this pom! the followmg produt!Ion applied:

THEN the subgoal IS to prove Yz ~ Vw This productmn, ~lied to the situatiOn in Figure 8 set as the subgoal to prove BC ':;' BC as a step on the way to usmg SSS. At this point the following producllon .l!.£Piie<t_

P'· - ,_,_ and ZX · WU

P3:

IF the goal is to prove XY ~ XY

THEN this may be concluded hy reflexivity Th1s productiOn added BC ~ BC and allowed the followmg production to apply:

P4: IF the goal is to prove .A XYZ ~ A UVW

and~~ U\l

and Yz~ VVJ

and ZX ~ WtJ

THEN the goal may be concluded by SSS where XY · AB, UV · DB, YZ = BC. VW = BC. ZX = CA. and WU · CD. This adds the informahon that A ABC ~ ~ DBC. Fmally. the followmg productiOn applied which recognizes that the to-be-proven conclusiOn IS now established: P5: IF the goal IS to prove fX "'";;-' /U

and .::1 XYZ ~ ..6 UVW

THEN the goal may be concuded becaus~ of congruent

Tht· composillon process. operatmg on this sequence, produced a

parts of congruent tnangles sm~,:k producllon that served as a macro-operator:

1'6: IF the goal IS to prove LA~ LD

and LA IS part of ..6 ABC

and LQ 'J.. ~t of .0 DBC

and AB = DB

and 1;A ';"' Dc

and conclude 6 ABC ~ A DBC by SSS and conclude the goal because of congruent parts of congruent tr.angles

-""' - THEN conclude AB : AB hy refleXIVIty The vanables m th1s producllon have been named to correspond to the terms m F1gure 8 for purposes of readability. ThiS productiOn would immediately recognize the solutiOn to a problem like that in Figure 8. This compositiOn IS ach1eved basically by addmg together the cond1hons of the f1ve oTigmal productiOnS and makmg them the cond1llon of the composed productwn; adding together the actions and making these the act10n of the composed productiOn, ed1tmg out the unnecessary or redundant clauses in the composed production.

The details for the edihng of the unnecessary clauses are g1ven 111 Neves and Anderson ( 1981) but basically they mvolve (a) elimmating clauses from the conditiOnS of produchons late in the sequence which are satisfied by the actions of productions early m the sequence and ( b) eliminatmg the settmg and testing of goals which are met in the sequence. W1th respect to (b) composition serves the effect of collapsm~ several levels in the proof plan into a single level.

There is a questiOn of when to evoke compos1t10n. Th~ origmal 1mplementallon by Neves and Anderson was to use compositiOn on any immediately cont1guous sequence of producllons. However , I thmk it more reasonable to have 1t apply to a sequence of productiOns related by mampulat10n of the same goals--as m the case JUSt illustrated. These two defuut10ns of production sequence need not yield the same sequences m the ACT system. It IS quite possible for 1mmed1ately contiguous productwns not to share s1mllar goals.

Creation of Forward Inferences

It IS a feature of the composillon production P6 that It summaTizes what bad been a mulU-Ievel goal tree. The system had started With the goal of proving two angles congruent. set a subgoal of provmg two triangles congruent. set a subgoal of proving two Sides congruent, and then proceeded to pop the goals fmally achieving the highest level goal. It would be useful to have this available as a forward inference rule so that, should the situation appear again, the inferences can be made to embellish the problem representation. This can be ach1eved by dropping the goal specification from P6 (a Similar 1dea was proposed by Larkin, 198 I I. The resulting productiOn would be:

P7: IF LA is part A ABC

and /0 IS part of 0 DBC

and CA ~Dc - -- THEN conclude AB · AB by reflexivity

and n ~~

and conclude A ABC = A DBC by SSS and conclude LA ";"- LD because of congruent

parts of .:ongruent tnangles

I I IS 1nterestmg to note that thts production makes a reflexive mference 111 forward mode. To have a pure reflexive rule as a forward mference:

IF AB THEN As ~As hy reflexivity

would be a sheer disaster since it would complicate the problem representation With many useless mferences. However. cast as part of a larger operator as above 11 IS a very profitable forward inkrence.

To review, forward inferences can be made when composillon creates a macro-operator which ach1eves a stated goal by a sequence of inferences that previously had involved the embeddmg of subgoals. The forward mference can be created from the composition by deletmg the goal clause. It IS useful to understand why one would only want to drop goal clauses from the macro-operators rather than the origmal working­ backwards productions. The original productions are so little constrained that the goal clauses provide important additional tests of applicability. After a macro-operator is composed there

Given: As and Co bisect

each other

Prove:~XC ~~BXD

Figure 9

are enough tests in the non-goal aspects of Its condition to make it quite likely that the mferences will be useful. That IS. it IS unlikely to be an accident that the conJunctiOn of tests are satisfied.

We do not have any ev1dence for P6 or P7 as specific rules--probably because the pattern in Figure 8 occurs m the textbook exercises. In contrast the pattern in or slight variants of 1t occur quite frequently m the inference but once Figure 9 chapter. followmg The problem 111 F1gure 9 can be solved by the three productions.

P8:

IF the ~I is to prove ~ XYZ = c:1 UVW and n -:- 0'\! and Vi ~ V'W

THEN set as a subgoal to prove LXYZ ~ LUVW

IF the ~is to ~ve LXYZ or LUYW

P9: and XYW and~

THEN this can be concluded by vertical angles

PIO: IF the goal is to prove a XYZ-:- 4 UVW and XY = UV. YZ = VW. and LXYZ /UVW THEN this can be concluded by SAS -

Composmg these three productions together we get:

PI I :

IF the ~I is to prove ~ XYZ ~ 6 UYW and xv~m ~Yz ";" ¥W and XYW and UYZ

THEN conclude LXYZ ~ LUYW by vertical an):les and conclude ..0 XYZ ~A UYW by SAS

Deleting the goal clause we get the followmg forward mference:

P12:

IF ~rc;._:re ..d XS ~d ~ UYW XY :_l5' and YZ = YW

and XYW and~ THEN conclude /XYZ ~ LUYW by vertical angles and ~ XYZ ~A UYW by SAS

There IS clear evidence for such a forward inferenc~ rule 111 some more advanced students. For them. the pattern 1n F1gure 9 is something that will tngger the set of inferences even when it appears embedded in a larger problem. However. we have poor evidence on what the exact ongms are of this forward mference rule.

Final Points

There are two major issues that need to be pursued. One. as noted throughout the paper. is the detailed empirical verif1cat1on of these mechanisms. The second is a suff1c1ency proof of their operation by simulating a student's course through a textbook. While we have worked up md1vidual examples of successful tuning by these learning mechanisms. we have not done the large scale Simulation to show that theu cumulative effect after hundreds of problems will match the degree of tuning we see in the typ1cal student. We intend tCl pursue th1s and I am reasonably optimistic jpven that we have achieved success with such large-scale Simulations of our learnmc mechanisms m the domain of concept formation <Anderson & Kline, 1979) and syntax acquisition <Anderson, 1981 ).