Nonmonotonic Model Inference-A Formalization of Student Modeling

1 Introduction

Student modeling is one of the most important topics of ITS research, because the behavior of an ITS largely depends on a student model, which represents the snap­ shot of student's knowledge. This is a reason why many efforts concerning student modeling have been made, for instance, overlay model, buggy model, perturbation model, etc.[Wenger, 1987]. Most of the conventional modeling methods have simple pragmatic structures and have been incorporated into many ITS's. However, all the methods have some limitations and no complete and sound inference procedure for the models is obtained yet. In this paper, we formalize a student modeling problem as an inductive inference problem, that is, a problem to construct a model explaining observed data. In our case, data are student's answers and the model is student's knowledge.

In order to make ITS's intelligent, student models have to satisfy the following requirements:

1. Accuracy-cost tradeoff: In general, the more ac­ curate the student model becomes, the more effective the behavior of the system becomes. However, there exists trade-off between accuracy of the model and cost to con­ struct it. From a pragmatic viewpoint, we must set up an appropriate representation scheme for student models

by taking the trade-off into considerations.

1. Nonmonotonicity: Tutoring is to guide students toward better understanding of teaching material. This means that the learning process is essentially attained with change of their minds and hence the consistency of student's answers can be easily lost. Therefore, stu­ dent modeling methods should be able to automatically manage the consistency of student's answers in order to follow the student's mind. However, there is very few attempts to formulate the nonmonotonicity of student modeling process[Burton, 1982][Huang et al. , 1991a].
2. Unknown assertions: When a student fails to deduce her own solution for a problem, she would say to her teacher "I could not solve the problem". Needless to say, this assertion does not mean she does not have any knowledge. The student model module should use this assertion as informative data about her knowledge and construct a model which explains why she cannot de­ duce the answer from her own knowledge. This requires student model to deduce "unknown" assertions.
3. Theoretical foundation: Domain-independent and theoretical foundation for the student modeling mecha­ nism should be defined. It contributes to both clarifica­ tion of the inherent property of student modeling prob­ lem and to articulation of the scalability and reusability of the proposed mechanism.

To meet these requirements, we have developed a stu­ dent model description language SMDL and a hypothet­ ical student model inference system HSMIS. SMDL is an extended version of Prolog and takes four truth val­ ues including "unknown" to model the student precisely. HSMIS, an extended version of Shapiro's MIS[Shapiro, 1982], is an inductive inference system for SMDL. The second requirement mentioned above suggests that the inference procedure should cope with nonmonotonic modeling process. In HSMIS, ATMS: Assumption-based Truth Maintenance System [de Kleer, 1986] is employed for this purpose. HSMIS has been implemented in Com­ mon ESP(Extended Self-contained Prolog) on SPARC station.

2 SMDL: A Student Model Description Language

In addition to the above requirements, a student model is required to represent not only students but also systerns' understanding of the students, which implies the model has to distinguish the two states: The system can predict the behavior of the student and the system can­ not. When the model is based on logic, which is our case, it has to have two truth values, true and false, which denote the above two states, respectively. Need­ less to say, the former state, that is, one corresponding to "true", should represent the student's logical state such as "true", "false", and "unknown" which stand for "the student believes a statement is true", "the student be­ lieves it is false" and "the student does not ascertain its truth", respectively. Then, we have two seemingly same truth values "false", which can be discriminated as fol­ lows: Employing Prolog terminology, the former "false" is treated as "fail" and the other as one of the three val­ ues corresponding to "success". Discrimination among the three values is done by introducing an auxiliary ar­ gument interpreted by meta-interpreter.

2.1 Overview of SMDL

Facts are represented in SMDL as follows.

temperate(paris,true). torrid(paris,false). fertile(paris,unknovn).

These three facts represent "the student believes Paris is not in the torrid zone but in the temperate zone and does not know whether it is fertile or not." If the facts are all in the student model, it also represents "the system cannot say anything about student's knowledge for other statements."

Clauses are written in the form of

A is called a head and RHS of the clause is called a body. Some simplified examples are shown below.

?- grow(paris,T).

grow(X ,T4 ) : :- temperate(X ,T1).

grow(X ,T5 ) : :- torrid(X ,T2), wet(X ,T3).

These two clauses show that the student thinks "if place X is in the temperate zone or in the torrid, wet zone then the plant grows in X". Intuitively, the clauses with the same head have a disjunctive relation and the pred­ icates in the body have a conjunctive relation. Given a goal grow(paris,T) , SMDL interpreter calls the sub­ goals temperate (paris, T1) , torrid(paris, T2) and wet (paris, T3) in this order. The truth value T of grow(paris,T) is obtained according toT= T4VT5 = T1 V(T2/\T3) = trueV(false/\unknown). Semantics of the logical operators "/\" and "V" are shown in Table 1.

2.2 Definition of SMDL

The predicate of SMDL is of the form p(X1, X2, · · ·, Xm, T), where p is a predicate name and Xi (1 ~ X ~ m) is a variable. From now on, a sequence of variables, for example x1, x2, ... 'Xm, is abbreviated as X. Tis a truth valuable or one of four truth values.

The clause of SMDL is of the form: P::-Q1, Q2, · · ·, Qm., m ;::: 0, where P, Qi (1 ~ i ~ m) are predicates. In the case of m = 0, it is called a fact. The SMDL program P is a finite set of clauses.

The execution process is defined as two different forms: Weak-derivation and strong-derivation. The former is like to the execution process of Prolog, that is, "a goal succeeds in weak-deriYation if there exists at least one clause which derives the goal". On the other hand, the strong-derivation is somewhat different and complicated. Roughly speaking, a goal with truth value T succeeds in strong-derivation, if all the OR clauses unifiable with the goal succeed and the result of OR evaluation is T. Formal definition of the execution of G with P is given below.

[Definition 1] When a goal G = p(X', T') is given and there exist the clause C = p(X, T)::-q1(X1, TI), · · ·, qk(Xk, Tk) E P and the substitution 8o such that p(X',T') = p(X,T)80 , a new goal G' = {q1(X1,T!), · · ·, qk(Xk, Tk)}8 is derived from the goal G and the clause C. When k ;::: 1, 8 = {T/(T1/\···Tk)} U 8o. This operation is called weak derivation and denoted by a triple< G',8,C >. G8o81···8z_1 is weakly-derived from P, if there exists a sequence of the weak deriva­ tion: < G, 8o, Co >< G1, 81, C1 > · · · < 4J, 8z, Cz > , whereCiEP(O~i~l-1). o

[Definition 2] For a given goal G = p(X', T'), if there exist a set of clauses S such that S = { Ci I Ci = p(Xi,T)::-qi1(Xil,Ti1),···, qin;(XinpTin;) E P p(X', T') = p(Xi, Ti)8i, 1 ~ i ~ m and the most general unifier 80 of {p(X')} U {p(Xi)l1 ~ i ~ m} then a new goal G' as shown below· is derived from G and S.

G' = {qik(Xik, T,k)ll1 ~ i ~ m, 1 ~ k ~ ni} 8, where 8 = {(Ti./ /\~;, 1 T,k)j1 ~ i ~ m} U {T'/(V~1 T,)} U 8o.

This operation is called strong derivation and denoted by a triple ¢: G, 8, S ~- G8o81 · · · 81-1 is said to be strongly-derived from P, if there exists a sequence of the strong derivation operations as shown below,: ¢: G, 8o, So~¢: G1, 81, S1 ~ · · · ¢: 4J, 8z, Sz ~. where Sic P. o

[D;ftnition 3) When a goal G = p(X', T') and a SMDL program Pare given, the result of derivation is defined as follows. ( 1) p( X', true )8 is derived from P iff it is weakly­ derived from P. (2) p(X', false)8 is derived from P iff it is strongly-derived from P. (3) p(X', unknown)8 is derived from P iff it is strongly-derived from P. ( 4) Otherwise, p(X', fail)8 is derived from P. 0

3 HSMIS

In general, an inductive inference algorithm is based on the assumption that all the observed data( oracles) are consistent. In our case, it requires that student's an­ swers are consistent. Unfortunately, however, the as­ sumption does not always hold. Students change their minds and sometimes make careless mistakes. There­ fore, a student model inference system must cope with inconsistent data. In HSMIS, ATMS is employed for this purpose. Fig. 1 shows the block diagram of HSMIS. It consists of SMIS[Ikeda et al., 1989], ATMS, Virtual ora­ cle generator( explained below) and Contradiction resolv­ ing system(CRS). The main task of ATMS is to manage consistency of a set of assumptions (environment) used by the problem solver, SMIS in our case. Virtual oracle generator is responsible for improving the performance of model inference by generating assumed student answers based on the reliability of the student without asking t.he student questions. CRS resolves the inconsistency identified by changing the environment.

Table 1: Definition of A and V.

3.1 SMtS

A pair of a problem and an answer to it is called an oracle and is used as data to be covered by the model obtained.

[Definition 4] An oracle is of the form < p(X', T), T' >, where X' is a sequence of ground terms, T is a truth variable and T' E {true, false, unknown} . 0

Because fail represents the system's understanding of student, it cannot be the truth value of an oracle. A set of oracles given to the system is called an oracle set and denoted by n.

[Definition 5] The clause C = p(X, T)::-q1(X1 , Tt), q2(X2,T2),···,qk(Xk,Tk) E P covers p(X',T'), when there exist 8 such that CO =p(X',T')::-q1 (X~,T{), q2.(X~,Tn, ... 'qk(Xk, Tn, T'= A:=1 Tf and {< p(X',T),'T' >} u {< qi(XI,Ji),Tf > 11 ~ i ~ k} c n. We call the q1(X~,T{),···,qk(Xk,TD a top-level trace of C for p(X',T'). 0

A simplified but concrete example of top-level trace is shown in Fig.2, where the oracles 0 1 , · · · , 0 6 correspond to student's answers (a) through (f), respectively. In this case, the clause C covers 0 1 , where the top-level trace is made by 02 and 03.

SMIS applies the following procedure repeatedly to the model: (1) if there is a difference between an oracle and the fact derived from the student model, activate the student model diagnosis system, SMDS, to identify the cause of the difference. (2) According to the diagnosis, SMIS selects an appropriate operation, either removal of an incorrect clause or addition of a new clause, and informs ATMS of it.

3.1.1 SMDS: Student Model Diagnosis System

SMDS traces derivation process of the current model and checks the results with oracles. SMDS has three subprocedures, such as, ip , fp and failp . The procedure ip finds out where a new clause should be added. The procedure fp detects an incorrect clause which should be removed from the model. The procedure failp dynami­ cally decides which procedure, fp or ip , should be acti­ vated. SMDS selectively activates one of them according to the difference between the oracle's truth value and the one derived from the student model.

[Definition 6] The model P is said to be weak, if there exists an oracle < p(X', T), T' > and p(X', T') is not weakly-derived from the current model P. 0

The cause of the weakness is identified by the proce­ dure ip . To cover the uncovered goal detected by ip , HSMIS searches for a new clause to add into the model.

We define -< to be the binary relation over truth val­ ues. When two clauses derive different truth values, T1 and T2 , for a goal, T1 is dominant if the relation T1 >- T2 holds.

[Definition 7] T1 >- T2 iff T1 = T1 VT2, where Tt.T2 E {true, false, unknown} and T1-::/= T2. 0

.[Definition 8] Assume that< p(X',T),T' >En and T' E {unknown, false}. The model P is said to be strong if p(X', Tg) such that Tg >- T' is weakly-derived from P. 0

A strong model has at least one incorrect clause which has a refutation as defined below.

[Definition 9] The clause C = p(X,T)::-q1(X1,Tt), ... ,qk(Xk,Tk) is said to be incorrect, if there exist < p(X',T),T' >En and{< qi(x:,Ti),Tf > 11 ~ i ~ k} c n, where T'-< A~-1Tf. p(X,T')::-q1(X{,T{), · · ·, qk(Xk, TD is called refutation for C. 0

In Fig.2, the clause C is refuted by oracles 0 4 , 0 5 and 0 6 · The incorrect clause with a refutation, which should be removed from the model as a cause of strongness, is identified by the procedure fp .

[Definition 10] The model P is said to be incomplete if< p(X',T),T' >En and p(X',fail) is derived from p 0

The procedure failp identifies the cause of the incom­ pleteness, which is either an uncovered goal or an incor­ rect clause. Because of the space limitation, detailed ex­ planation of the procedures, ip , fp and failp , is omitted.

More detailed explanation and Prolog implementation of each procedure is shown in [Ikeda et al., I992].

3.1.2 Search for a new clause

A clause to be added into the model is searched by us­ ing the refinement graph having the clause as a node according to breadth-first search. The directed arc C ..!!... C' on the refinement graph suffices the following relation.

C ..!!... C' : When the clause C' covers a goal A

· then the clause C covers A

With contraposition of this condition, the search on the refinement graph can be pruned. That is, when the clause does not cover A, branches leading to descendents of C in the graph can be pruned. A refinement operator p , which is defined by modifying that defined in MIS, produces a refined clause C' from the given clause C.

A refinement graph represents knowledge which en­ ables efficient search for a clause to be added into the model. However, it does not have any a priori knowl­ edge of bugs. So, it always tries to find out a clause from a fixed root, that is, the most general clause, indepen­ dently of materials. Note here that we can introduce the concept of bug when we know the material well. Given some typical bugs specific to the teaching material un­ der consideration, search procedure can begin searching from these bugs, which makes search very efficient.

3.2 Managing consistency of the inference process

There are two types of nonmonotonicity in our system. One is inherent to inductive model inference itself and the other is caused by inconsistency of students' behav­ ior. Both of them are formalized in a unified architecture on HSMIS by combining SMIS and ATMS. The model­ ing task performed by HSMIS is defined as follows:

[Definition 11) When an oracle set S1 is given, infer a model for n allowing the distance D(S1, n) to be mini­ mized. n satisfies the following restriction.

The distance D(S1, n) is defined as number of the oracles of n whose truth value is different from the corre­ sponding one in n .

With. the aid of schematic diagram shown in Fig. I, the overall behavior of the system will be made clear in this subsection. {I) Given student answers ("real ora­ cle"), Virtual oracle generator generates virtual oracles if necessary and pass them to ATMS with the real ora­ cles. {2) SMIS informs ATMS of all the inference process. When a contradiction is informed, ATMS computes the label responsible for the inconsistency based on the infor­ mation given up to that point and store it in the nogood record. {3) SMIS asks CRS to resolve the inconsistency. ( 4) According to the cause of inconsistency identified, CRS selects a new environment which is consistent by asking ATMS to check its consistency. (5) ATMS an­ swers the queries by inspecting the nogood record and {6) pass the control to SMIS together with a new context supported by the new consistent environment.

With regard to the contradiction caused by the incon­ sistent oracle set, CRS searches for a consistent n in the ascending order of D{S1, n ). To improve the efficiency and educational validity of selecting the consistent ora­ cle set which has the minimal distance, we incorporated some domain-independent heuristics into the search pro­ cedure: Give priority to correct answers, give priority to the oracles supporting the plausible clause, which is supported by relatively many oracles, and so on. After that, HSMIS continues inference on the new consistent environment including n . Details of HSMIS reasoning process are explained in the following subsections.

3.2.1 Description of inference process

Conditions for HSMIS to add a new clause C = p(X,T) ::-ql(Xl,Tl),· .. ,qk(Xk,Tk) to a model can be described as shown below.

if condi:

cond2:

( < p(X', T), T' >En) and

( C is correct) and

cond3: (C covers p(X',T')) and

cond4:

then

( C is the most general clause )

( add C to the model )

The conditions, i.e. condl through cond4, are de­ scribed as follows.

condl: To cope with nonmonotonicity of student's an­ swers, the oracle is dealt with as the following assumed node of ATMS.

cond2: The correctness, which means there is no refuta­ tion for C, is also dealt with as the assumption node as shown below.

cond3: The condition means that C has a correct top­ level trace for p(X', T') in f2 . HSMIS informs ATMS of its existence in the following form.

where T' = A~=1 Tf and (ql(Xl!Tl), .. ·,qk(Xk,Tk))8 is a correct top-level trace of the clause C for p(X', T').

cond4: When C is added to the model, it has to be guar­ anteed that its ancestor clause in the refinement graph, which is more general than C, does not exist in the cur­ rent model. However, an ancestor clause may be added to the model as the inference proceeds, because of the nonmonotonicity of the inference process. Therefore, the generality of C is also dealt with as the assumption.

Addition of C to the model is informed ATMS in a style as shown below.

If the environment is changed and the model( C) does not hold in the new environment, ATMS changes the status of the node from in to out .

When a refutation for a clause C identified by the SMDS, it is informed ATMS in the following form.

where p(X', T')::-ql (Xf, T{), · · ·, qk(Xk, Tk) is a refuta­ tion for C.

When it is found that C' does not cover p(X', T'), HSMIS informs ATMS of it as an assumption.

3.2.2 Controlling the modeling process

HSMIS tries to model the student from her behavior during which it automatically asks questions which con­ tribute to disambiguation of alternative clause selection and diagnosis. In other words, HSMIS asks questions regardless of their appropriateness in the sense of tutor­ ing. This requires some control mechanism of the HSMIS behavior. This subsection describes several additional mechanisms introduced to augment the HSMIS.

1 An ATMS node is a triple < D, L, J >, where D is the datum used in the reasoning system, Lis a label, which is a set of environment the dautm holds and J is a set of justi­ fications. An assumed node has the same set composed of a single identifier as a label and a justification( in this paper, the identifier of the assumption will be expressed with a;).

Virtual Oracles: Let us discuss the initial model prob­ lem. There are two alternative initial models: one is empty which means the teacher does not know anything about the student in advance and the other is complete knowledge (teaching material) which means teacher as­ sumes the students usually understand the material very well. Although the former case is reasonable, the system tends to ask many questions to get a lot of information of how well the student understands the material. On the other hand, the latter case does not require many questions at least for excellent students, since the model can explain their correct behavior. This characteristics is very reasonable in real tutoring. Therefore, we de­ cided to employ the latter. However, a serious problem still remains. One cannot simply put a clause into the student model without any justification.

In order to cope with this problem, we devised an Vir­ tual oracle generator, which generates plausible student answers based on the reliability of the current student model instead of asking questions. When a student's behavior is confined within the scope of her teacher's prediction, the teacher asks less questions by replacing the necessary information with correct answers. We call this type of oracle a "virtual oracles".

Let C be an SMDL clause p(X,T)::-ql(Xl,Tt), ... , q~c(X~c, T~c) which is either correct knoledge or plausi­ ble buggy knoledge in the teaching material. When the student makes an answer p( X', T') for the head of C and C is supported by p(X', T') and a set of cor­ rect answers concerning C, ATMS is informed of an as­ sumtion trust(C), which means "C is reliable." When trust(C) is in the current environment, Virtual ora­ cle generator generates a set of virtual oracles, that is, { < q1 (Xf,Tt), T{ >, .. ·, < qk(Xk,Tk), Tk > }. The vir­ tual oracles together with p(X', T') construct a correct top-level trace of C and are correct answers of the teach­ ing material. For each virtual oracle < qi(x:, Ti), Tf >, ATMS is informed its generation according to the fol­ lowing justification:

SMIS treats oracles and v..oracles in the same manner, while ATMS manages their consistency.

Meta-Oracles: Students sometimes want to say her knowledge in the form of knowledge instead of facts. And the system sometimes wants to ask the student the rea­ son why she answers a question that way. The following is an example.

System : Does rice grow in Russia? Student: Yes, it does. System : Why do you think rice grovs in Russia? Student: It has wide flat field and river.

In this case, HSMIS can obtain an oracle and a clause as follows.

< grow( rice, russia, T), true >

The clause obtained from the student are called "meta-oracle". When the clause C is added to the model based on a "meta-oracle", HSMIS informs ATMS of the following justification.

Similarly, when the clause C is removed from the model based on a "meta-oracle", HSMIS informs ATMS of the following justification.

The meta-oracle is dealt with as the following assump­ tion node of ATMS.

3.2.3 Detection of contradiction

The contradiction derived during the inference process of HSMIS is classified into the following seven types: 1) Contradiction of correctness, 2) Contradiction of cover test, 3)Contradiction of clause generality, 4) Contradic­ tion of trust, 5) Contradiction of meta-oracle, 6) Contra­ diction of oracle and 7) Failure of clause search. More detailed explanation of the contradictions and the mech­ anism to detect them is shown in [Ikeda et al., 1992). When any types of the contradiction is detected, ATMS is informed of it and updates the nogood record.

3.2.4 Resolution of contradiction

correct( C), uncover( C, A), general( C), trust( C) and metaOracle( C) are called to be default assumptions, which means that "so long as no contrary evidence is found, it is assumed to be in ". The set of these as­ sumptions included in the environment is called a de­ fault environment (expressed with De)· From this, the current environment Ce can be expressed with

Thus, contradiction can be classified into I) one re­ garding the default environment and II) one regarding the oracle environment. I) is the contradiction caused by the nonmonotonicity inherent to the inference process, whereas II) is the one caused by the nonmonotonicity of the student's answers.

I) A resolution method for contradiction of the default environment can be easily derived from its definition.

Suppose that contradiction is detected since there exist both the refutation( C) and the correct( C) in the current context. As has already been stated, the correct( C) can be hold so long as there does not ex­ ist the refutation for the clause C (refutation(C)). Therefore, the inconsistency can be resolved by remov­ ing the correct( C) from the default environment. Sim­ ilarly, the assumptions, uncover( C, A), trust( C) and metaOracle( C), are removed from the default environ­ ment when the contradictory data is found.

II) In the case of the oracle contradiction, it is nec­ essary for the distance between the two oracle sets to be minimized and all the contradiction already detected will be evaded in the new environment. This is done by the heuristic search method.

3.3 Behavior of HSMIS

In this subsection, we show an example of how HSMIS works, in which the description is partially simplified because of space limitation, for example, the description of teaching material is not correct in the strict sense( for example, the first argument of grow is omitted).

[An example of HSMIS modeling process]

Because ol is a correct answer, the correct clause Cl i· added to the model. And then, v_o2 and v_o3, which are correct answers, are generated by oracle-generator. They are justified by trust(CJ) and oracle(ol). ATMS is informed of the following assumptions and justifications. Assumptions: oracle(ol), trust(Cl), correct(Cl), general(Cl)

J usti]u:ations:

trust(Cl), oracle(ol) ~ v_oracle(v_o2)

trust(Cl), oracle(ol) ~ v_oracle(v_o3)

oracle(ol), v_oracle(v_o2), v_oracle(v_o3) ~over(Cl,ol). oracle(ol), correct(Cl), cover(Cl,ol), general(Cl)~model( Cl)

A buggy clause C2 i· added to the model, because o4 is a typical incorrect answer(Kiev is too cold for rice to grow). A virtual oracle v _o5, which is justified by trust(C2) and oracle(o4), is generated by the oracle-generator. Since the clause C 1 is a descendent node of C2 in refinement graph, model(Cl) become· 'out' by outing general(CI). Then the status ofv_o2 and v_o3 becomes 'out'. However, v_o3 becomes 'in' at once, because it is justified by trust(C2) and oracle(ol).

Assumeptions oracle(o4), trust(C2), correct(C2),general(C2)

J usti]u:ations:

trust(C2), oracle(ol) ~ v_oracle(v_o3)

trust(C2). oracle(o4) ~ v_oracle(v_o5)

oracle(o4), v _oracle(v _o5) ~over(C2,o4). oracle(o4), correct(C2), cover(C2,o4), general(C2)~model( C2)

Oracle environment

in ol:<growUapan),yes. > out v _o2:<tmpUapan), yes. > in v_o3:<soi1Uapan), yes.> in o4:<grow(kiev), yes.> in v _o5:<soil(kiev), yes.>

Does rice grow in Moscow?

lliL

o6:grow(moscow), no.

Is Soil of Moscow suitable for rice to grow?

~ o7:soil(moscow), yes.

SMDS: C2 is refuted by o6 and o7; Refulalion: gruw{mosCOUJfalst)::-srJ{mosC11DJ,trw) C2 i· removed because SMDS found out its refutation. A contradiction is found between refutation(C2) and correct(C2). CRS resolves this by outing the default assumption correct(C2). Then the model(C2), oracle(v_o3) and oracle(v_o5) become 'out'. HSMIS starts to search for a clause which covers o4.

J usti]u:ations:

oracle(o6), oracle(o7)~refutation(C2).

Oracle environment

in ol:<growUapan),yes. > out v _o2:<tmpUapan), yes. > out v _o3:<soi!Uapan), yes. > in o4:<grow(kiev), yes. > in v_o5:<soil(kiev), yes.> in o6:<grow(moscow), no. > n o7:<soil(moscow), yes.>

Is soil of Kiev suitable for rice to grow?

yes. oS:soil(kiev), yes. (confirmed by the student)

Is Temperature of Kiev suitable for rice to grow? !:!!L o8: temp(kiev), no.

SMIS: C3: grow(Place):-temp(Piace) cannot cover grow(kiev,yes~ Contradiction is found, because HSMIS has failed to search for a cover of grow(kiev,true). CRS changes the oracle environment to resolve the contradiction based on give-a­ priority-to-correct-answer heuristics. In this case, o4 becomes 'out' and o9, whose truth value is opposite to o4, is believed according to give-priority-to-correct-answer heuristic. Finally, Cl i· added to the current model (model(CJ) becomes 'in' again) in the new consistent oracle environment .

<Assumptions and JustifiCations are omiJted > Oracl~ environment

In order to realize the above behavior of HSMIS, at least two kinds of knowledge is required. One is the knowledge for refinement graph generation. In the above example, for example, the following knowledge is used for generating three clauses C1, C2 and C3.

declare_called(grow(Place, T),

(temp( Place, TI), soil(Place, T2 )])

This means that the predicates in the second argument, that is, temp( Place, TI) and soil(Place, T2), can appear in the body of a clause whose head is grow( Place, T). If this form of knowledge including necessary predicates is prepared, HSMIS can automatically generate a complete set of clauses as a model of the student.

The other one is the correct domain knowledge which provides HSMIS with correct answers. In the above ex­ ample, the knowledge is used for three purposes, that is, for the virtual oracle generation, the environment man­ agement by CRS, and the problem generation.

In the above example, the student model changed two times. The first change from C1 to C2 can be regarded as corresponding to the nonmonotonicity inherent to the in­ ference process, that is, C1 is not an appropriate hypoth­ esis of the student understanding at that time. Mean­ while, the second change from C2 to C1 corresponds to the nonmonotonicity of student's understanding.

4 Concluding remarks

Both SMDL interpreter and HSMIS have been imple­ mented in Common ESP(Extended Self-contained Pro­ log) and incorporated in a framework for ITS, called FITS[Mizoguchi and Ikeda, 1991). HSMIS can cope with a variety of teaching materials as far as it can be repre­ sented in Prolog. Therefore, the authors think that the generality of HSMIS is relatively high.

Two ITS's have been built using FITS, one is on ge­ ography and the other is on chemical reactions. Simple examination of both systems shows they run in real time if the oracle contradiction does not occur. When the or­ acle contradiction occurs and there is no heuristics for its resolution, we find that the cost to resolve the con­ tradiction is very expensive.

The current implementation of contradiction resolu­ tion is based on . a somewhat brute-force method us­ ing domain-independent heuristics. To improve the efficiency, more powerful domain-dependent heuristics should be employed. It seems promising to adopt a be­ lief revision mechanism developed by X. Huang et.al, which provides efficient, minimal revision of belief bases by using attention(focus) in the belief space[Huang et al., 1991b).

We have discussed mechanisms to avoid inconsistency in model inference in this paper. However, there exist such students who have contradictions in their head. To cope with modeling of such students, the system may not avoid the inconsistency but has to model inconsis­ tent knowledge as it is. This issue will involve the de­ velopment of more sophisticated control mechanism for student modeling. We are currently engaging in the issue, where student's inconsistent knowledge is mod­ eled in multiple worlds which are again supported by ATMS[Kono et al., 1992).

Acknowledgements : The authors are grateful to re­ viewers for their valuable comments.