Contents
1 Introduction

1

2 Contradictions in student modeling2

3 Nonmonotonic student modeling in a single world

10

4 Nonmonotonic student modeling in multiple worlds

19

5 Discussions

22

6 Concluding remarks

24

References

24

Appendix

26

A Formal de nition of execution of SMDL program

26

B Formal de nition of terms for SMIS

26

C ATMS

27

D Formulation of the inference process of THEMIS

27

2.1
2.2
2.3
2.4

What is a tudent knowledge contradiction? : : : : : : : : : : : : : : : : : : : : : : : : :Formulations of student knowledge contradictions based on the multi-world logic : : : :Classi cation and handling of contradictions : : : : : : : : : : : : : : : : : : : : : : : : :Heuristics to distinguish contradictions : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.1 SMDL: A student model description language : : : : : : : : : : : : : : : : : : : : : : : :3.2 SMIS: Inductive student model inference system : : : : : : : : : : : : : : : : : : : : : :3.2.1 Student model diagnosis system : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.2.2 Search for a new clause : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.3 ATMS : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.4 Managing consistency to control the model building process : : : : : : : : : : : : : : : :3.5 Assumptions to cope with single world contradictions : : : : : : : : : : : : : : : : : : :3.6 Detection and resolution of contradiction : : : : : : : : : : : : : : : : : : : : : : : : : :3.7 Behavior of HSMIS : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :

3
4
8
9

10
12
12
14
15
16
17
17
18

4.1 Inference process in THEMIS : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 19
4.2 Modeling student knowledge contradictions : : : : : : : : : : : : : : : : : : : : : : : : : 20
4.3 Correcting student knowledge contradictions : : : : : : : : : : : : : : : : : : : : : : : : : 21

C.1 Data structure of ATMS : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 27
C.2 Detection and resolution of contradiction : : : : : : : : : : : : : : : : : : : : : : : : : : 27

D.1 Description of model inference process of SMIS : : : : : : : : : : : : : : : : : : : : : : :D.2 Controlling mechanisms of the modeling process : : : : : : : : : : : : : : : : : : : : : :D.2.1 Virtual Oracles : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :D.2.2 Meta-Oracles : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :D.3 Formulation for multi-world model inference : : : : : : : : : : : : : : : : : : : : : : : : :D.4 Detection of contradiction : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :

i

27
29
29
29
29
30

List of Figures
1 Examples of behavior of a student who has undi erentiated concepts. : : : : : : : : : :2 Concept discrimination tree : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :3 Interpretation of the student contradiction : : : : : : : : : : : : : : : : : : : : : : : : : :4 Examples of multi-world student model representation in Prolog : : : : : : : : : : : : :5 Block diagram of THEMIS. : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :6 Examples of the top-level trace and the refutation for a clause. : : : : : : : : : : : : : :7 Prolog implementation of ip : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :8 Prolog implementation of fp : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :9 Prolog implementation of failp : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :10 An example of HSMIS modeling process : : : : : : : : : : : : : : : : : : : : : : : : : : :11 A hypothetical example of tutoring behavior using student knowledge contradiction. : :

3
5
6
7
12
13
14
14
15
19
22

List of Tables
1 Classi cation of contradictions in student modeling : : : : : : : : : : : : : : : : : : : : : 8
2 De nition of ^ and _. : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 11
3 Activation of SMDS subprocedures : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 13
4 Evaluation of student models : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 23ii

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 a snapshot of the student's knowledge. This isa reason why many e orts 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 ITSs. However, all the methods
have some limitations and no complete and sound inference procedure for modeling has been obtained
yet. In this paper, we formulate the student modeling problem as an inductive inference problem, i.e.,a problem of constructing a model explaining observed data which are, in our case, student's answers
to the problems given.
A student who is in the xing stage1 of the acquired knowledge often shows contradictory behavior.
This means a student is apt to apply problem solving methods unstably, since he2 has not built themor since he has not completed in a formulation of related concepts, etc. It is clear that he shows suchnonmonotonic learning processes in xing his knowledge in the process of acquiring new knowledge.
There are other types of contradiction to be considered in designing a student modeling system. A
modeling system often gets an answer from the student that is consistent with his current belief but
inconsistent with his past answers, because he has changed his mind as his learning proceeds or hesometimes makes careless mistakes, so-called \slips."
Contradictions which a modeling system should cope with are classi ed into the following two types:(1) contradictions which should be resolved by revising the student model, and(2) contradictions which should be captured as they are.
Generally speaking, an ITS should follow a student's nonmonotonic change. Furthermore, a student modeling system should realize more exible modeling behavior and construct reasonable student
models from didactic viewpoints by embodying a teacher's insight, e.g., the ability to capture her student's status by asking fewer questions. Contradictions of type (1) inevitably appear in the student
modeling process. Therefore, a student modeling system is required to have the ability to cope withvarious kinds of nonmonotonicities. To this end, a student modeling system should always make belief
revisions to keep data for inference consistent. Surprisingly, however, only Huang et al (1991a;1991b)
has tackled this problem, except that Woolf et al (1993) has pointed out its signi cance. The authors have been attacking this issue and developing an inductive student model inference algorithm
HSMIS (Kawai et al, 1987; Mizoguchi et al, 1987; Mizoguchi et al, 1991). HSMIS (Hypothetical Student Model Inference System) employs the ATMS (Assumption-based Truth Maintenance System)(deKleer, 1986) to maintain consistency of the student modeling process (Ikeda et al, 1988). The architecture of HSMIS is based on a logic-based inductive inference algorithm SMIS (Ikeda et al, 1989),
whose model description language is also a logic-based language called SMDL (Student Model Description Language) which takes four truth values to represent a student's understanding. This paper rst
discusses the characteristics of contradictions and nonmonotonicities observed in the student modelingprocess. Then a student modeling architecture to deal with those nonmonotonicities is presented, after
SMDL and SMIS are de ned. Thus HSMIS realizes relatively high model representation power andmodeling ability.
The second problem, that is, to capture a student's contradictory knowledge as it is, seems more
important from educational viewpoints. The Socratic method, for example, is a contradiction-basedtutoring strategy which teachers use especially to help students in the xing stage. It is a well-known
and already veri ed method that gives such a student a strong impression that he misapplied his
knowledge. Although building high- delity student models is an intractable problem (Self, 1988), an
ITS should have a student model which is precise enough to handle tutoring strategies integrated into
the ITS (Dillenbourg, 1989). In order to generate sophisticated tutoring behavior like the Socratic
method, student modeling methods should be able to cover a student's contradictory knowledge. His
knowledge acquisition and xing processes should be captured by modeling him as he is, even if he has
contradictory knowledge (Kono et al, 1992; Kono et al, 1993b; Kono et al, 1994).
1 \Fixing stage" means an intermediate learning stage where acquired knowledge is not completely established yet.
2 For simplicity \she" is used to refer to the teacher and \he" to refer to the student in general.

1Some might say that some ITSs, e.g., WHY (Stevens et al, 1977), have realized the Socratic method.
Tutoring behaviors generated by most Socratic tutors, however, do not notice or suggest contradictions
that exist inside a student in spite of the fact that such a suggestion is the real behavior of the Socratic
method. They only give a new negative example of his knowledge. They do not realize the real andcomplete Socratic method. HSMIS is equipped with a mechanism to cope with all the contradictionsof type (1) which are formulated in this paper. HSMIS generates student models in SMDL which has
more expressiveness than Horn clauses. Therefore, HSMIS realizes a high modeling ability and model
expressiveness which surpasses most other modeling methods.
This paper presents a new methodology for handling a student's contradictory knowledge in conjunction with Socratic tutoring based on the concrete foundation of student modeling. It is dicult for
not only modeling systems but also human teachers to distinguish the two types of contradiction, i.e.,
one where a modeling system should treat the student's knowledge as contradictory and the other where
the system should follow the student's nonmonotonic change, because all of their indications are very
similar. Two types of contradictions are formulated. Type (1) is named \single world contradiction"
which is coped with by HSMIS and type (2) is named \multi-world contradiction" which is coped withby the structure of a concept discrimination tree. The two methodologies, HSMIS and a multi-world
inference mechanism, are successfully incorporated into the architecture of THEMIS by enumeratingand equipping domain independent heuristics to distinguish the two types of contradiction. In the
newly formulated THEMIS, ATMS plays another important role of managing multiple worlds whichenable the modeling of students with contradictions.
This paper rst classi es and formulates the above two types of contradiction which should be
dealt with in student modeling. HSMIS, a nonmonotonic inductive student modeling system, which
is able to cope with single world contradictions is then formulated. Next, a mechanism which copeswith multi-world contradictions is formulated, which is incorporated into THEMIS based on HSMIS.
Finally, THEMIS is evaluated and compared with other representative systems.

2 Contradictions in student modeling
A student's answer to a question is represented by a pair of a fact and its truth value, and is called
an oracle. The student modeling problem can be formulated as an inductive inference problem, i.e., aproblem of constructing a model explaining observed data. A set of oracles acquired by observation of a
student's behavior within a certain period tends to be inconsistent for several reasons. Such inconsistentbehavior is classi ed into the following three types of contradiction according to the causes of them:[A1] Oracle contradictions caused by change of student's mind: A student's learning process is essentially attained by acquiring new knowledge causing change of his mind. The consistency of his
answers within the whole learning process can be easily lost, because he behaves based on his
current knowledge independent of his previous knowledge.
[A2] Oracle contradictions caused by slips: A student often makes careless mistakes. Oracles based onthem are inconsistent with his actual knowledge, hence, the set of oracles that contains slips isinconsistent.
[A3] Student knowledge contradictions: A student sometimes has inconsistent knowledge in his head
which also causes contradictory oracles.
These three kinds of contradiction are referred to as \student contradictions", since they are related tononmonotonicities of a student's behavior or knowledge.
The student modeling process is essentially hypothetical, hence, the completeness of an inferred
student model is not always guaranteed. The expectation of a student's answer deduced from thecurrent student model is often di erent from new oracles, when the current model does not completely
represent his current status. Assumptions which were assumed when the current model was inferredbecome inconsistent with the set of oracles. Such a type of contradiction is called[B] assumption contradiction in modeling.
Contradictions of type [A1], [A2] and [B] should be placed in the same category when classifying
them according to how to treat them, because all of them should be resolved by revising the current

2Question 1

Question 2

Question 3

A sphere has passed through the origin with ve- A sphere has passed through An sphere is thrown directly uplocity 19:6m/s to the right at t = 0s. It continues the origin with velocity 19.6m/s wards with initial velocity 19:6m/s
linear and uniformly accelerated motion along x- to the right at t = 0s along x- at t=0s. It reaches at the maximum
axis of a horizontal plane, and stopped at t = 2s. axis of a horizontal plane. P is hight at t=2s. Determine the direcIt mass = 2kg. Get its displacement at t = 1s. moving with linear motion with tion of the applied force at t=1s.
Determine both the direction and the magnitude its velocity decreasing at a uni- Student's
answerv 0v
0of the applied force.
formed rate. It stopped at t = vt = Tt00 0T00 3 t + v0 = 192:060
0 31+0tStudent's answer
2s. Determine its displacement
=
9
:8m/s
vt 0v0
19:6 = 09:8m=s2= 0020a =at t = 1s.
It is still moving upward at t = 1s.
Tt 0T002Student's answer
0
9
:831
1
2
St = S 0 + v0 t + at = 0+19:6 3 1+
= 14:7 S = S +vt = 0+19:631 = 19:6 Therefore, it is still receiving upward22
t0
force at t = 1s.
The displacement is 14.7m from the origin.
The displacement is 19.6m.
2
F = ma = 2 3 09:8 = 019:6kg1m/s
It receives 19.6 kg1m/s2 of force to the left.

Figure 1: Examples of behavior of a student who has undi erentiated concepts.
student model. On the other hand, contradictions of type [A3] should not be resolved, but a student's
contradictory knowledge should be represented as it is so as to utilize them e ectively in tutoring.
Some examples of student knowledge contradictions are given in Section 2.1, and a formulation of
the contradictions is made based on the multi-world logic in subsequent subsections. All types of theabove contradictions in student modeling are then classi ed and discriminated from the viewpoint of
how they should be handled in the student modeling process.
2.1 What is a tudent knowledge contradiction?

Let us assume that a student is in the stage of acquiring a certain new concept and that he has not fully
discriminated it from other related concepts he has already acquired. Such a student is apt to behave
unstably in applying knowledge to solve problems which contain the undi erentiated concept. Figure
1 indicates the behavior of a student who has undi erentiated concepts, i.e., the concept of \uniform
motion" and the concept of \uniformly accelerated motion." He correctly calculated the location of
P in Question 1, which speci es the type of motion as \linear and uniformly accelerated motion." In
Question 2, however, he mistook a uniformly accelerated motion for a uniform motion, and so applied
problem solving knowledge for uniform motion. Such a situation occurs due to his confusion between
the two concepts. As a result, his problem solving ability becomes unstable.
A student can choose certain problem solving methods appropriate for the problem given, if he has
well-discriminated concepts and has adequate knowledge of their attributes. If he has not, however, hemight misapply a procedure which belongs to another world by taking no notice of particular attributesof the problem. For instance, methods to \calculate the location of a moving object" are associated withboth concepts, such as uniformly accelerated linear motion (St = S0 +v0 t+at2 or St = S0 +(v0 +vt)3t=2)
and uniform motion (St = S0 + vt). In solving Question 2 in Figure 1, he retrieves the method de nedin the concept of uniform motion, while he should apply the method de ned in the concept of uniformly
accelerated linear motion.
A more interesting example of student knowledge contradiction is found in Question 3 in Figure 1.
The student who had correctly calculated the force that the sphere receives in Question 1 could not
determine the correct direction of the force in Question 3 in spite of the fact that the two motions are
physically identical except for the direction of the motion.
Such con icts among his answers suggest the \multi-world inference" assumption that he partitions
his whole storage and inference space. Each small partition in his inference space with relevant storageis called a \world." He stores problem solving methods and rules which he can handle at once in eachworld. He can retrieve and utilize these methods in a certain world, only when he makes inferences in
the world. A contradiction can be found when he utilized two di erent worlds in solving problems. One
is the world of well-formulated physics for Question 1 in which he stores the knowledge learned throughthe curriculum of physics, e.g., formulas and de nitions, and another is his naive physical world for
Question 3 which has been deeply engraved on his memory since his childhood, for instance. He has a\motion implies a force" misconception (Clement, 1982) in the naive one in this case. It is inconsistent
with the knowledge for \uniformly accelerated motion" in the well-formulated one. He has answered

3

that the force is directed upward because he used the naively misconceptualized world.
\Student knowledge contradictions" are de ned in this paper as the status which causes behaviors which can be regarded as a contradiction viewed from the standpoint of an observer. A typicalinterpretation of contradiction is as follows: He places more than two series of problem solving methods, which are originally placed in di erent
worlds of concepts, in the same world regardless of their attributes. This is caused by his failure
in di erentiating them from each other.
 He makes decisions which are able to derive di erent truth values for a certain fact within alimited time, since his knowledge is unstable.
2.2 Formulations of student knowledge contradictions based on the multi-world logic

Here we discuss a formulation of student knowledge contradictions based on the concept discrimination
structure and multi-world logic mentioned in Section 2.1. It is an intractable problem to try to modela student's inconsistent knowledge in a single reasoning space, since it cannot represent contradiction.
This suggests we need another modeling paradigm which is able to cope with inconsistency.
The formulation is based on the authors' speculation that human beings partition their whole storageand inference space into multiple \worlds" and organize them in a discrimination tree to retrieve theirknowledge eciently by
1. rst retrieving which world (concept) the given problem belongs to along a certain discriminating
structure, and2. retrieving and executing methods that contribute to problem solving in the world corresponding
to the problem.
The rst step, i.e., the decision on the target world, is regarded as a search on a concept discrimination
tree as depicted in Figure 2. Each node of a discrimination tree corresponds to a concept and each leaf
node to a world. When a problem is given to the current model, the discrimination tree in the modelis at rst interpreted to retrieve the conceptual world the problem belongs to by searching the tree
from its root. The searching and retrieval process is called discrimination level reasoning. The second
step is regarded as a search for and execution of methods that contribute to solving the problem. A
set of problem solving methods is de ned inside each world. Method level reasoning is thus carried out
in the retrieved world, each of which consists of consistent knowledge. Contradiction is modeled asa mixture of multiple worlds which is caused by an incorrect discrimination tree structure. Roughly
speaking, therefore, student knowledge contradictions are represented as wrong concept discrimination
conditions, while conventional bugs are represented as wrong methods inside each world.
Problem solving knowledge is represented as a set of predicates whose formula is either solve(G; X~in ; X~out )or goal(X~in ; X~out ). G denotes the goal of the problem, that is, what should be determined under what constraints. X~in is a vector of input variables which are instantiated and X~out is a vectorof output variables which are not instantiated when the predicate is called. fX~in ; X~outg represents
whole the articulation of the problem space. For instance, the problem space \motion" is represented
as fm; (s(t); As ); (v(t); Av ); (a(t); Aa ); (f (t); Af ); [(T0; S0 ; V0 ; a0 ; F0 ); 1 1 1]g, where the elements are themass of the moving object, location, velocity, acceleration and applied force as functions of time elapsed,and sets of the elements of the motion, respectively. Each function of time elapsed is denoted as a couple of the function itself and the attribute of the function. The problem space, which is adopted in
Question 1 in Figure 1, is represented as f2; (s(t)); (v(t)); (a(t); f ixed); (f (t)); [(2; S0; (0; 0); a0 ; F0 );(0; (0; 0); (19:6; 0); a1 ; F1 )]g. When the problem solving begins, input variables are given in the formula
as instantiated variables. For instance, the location and the velocity on t = 0 are instantiated as (0; 0)and (19:6; 0), because they are given in the problem. Problem solving is a retrieval and an executionof methods described in the problem solving knowledge base, to get the output parameter list fX~out ginstantiated from the given input parameter list fX~ing.
The given problem is represented as a vector of primitive attributes which is used for deciding theworlds the problem belongs to by tracing the given tree from its root. Each conceptual node on the treethat is not a leaf node has no problem solving methods but discrimination knowledge, which de nes what4

Figure 2: Concept discrimination treechildren nodes the node has and what conditions the problem must satisfy to discriminate each childconcept from others. The conceptual node Ni that has children concepts Ni1 1 1 1 Nij has discrimination
knowledge d(Ni ; [Ni1 ; 1 1 1 ; Nij ];[Ci1; 1 1 1 ; Cij ]) in general. To go forward through the path from Ni to Nik(1  k  j ) requires that fX~ing, input variables of the problem, should satisfy Cik , the discrimination
condition for Nik . In Figure 2(a), the discrimination knowledge d(N1 ; [W1 ; W2 ]; [C1 ; C2 ]) is de ned forthe conceptual node N1 that has children worlds W1 and W2 , e.g., to go from N1 to W1 requires the
problem to satisfy the condition C1 . Let us assume that N1 corresponds to the concept of \linear
motion", W1 to \uniform motion", and W2 to \linear and uniformly accelerated motion." Given thevector for Question 1 in Figure 1, it traces a path on the tree from the root and reaches the world
W2 via N1 , because it satis es the discrimination condition C2 , e.g., constant(At ) which means \theacceleration is constant." In each world, m(Wi ), a set of problem solving methods which belong to
Wi , is given. A method level student model, i.e., model of the method set m(W i), corresponds to aconventional student model. When Sw , the set of the worlds to which the given problem belongs, isidenti ed, methods which contribute to solving the problem are retrieved and executed from the unionof method sets, each of which is an element of Sw . When only one world W2 is retrieved, method levelreasoning takes place inside the world, i.e., problem solving methods are retrieved from m(W2 ) and
executed. A discrimination condition has a predicate formula, which is called a world predicate andboth C1 and C2 are world predicates in Figure 2. Each world predicate takes only input variables, i.e.,
fX~in g, as its argument.
Student knowledge contradictions are modeled in terms of erroneous concept discrimination trees,
because the student who has such an erroneous tree cannot manage consistency in retrieving problem

5Figure 3: Interpretation of the student contradiction
solving methods as mentioned above. Such kinds of contradiction can be modeled by erroneous world
predicates in the multi-world model. When a student has not fully discriminated concepts Nip andNiq (1  p < q  j ) which are both children nodes of Ni , the discrimination knowledge of Ni in the student model for him is revised to be d(Ni ; [Ni1 ; 1 1 1 ; Nip ; 1 1 1 ; Niq ; 1 1 1 ; Nij ]; [Ci1 ; 1 1 1 ; Cip _Ciq ; 1 1 1 ; Cip _Ciq ; 1 1 1 ; Cij ]),i.e., discrimination conditions for both Nip and Niq become Cip _Ciq . Method level reasoning of the
problem that belongs to any descendant worlds of either Nip or Niq takes place in the combined reasoning space m(Niq @Niq ) such that both method sets m(Nip ) and m(Niq ) are merged into it, wherem(Nip ) contains all the methods de ned in all the descendant worlds of Nip and m(Niq ) contains
those of Niq . The model of the student who has not fully discriminated uniform motion and uniformly accelerated motion, in the above example, is represented by the discrimination knowledge ofN1 , d(N1 ; [W1 ; W2 ];[C1 _C2 ; C1 _C2 ]) as depicted in Figure 2(b). Method level reasoning is done in the
combined reasoning space m(W1 @W2 ). Such model representation and interpretation enables the capture of his unstable applications of knowledge. When he becomes able to discriminate these concepts,
the discrimination model is revised again to be correct and method sets that had been combined sincethen are restored.
Figure 3 illustrates a few instances of simpli ed student models. Each predicate written beside eacharc of the tree, e.g., solve in naive world, is the world predicate which discriminates the child conceptual nodes of the parent one. The student model for a student who has not yet discriminated between
uniform motion and uniformly accelerated motion is illustrated in Figure 3(a). World predicates forthese concepts are revised to be uniform motion(X~in )_ unif ormly accelerated motion(X~in). Figure3(b) represents the status of the student who has the \motion implies a force" misconception in his
naive world and unstably applies it in solving physics problems. World predicates for the naive world\solve in naive world(X~in )" and that for formulated worlds \solve in f ormulated world(X~in)" areboth revised to be solve in f ormulated world(X~in )_solve in naive world(X~in ). Although student's
undi erentiation of concepts is represented by the disjunctive of world predicates as is explained above,
conventional bugs are represented by wrong methods in a certain world. The student who has wrong
knowledge, say knowledge for calculating location of the object that is moving linearly and uniformly,
is modeled so that there exists at least a wrong method, e.g., \St = V0 3 t" in place of \St = S0 + V0 3 t,"
in the world of uniform motion.
More detailed multi-world model descriptions are given in Figure 4 using the geographic domain.
The domain is structured aiming to make a student understand that climates of seaside regions are6

d(earth, [southern hemisphere, northern hemisphere],[southern hemisphere(Place),
northern hemisphere(Place)]).
m(southern hemisphere, [(grow(Crop, Place, T ) :suitable temperature(Crop, Place, T1 ),suitable soil(Crop, Place, T2 ),suitable lay(Crop, Place, T3 ),has irrigation(Place, T4 ),and(T1 ,T2 ,T3 ,T4 ,T )),(suitable temperature(Crop, Place, T ) :middle latitude(Place, T ))]).
m(northern hemisphere, [(grow(Crop, Place, T ) :suitable temperature(Crop, Place, T1 ),suitable soil(Crop, Place, T2 ),suitable lay(Crop, Place, T3 ),has irrigation(Place, T4 ),and(T1 ,T2 ,T3 ,T4 ,T )),(suitable temperature(Crop, Place, T ) :middle latitude(Place, T )),(suitable temperature(Crop, Place, T ) :middle high latitude(Place, T1 ),west coast(Place, T2 ),and(T1 ,T2 ,T ))]).

d(earth, [southern hemisphere, northern hemisphere],[southern hemisphere(Place)_northern hemisphere(Place),southern hemisphere(Place)_northern hemisphere(Place)]).
m(southern hemisphere, [(grow(Crop, Place, T ) :suitable temperature(Crop, Place, T1 ),suitable soil(Crop, Place, T2 ),suitable lay(Crop, Place, T3 ),has irrigation(Place, T4 ),and(T1 ,T2 ,T3 ,T4 ,T )),(suitable temperature(Crop, Place, T ) :middle latitude(Place, T ))]).
m(northern hemisphere, [(grow(Crop, Place, T ) :suitable temperature(Crop, Place, T1 ),suitable soil(Crop, Place, T2 ),suitable lay(Crop, Place, T3 ),has irrigation(Place, T4 ),and(T1 ,T2 ,T3 ,T4 ,T )),(suitable temperature(Crop, Place, T ) :middle latitude(Place, T )),(suitable temperature(Crop, Place, T ) :middle high latitude(Place, T1 ),west coast(Place, T2 ),and(T1 ,T2 ,T ))]).

(a)

(b)

Figure 4: Examples of multi-world student model representation in Prolog
di erent between the Southern hemisphere and the Northern hemisphere because of the e ects of sea
currents. The whole correct model except knowledge of instances (correct facts) is given in Figure 4(a).
The conceptual node \earth" is the root of the discrimination tree and has two children worlds \southern hemisphere" and \northern hemisphere." World predicates \southern hemisphere(Place)" and\northern hemisphere(Place)" are given for discrimination conditions. Each input variable, i.e.,
Place, is bound to a name of the region and the discrimination knowledge evaluates which world the region belongs to. If a region is in the Northern hemisphere, world predicate northern hemisphere(Place)indicates true and world northern hemisphere is selected. Method level student models are actually
represented in SMDL which is an extended version of Prolog and is formulated later, though they are
written in Prolog in the gure. In each clause of method level models, only the last parameter, the truth
variable, is the output variable and all other parameters, i.e., Crop and Place, are input variables. The
correct method level student model of the world southern hemisphere consists of two clauses, whichmean \The Crop grows in a certain Place, if the temperature, the soil, and the lay of the Place issuitable and there exists enough irrigation," and \The temperature of a certain Place is suitable for
the Crop, if the Place is the middle latitudes," respectively. The correct method level model of theworld northern hemisphere is additionally given a clause that means \The temperature of a certain
Place is suitable for the Crop even if the Place is in relatively high latitude, if the Place is on thewest cost of a continent," because warm currents and wind from the west bring such regions a warm
climate in the Northern hemisphere.
The discrimination knowledge of the student model in Figure 4(b) is revised from the correctone (underlined), i.e., both world predicates for southern hemisphere world and northern hemisphereworld are southern hemisphere(Place)_northern hemisphere(Place). Such a representation of thediscrimination knowledge denotes that the student has not yet correctly discriminated the two worlds.
Given a problem on this subject, for instance, \Does wheat grow in the southern part of Chile?," bothof the discrimination conditions indicate true, so the student model interpreter generates a combined
method set of the two worlds. Then the model in the southern hemisphere world correctly returns
f alse, but the model in the northern hemisphere world returns true which causes a contradiction.

7

Table 1: Classi cation of contradictions in student modeling(a) Classi cation by cause
Classi ed nameType
Student Contradiction [A1][A2][A3]Modeling Contradiction [B](b) Classi cation by handlingClassi ed nameTypeSingle World Contradiction [A1][A2][B]
Multi-World Contradiction [A3]2.3 Classi cation and handling of contradictions

Contradictions enumerated at the beginning of this section are classi ed by their causes into two
categories:
1. student contradictions ([A1][A2][A3]),
2. modeling contradictions ([B]).
Student contradictions are caused by inconsistencies of a student's behavior or his knowledge itself. On
the other hand, modeling contradictions are caused by inconsistencies between the knowledge that a
student actually has and the knowledge that is represented in the student model. This classi cation issummarized in Table 1(a).
Next, let us classify these contradictions from the viewpoint of how they should be handled in
student modeling. This classi cation is summarized in Table 1(b).
An inconsistency between a student's actual understanding and a student model must be caused
by faulty assumptions that were hypothesized in a previous inference stage and have been believed. A
nonmonotonic student modeling process is required to get rid of these inconsistencies, i.e., to revise thestudent model so as to be consistent with the student's knowledge:
1. set up assumptions that are necessary to construct the student model which satis es the set ofgiven oracles in each phase of student modeling,
2. derive the model from these assumptions and record the derivation process,3. when a certain inconsistency between the oracle set and the model is detected, nd a set ofassumptions which causes the inconsistency,
4. resolve the contradiction by revising the system-made assumptions in the set and continue themodeling.
Considering each oracle as an assumption, the above nonmonotonic modeling methodology to resolve
the inconsistencies is applicable to contradictions of types [A1] and [A2]. Oracles that are not consistent
with a student's current understanding should be removed from the current assumption (oracle) set. A
student model that is consistent with a student's understanding can be constructed from the assumption
set manipulated in such a way inside a single world. Single world contradiction is a general term forthese types of contradictions, i.e., [A1], [A2] and [B], which a modeling system should try to build aconsistent model of in a single world by nding an appropriate set of oracles (assumptions).
The above four steps of the belief revision process suggest that ATMS is appropriate for a coremodule of the controlling mechanism for student modeling. In ATMS-based problem solving systems,
ATMS and an inference system work in collaboration with each other. The inference system executes
problem solving and informs ATMS of its inference process. The consistency among data dealt with by
the inference system are managed by ATMS. ATMS holds and revises a set of valid assumptions whichis the origin of the inference and derivation process of data by the inference system. When derivationof a contradiction is informed, ATMS calculates the set of assumptions which causes the contradiction
by tracing back the informed derivation paths from the contradiction. When an assumption is denied,data which rely on it can not hold any more and hence are automatically denied by ATMS. In addition,

8

ATMS is able to avoid redundant calculations which have previously been made, which is useful tomake the inference process very ecient.
All the single world contradictions, i.e., [A1], [A2] and [B], are dealt with by the same mechanism,
which is realized by formulating the inductive student modeling process on the basis of ATMS in
HSMIS. A detailed description of this topic is given in Section 3.
In the case of student knowledge contradictions, i.e., type [A3], on the other hand, contradictions
in his knowledge should not be resolved but should be represented as they are. As is discussed in
the above two subsections, such a type of contradiction is represented well on the basis of multi-world
logic, and is called a \multi-world contradiction" in contrast with a single world contradiction. Basedon the multi-world formulation, a student knowledge contradiction can also be de ned as a certain
kind of inconsistency which arises among some assumptions that have been assumed in the inference
process in a manner similar to a single world contradiction. It is hence possible to capture a student's
contradictory knowledge by formulating its detecting/handling methodology.
The student modeling system THEMIS which is able to cope with multi-world contradictions consistsof HSMIS and the controlling mechanism of multiple worlds. HSMIS makes inferences consistently ineach world coping with and resolving single world contradictions. When a multi-world contradiction isdetected, HSMIS passes the control to the Multi-World Controller. It revises the concept discrimination
tree of the given domain knowledge to represent the contradiction. A detailed description of this topic
is given in Section 4.
2.4 Heuristics to distinguish contradictions

It is dicult for not only modeling systems but also human teachers to distinguish and detect thefour types of contradictions, i.e., type [A1], [A2], [A3] and [B], which are the essentials in student
modeling as already mentioned, because all of their indications are very similar (Dillenbourg et al, 1992;
Self, 1993b). They are triggered by a di erence between the expectation of the student answer deduced
from the current student model and his actual answer. One of the research goals of this paper isto produce a generic and formulated modeling mechanism which is able to cope with these kindsof contradictions. Although a generic methodology to distinguish them is not fully developed, someheuristics are employed as shown below.
Let us assume that the certainty of every given oracle and clause in the student model can beavailable. Both single world contradictions and multi-world contradictions are detectable by quite
similar triggers, i.e., the expectation from the model and the actual oracles. The contradiction resolving
procedures of those contradictions are quite di erent from each other. Single world contradictions
need to be resolved by revising the set of oracles or the current model in general. The contradiction
resolution procedure for each type of single world contradiction is a bit di erent, and hence the detection
processes for them are di erent from each other. In the heuristics, multi-world contradictions are rst
distinguished from single world contradictions.
Student knowledge contradictions, i.e., type [A3], should not be resolved, because the student's
inconsistency should be modeled as he is. Student knowledge contradictions require the revision ofneither the oracle set nor the clauses that are inconsistent with oracles, but the discrimination structure
to permit it to contain the inconsistency. Such a di erence in treatment of multi-world contradictions
and single world contradictions suggests the following way of discriminating them. If either the certainty
of a clause which is inconsistent with valid oracles or certainties of some of the oracles are less than acertain threshold, the inconsistency should be considered to be a single world contradiction and hence
should be resolved. On the other hand, if all the certainties are high enough, the inconsistency is
considered to be a student knowledge contradiction. They are not revised but put into some worlds,
i.e., all the reliable data can be alive in the multi-world formulation. The following heuristics to detect
contradictions of each sub category of single world contradictions are incorporated.
The change of student's knowledge which causes type [A1] of contradictions occurs especially rightafter his errors are corrected. He then generally changes his understanding from an erroneous toa correct status. It is appropriate to apply revision procedures for type [A1], when correct oracles
are obtained right after tutoring, i.e., the system resolves the contradiction by excluding the pastoracles inconsistent with correct clauses, or by asking him truth values of the oracles. The revision of9oracles results in the revision of the model, i.e., erroneous clauses are dismissed and correct clauses areappended.
Independently of the correctness, generally speaking, the student ought to have consistently applied
the clauses that are inconsistent with newly obtained oracles throughout a certain period, in the casethat he makes careless mistakes which cause type [A2] of student contradictions. Thus such a typeof contradiction is detected by similar criteria as those for student knowledge contradictions, i.e., theinconsistent oracles and clauses would be both reliable enough. There are two ways to distinguish them;
one is to consider a situation as a type [A2] only when the situation could not be treated as a student
knowledge contradiction, and another is to ask him a very similar question to get a con rmation.
These contradictions can be more suciently distinguished by introducing and enriching domain
dependent heuristics, e.g., \Students tend to mistake a uniformly accelerated motion for a uniform
motion if the motion is vertical," in addition to the domain independent heuristics explained above.
There is one more point which should be considered in designing a student modeling system. It canbe assumed that there exists a student who hardly behaves consistently, because of his low ability or
the system's inappropriate selection of the level of task. It does not make sense to let such a student
complete the current task. It is possible to detect such a status of the student by diagnosing the pastrecord of acquired oracles. In such cases, the modeling system should give up modeling him and informthe monitor of the failure so as to let the student go back to elementary tasks.

3 Nonmonotonic student modeling in a single world
On the basis of the above conceptual-level discussion on contradictions in student modeling, this section
proposes a powerful nonmonotonic inductive student modeling methodology which is able to cope withsingle world contradictions. Student models have to satisfy the following requirements in addition to
the requirements for the nonmonotonicities already discussed:
1. Accuracy-cost tradeo : In general, the more accurate the student model becomes, the more e ective
the behavior of the system becomes. However, there exists a tradeo between the accuracy of themodel and the cost of constructing it. From a pragmatic viewpoint, we must set up an appropriate
representation scheme for student models by taking the tradeo into consideration.
2. Unknown assertions: When a student fails to deduce his own solution for a problem, he would
say to his teacher \I could not solve the problem." Needless to say, this assertion does not mean hedoes not have any knowledge. The student model module should use this assertion as informative data
about his knowledge and construct a model which explains why he cannot deduce the answer from his
own knowledge. This requires the student model to deduce \unknown" assertions.
3. Theoretical foundation: Domain-independent and theoretical foundations for the student modelingmechanism should be de ned. It contributes to both the clari cation of the inherent properties of thestudent modeling problem and to the articulation of the scalability and reusability of the proposedmechanism.
To meet these requirements, the authors have developed a student model description language
SMDL and a hypothetical student model inference system HSMIS. SMDL is an extended version of
Prolog and takes four truth values including \unknown" to model the student precisely. HSMIS,an extended version of Shapiro's MIS (Model Inference System) (Shapiro, 1982; Shapiro, 1981), is
an inductive inference system for SMDL. In HSMIS, ATMS: Assumption-based Truth Maintenance
System (deKleer, 1986) is employed for dealing with nonmonotonicities. HSMIS has been implemented
in Common ESP(Extended Self-contained Prolog) on SPARC station (AIR, 1990).
3.1 SMDL: A student model description language

In addition to the above requirements, a student model is required to represent not only students but
also the systems' understanding of the students, which implies the model has to distinguish the twostates: The system can predict the behavior of the student and the system cannot. When the modelis based on logic, which is our case, it has to have two truth values, true and false, to denote theabove two states, respectively. Needless to say, the former state, i.e., the 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 believes it is false" and \the student does not

10

^

true
unk.
false
fail

(a)
true
true
unk.
false
fail

Table 2: De nition of ^ and _.

^ operator
unk.
unk.
unk.
false
fail

false
false
false
false
fail

_

fail
fail
fail
fail
fail

true
unk.
false
fail

(b)
true
true
true
true
true

_ operator
unk.
true
unk.
unk.
fail

false
true
unk.
false
fail

fail
true
fail
fail
fail

ascertain its truth", respectively. Then, we have two seemingly the same truth values \false", which
can be discriminated as follows: Employing Prolog terminology, the former \false" is treated as \fail"and the latter as one of the three values corresponding to \success." Discrimination among the threevalues is done by introducing an auxiliary argument interpreted by a meta-interpreter.
Facts are represented in SMDL as follows.
torrid(paris,false). temperate(paris,true). fertile(paris,unknown).

These three facts represent \The student believes Paris is not in the torrid zone but in the temperatezone and does not know whether it is fertile or not."Clauses are written in the form of
A :: 0B1 ; B2 ; 1 1 1 ; Bk
A is called a head and the RHS of the clause is called a body. Some simpli ed examples are shown
below.
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 and wet zone then the plant grows in X ." Intuitively, the clauses with the same head havea disjunctive relation and the predicates in the body have a conjunctive relation. Given a goalgrow(paris,T ) , the SMDL interpreter calls the subgoals temperate(paris,T1 ) , torrid(paris,T2 )and wet(paris,T3 ) in this order. The truth value T of grow(paris,T ) is obtained according to
T = T4 _T5 = T1 _(T2 ^T3 ) = true_(f alse^unknown). The semantics of the logical operators \^" and\_" are shown in Table 2.
The predicate of SMDL is of the form p(X1; X2 ; 1 1 1 ; 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 ; 1 1 1 ; Xm , isabbreviated as X~ . T is a truth variable or one of four truth values.
An SMDL clause is of the form: H ::-B1; B2 ; 1 1 1 ; Bn ; n  0, where H; Bi (1  i  n) are predicates.
In the case of n = 0, it is called a fact. The SMDL program P is a nite set of clauses.
The execution process is de ned as two di erent forms: Weak-resolution and strong-resolution. The
former is like the execution process of Prolog, i.e., \a goal succeeds in weak-resolution i there exists atleast one clause which derives the goal" (see De nition A.1 in Appendix A). On the other hand, strongresolution is somewhat di erent and complicated. Roughly speaking, a goal with truth value T succeeds
in strong-resolution, i all the OR clauses uni able with the goal succeed and the result of the OR
evaluation is T (see De nition A.2 in Appendix A). Generally speaking, a goal with truth value true canbe weakly derived but a goal with another truth value needs to be strongly derived. For instance, a goalgrow(paris,T ) succeeds in weak-resolution with truth value true by executing only the rst clause, if
a subgoal temperate(paris,true) succeeds. On the other hand, a goal grow(antarctica,T ) needs
to succeed in strong-resolution with truth value f alse by executing both clauses to call the subgoals
temperate(antarctica,T1 ) , torrid(antarctica,T2 ) and wet(antarctica,T3 ) , whose execution
results are f alse, f alse and true, respectively, and to obtain the truth value of the goal according tof alse _ (true ^ f alse). Formal de nition of the execution of goal G with program P is given in
De nition A.3.

11

Figure 5: Block diagram of THEMIS.
3.2 SMIS: Inductive student model inference system

Figure 5 shows the block diagram of THEMIS. HSMIS, the core module of THEMIS, consists of SMIS
(Ikeda et al, 1989), ATMS (explained below), The Virtual oracle generator (also explained below) andthe Contradiction resolving system (CRS). The main task of ATMS is to manage the consistencyof a set of assumptions (environment) used by the problem solver, SMIS in our case. The 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 the student questions. CRS
resolves the inconsistency identi ed by changing the environment.
A pair of a problem and an answer to it is called an oracle and is used as data to be covered by themodel obtained. An oracle is of the form < p(X~ 0; T ); T 0 >; where X~ 0 is a sequence of ground terms,
T is a truth variable and T 0 2 f true; f alse; unknown g (see De nition B.1 in Appendix B). Because
f ail represents the system's understanding of the 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 .
SMIS applies the following procedure repeatedly to the model:(1) if there is a di erence between an oracle and the fact derived from the student model, activate
the student model diagnosis system, SMDS, to identify the cause of the di erence.
(2) According to the diagnosis, SMIS selects an appropriate operation, either removal of an -refuted
clause or addition of a new clause, and informs ATMS of the process.
3.2.1 Student model diagnosis system

SMDS traces the resolution process of the current model and checks the results with oracles. SMDS has
three subprocedures, that is, ip , fp and failp . The procedure ip nds out where a new clause should
be added. The procedure fp detects an -refuted clause which should be removed from the model. The
procedure failp dynamically decides which procedure, fp or ip , should be activated. SMDS selectively
activates one of them according to the di erence between the oracle's truth value and the one derived
from the student model(See Table 3).
~ T )::-q1 (X~1 ; T1 );Let us assume that there exists an oracle H =< p(X~ 0; T ); T 0 >, a clause C = p(X;
~2 ; T2 ); 1 1 1 ; qk (X~k ; Tk ), and the set of oracles q1 (X~10 ; T10 ); q2 (X~20 ; T20 ); 1 1 1 ; qk (X~k0 ; Tk0 ) that derives
q2 (X~ 0; T 0) with C . The set of oracles is called a top-level-trace of C for H (see De nition B.2 inp( XAppendix B). A simpli ed but concrete example of a top-level trace is shown in Figure 6, where the12Table 3: Activation of SMDS subprocedures

Figure 6: Examples of the top-level trace and the refutation for a clause.
oracles O1 ; 1 1 1 ; O6 correspond to student's answers (a) through (f), respectively. In this case, the clause
C covers O1 , where the top-level trace is made by O2 and O3 .
Let us assume that there exists an oracle O7 : < grow(rice; kiev; T7 ); true >. The top-level traceof C for O7 can be made, i there exist the following two oracles:
O8 : < suitable temperature(rice; kiev; T8 ); true > andO9 : < suitable soil(rice; kiev; T9 ); true >.
However, when there exists an oracle O80 : < suitable temperature(rice; kiev; T80 ); false > insteadof O8 and there are no OR clauses uni able with the goal O7 , O7 cannot be weakly-derived from thecurrent model. In such a situation, the model P is said to be too weak with respect to a goal O7 (seeDe nition B.3 in Appendix B). When a weakness is detected in P , ip is activated and it searches forthe cause of the weakness by proving each clause in the proof tree of the oracle. Formal de nition of
top-level-trace and weakness is given in Appendix B.
~ T ), T 0 , Body, Tb )Figure 7 shows a Prolog implementation of ip . The goal good oracle top( p(X;~ T )::- Body 2 P which has a correct top-level trace. If such a clause does not exist,nds a clause p(X;0~
the goal p(X; T )is uncovered by P and returned as an output by ip . Otherwise, ip is recursively called.
To cover the uncovered goal detected by ip , HSMIS searches for a new clause to add into the model.
We de ne a binary relation \" over truth values. When two clauses derive di erent truth values,
T1 and T2 , for a goal, we say T1 is stronger than T2 i T1 = T1 _ T2 and write T1  T2 (see De nition
B.4 in Appendix B).
We say a model is too strong with respect to a goal, if it has at least one clause which derives astronger truth value than the oracle with respect to the goal (see De nition B.5 in Appendix B). A toostrong model has at least one -refuted clause which has a refutation (see De nition B.6 in Appendix
B). In Figure 6, the clause C is refuted by oracles O4 , O5 and O6 . The -refuted clause, which should13ip( (A,B), (Ta, Tb), C ) :weakly derive( A, Ta)ip( B, Tb, C );ip( A, Ta, C ).
ip( A, Ta, C ) :good oracle top( A, Ta, Body, Tb)
ip( Body, Tb, C );C = [A::Ta, uncover].

!

!

Figure 7: Prolog implementation of ip
fp( A, T, C ) :refutation( A, T, Body, Tb),
check refutation( Body, Tb, Cb),
( Cb==ok-> C = [A::-Body, incorrect];
C = Cb).
check refutation( (A,B), (Ta,Tb), C ) :check refutation( A, Ta, Ca)( Ca==ok-> check refutation( B, Tb, C );C = Ca).
check refutation( A, Ta, C ) :oracle( A, T )( ge( T, Ta)-> C = ok ; fp( A, T, C ) ).

Figure 8: Prolog implementation of fp
be removed from the model as a cause of strength, is identi ed by the procedure fp .
Figure 8 shows a Prolog implementation of fp. The goal refutation( p(X~ 0; T ), T 0 , Body, Tb )~ T )::- Body 2 P which weakly-derives p(X~ 0; T g) such that T g  T 0 . The goalnds the clause p(X;check refutation( Body, T a, C ) checks each goal of the Body with .
Let us assume that check refutation(qi (X~i0 ; Ti), Ti0, C ) is activated under the condition that qi (X~i0 ; Ti0)
is derived >from P and < qi(X~i0 ; Ti); Ti00 > is in . If Ti00  Ti0 then the cause of strength should be foundin the resolution process of qi (X~i0 ; Ti0). Therefore check refutation calls fp(qi(X~i0 ; Ti), Ti00 , C) recursively.
Otherwise it returns C=ok.
The model P is said to be incomplete, if P derives the truth value f ail to a certain fact whichis contained in . The procedure failp identi es the cause of the incompleteness, which is either an
uncovered goal or an -refuted clause. Figure 9 shows a Prolog implementation of failp. The procedure
failp(p(X~ 0 ; T ), T 0, C) is activated when the model P cannot derive p(X~ 0; T 0 ) and < p(X~ 0; T ); T 0 > is in. If P cannot weakly-derive p(X~ 0 ; T 0 ), it calls ip(p(X~ 0 ; T ), T 0 , C). Otherwise, it calls fp2(p(X~ 0; T ), T 0,
C). The procedure fp2 selects the clause which derives p(X~ 0; f ail) and nds a correct top-level traceof the clause. If the correct top-level trace derives p(X~ 0 ; T g) and T g  T 0 then fp2 returns the clauseas an -refuted clause. Otherwise fp2 calls failp for the body of the clause. The formal de nition ofincompleteness is given in De nition B.7.
3.2.2 Search for a new clause

A candidate clause to be added into the model is generated using the re nement graph which is de nedby re nement operators. The generation process is viewed as a kind of search on a dynamically generated tree. The re nement graph is rooted by a most general clause. Its nodes correspond to candidate

14

failp( (A,B), (Ta,Tb), C ) :smdl( A, fail )-> failp( A, Ta, C );failp( B, Tb, C ).
failp( A, Ta, C ) :not( weakly derive( A, Ta) )-> ip( A, Ta, C );fp2( B, Tb, C ).
fp2( A, Ta, C ) :smdl clause( A, Body ),smdl( Body, fail ),good oracle top( A, Tg, Body, Tb),
( le( Tg, Ta), failp( Body, Tb, C );( gt( Tg, Ta), C = [A::-Body,incorrect] )).

Figure 9: Prolog implementation of failp
clauses and directed arcs C ! C 0 to the re nement operations applied to clauses. Typical examples ofre nement operations include adding a predicate into the body and uni cation of variables. The graphhas the following important characteristic:
If the clause C does not cover a goal A, then any C 0 satisfying C ! C 0 does not cover it either.
This is used for pruning the unnecessary branches, which makes the search ecient.
A re nement graph represents knowledge which enables an ecient search for a clause to be added
into the model. However, it does not have any a priori knowledge of bugs. So, it always tries to nda clause from a xed root, i.e., the most general clause, independently of material. Note here that we
can introduce the concept of bug when we know the material well. Given some typical bugs speci c tothe teaching material under consideration, the search procedure can begin searching from these bugs,
which makes the search very ecient.
3.3 ATMS

This section brie y explains ATMS. Detailed description is given in Appendix C.
The information given by the inference system takes a form of
N1 ; N2 ;1 1 1 ; Nk ) D

which means that the datum D is derived from a set of the data fN1; N2; :::; Nk g. fN1 ; N2 ; :::; Nk g iscalled a justi cation of D .
The data dealt with in the inference system are classi ed into three kinds of data, i.e., premise data,assumed data and derived data. A premise is de ned as a datum that can be true under any context.
An assumed datum is one produced with an assumption that holds without depending on any otherdata. A derived datum is one inferred from other data.
Following each justi cation back from a certain derived datum nally reaches a set of assumptions
and premises. That is to say, the set of assumptions that an individual datum depends on can becalculated. A set of assumptions is called an environment. It is one of the major tasks for ATMS
to record justi cations informed from the inference system and to calculate a consistent environment
where the data can be inferred. When derivation of the contradiction is informed, ATMS calculates
the nogood environment, which is the cause of the contradiction and recorded in ATMS (hereafter
called the nogood record). Every environment included in the nogood record can be regarded as an
inadequate combination of the assumptions. ATMS maintains the consistency of the inference process
by using the nogood record. The inference system selects a new consistent environment, which does
not include the nogood record elements, and continues inference.
A situation in the problem solving process is called a context, which is de ned by the set of the15data that hold in the situation. An environment deriving all the data included in the context is calleda characteristic environment of the context.
When the derivation of an inconsistency is informed, ATMS calculates and records the environmentof ? . The inference system ceases to solve the problem in the contradicted context and transfers to a
new consistent characteristic environment.
With regard to the nodes which have been derived before that time, ATMS determines whether eachnode holds (in ) or does not hold (out ) in the new characteristic environment. Thus a new context is
composed with a set of in nodes.
3.4 Managing consistency to control the model building process

Single world contradictions are formulated in a uni ed architecture in HSMIS by combining SMIS
and ATMS. With the aid of the schematic diagram shown in Figure 5, the overall behavior of thesystem for single world contradictions will be made clear in this subsection. (1) Given student answers(\real oracle"), the Virtual oracle generator generates virtual oracles if necessary and passes them to
ATMS with the real oracles. (2) SMIS informs ATMS of all the inference process that is explained indetail in Appendix D. When a contradiction is informed, ATMS computes the label responsible forthe inconsistency based on the information given up to that point of time and stores it in the nogood
record. (3) SMIS asks CRS to resolve the inconsistency. (4) According to the cause of inconsistency
identi ed, CRS selects a new environment which is consistent by asking ATMS to check its consistency.
(5) ATMS answers the queries by inspecting the nogood record and (6) passes the control to SMIS
together with a new context supported by the new consistent environment.
HSMIS tries to model the student from his behavior during which it automatically asks questions
which contribute to the disambiguation of alternative clause selection and diagnosis. In other words,
HSMIS asks questions regardless of their appropriateness in the sense of tutoring. This requires some
control mechanism of the HSMIS behavior. The following additional mechanisms are introduced toaugment the HSMIS.
Virtual Oracles: Let us discuss the initial model problem. There are two alternative initial models:
one is empty, which means the teacher does not know anything about the student in advance, and theother is complete knowledge (teaching material), which means she assumes that he usually understands
the material very well. Although the former case is reasonable, the system would tend to ask manyquestions to get sucient information about how well he 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 characteristic is very reasonable in real tutoring. The latter is
employed. A serious problem still remains, however. One cannot simply put a clause into the student
model without any justi cation.
The Virtual oracle generator, which generates plausible student answers based on the certainty of
the current student model instead of asking questions, has been devised in order to cope with thisproblem. When a student's behavior is con ned within the scope of his teacher's prediction, she asks
fewer questions by replacing the necessary information with correct answers. This type of oracle iscalled a \virtual oracle." SMIS treats \real oracles" and \virtual oracles" in the same manner, while
ATMS manages their consistency. Detailed formulation of virtual oracle is given in Appendix D.2.1.
When a clause supported by virtual oracles turns out to be no longer in as the inference proceeds,
ATMS withdraws it and backs up to the point which causes the problem.
Meta-Oracles: Students sometimes want to express their knowledge in the form of knowledge insteadof facts. The system sometimes wants to ask the student the reason why he answers a question thatway. The following is an example.
System : Does rice grow in Russia?
Student: Yes, it does.
System : Why do you think rice grows in Russia?
Student: It has wide flat fields and rivers.

In this case, HSMIS can obtain an oracle and a clause as follows.
< grow (rice; russia; T ); true >16

grow(rice, Place) ::flat field(Place),river(Place).

The clause obtained from the student is called a \meta-oracle." The formulation is given in Appendix
D.2.2.
3.5 Assumptions to cope with single world contradictions

This subsection gives the formulation of assumptions to drive the mechanism mentioned in Section
3.4. The nonmonotonic inference process of HSMIS is realized by controlling the status of the assumptions representing various hypothetical decisions which are made during student modeling. Detailed
formulation of the assumptions and the inference process derived from them are explained in Appendix
D.
Given a consistent oracle set ~ , SMIS is able to construct a student model which explains ~ . Thatmeans SMIS is potentially able to cope with all the modeling contradictions in terms of SMDL, if anappropriate ~ is given. In HSMIS, these modeling contradictions are formulated to be controlled by
the following three types of assumption in the framework of ATMS:
uncover(C; O) which represents that an oracle O can not be covered by a certain clause C . It holds
unless cover(C; O) is derived. This type of assumption is used to prune branches in the re nement
graph and to detect that the search turns out a failure.
-consistent(C ) which represents that a clause C is consistent with ~ , the current oracle set. It holds
unless -ref utation(C ) is derived. Such a consistency is checked whenever ~ is changed by themechanism. This type of assumption is used for revising the student model to follow change of~.
general(C ) which represents that any ancestor clauses of C in the re nement graph which are moregeneral than C are not contained in the current model. It holds unless an ancestor clause of C
is added to the model. If an ancestor clause of C is added to the model, the clause C no longer
holds in the model.
In order to cope with two types of student contradictions, [A1] and [A2], which are both classi ed
into the single world contradiction, it is necessary to update the oracle set itself, e.g., to leave unreliable
oracles out of consideration in modeling or to modify truth values of some of the oracles which cause acertain inconsistency. This requirement means that the system should be able to generate the currently
reliable set of oracles ~ , which is considered in model inference, from the whole set of given oracles. The following type of assumption is formulated in addition to the above three types to meet therequirement.
oracle(O) which represents a question and a student's answer to it, i.e., a \real" oracle O. If theassumption oracle(O) is in , oracle O is in ~ . This means the oracle is reliable at present.
A modeling system must be able to realize more appropriate behavior if it copes with nonmonotonicities of a teacher's trust in student's knowledge and asks reasonable numbers of questions in the
didactic sense. Contradiction of trust is formulated by incorporating the following assumption:
trust(C ) which represents that the system trusts the student to have the knowledge that corresponds
to clause C . It is in unless -ref utation(C ) is derived. Virtual oracles are generated basedon this assumption and the oracle that is uni able with C . The number of system questions ishence reduced without losing logical consistency of the modeling process. When this assumption
becomes out , virtual oracles which were derived from it are automatically withdrawn, and thesystem asks the student the facts which had been trusted and have not been asked until then.
SMIS deals with oracles and virtual oracles in the same manner.
3.6 Detection and resolution of contradiction

The contradiction derived in the inference process of HSMIS is classi ed into the following seven types.

17S1) Contradiction of -consistency
S2) Contradiction of cover test
S3) Contradiction of generality
S4) Contradiction of trust
S5) Contradiction of meta-oracleS6) Contradiction of oracleS7) Failure of search
When any of the contradictions is detected, ATMS is informed of it and updates the nogood record.
Among the assumptions which are formulated in HSMIS to cope with single world contradictions,-consistent(C ) , uncover(C; A), general(C ), trust(C ) and metaOracle(C ) are called default assumptions, which means \they are assumed to be in so long as no contrary evidence is found." The
set of these assumptions included in the environment is called a default environment (denoted by De ).
From this, the current environment Ce can be expressed by
Ce = De [ ~Contradictions can be classi ed into (a) ones regarding the default environment and (b) ones regarding the oracle environment (corresponding to ~ ).
(a) The resolution method for contradictions of the default environment can be easily derived fromits de nition.
Suppose that a contradiction is detected since there exist both the -ref utation(C ) and the-consistent(C ) in the current context. As has already been stated, the -consistent(C )can hold so long as there does not exist the refutation for the clause C ,i.e., -ref utation(C ).
Therefore, the inconsistency can be resolved by removing the -consistent(C ) from the default
environment. Similarly, the assumptions, uncover(C; A), trust(C ) and metaOracle(C ) areremoved from the default environment when the contradictory data is found.
(b) CRS generates consistent ~ . The consistency is guaranteed to the extent that it does not include
any contradictions that have been found thus far. In other words, it may contain a contradiction
found in the future. The operations carried out for the generation are:(1) remove an oracle from ,(2) modify the truth value of an oracle in .
CRS searches for a consistent ~ in the ascending order of number of modi cations from . To
improve the eciency and educational validity of selecting the consistent oracle set which has
the minimal modi cations, some domain-independent heuristics are incorporated into the search
procedure: Give priority to correct or recent answers, give priority to the oracles supporting theplausible clause which is supported by relatively many oracles, and so on. Domain-dependent
heuristics may also be introduced.
3.7 Behavior of HSMIS

An example of how HSMIS works is given in Figure 10, in which the description is partially simpli ed
because of space limitation, i.e., the description of teaching material is not correct in the strict sense(for example, the rst argument of grow is omitted). An example of the modeling process for a student
knowledge contradiction is shown in Section 4.
In order to realize the above behavior of HSMIS, at least two kinds of knowledge are required. One
is the knowledge for re nement graph generation. In the above example, for example, the following
knowledge is used for generating three clauses C 1, C 2 and C 3.
declare called(grow(P lace; T ); [temp(P lace; T1 ); soil(P lace; T2 )])This means that the predicates in the second argument, i.e., temp(P lace; T1 ) and soil(P lace; T2), canappear in the body of a clause whose head is grow(P lace; T ). If this form of knowledge including
necessary predicates is prepared, HSMIS can automatically generate a complete set of clauses as amodel of the student.

18

Figure 10: An example of HSMIS modeling process
The other kind is the correct domain knowledge which provides HSMIS with correct answers. In theabove example, the knowledge is used for three purposes, i.e., for generating virtual oracles, managing
the environment, and generating problems.
In the above example, the student model changed two times. The rst change from C 1 to C 2 canbe regarded as corresponding to the nonmonotonicity inherent in the inference process, i.e., C 1 is not
an appropriate hypothesis of the student understanding at that time. Meanwhile, the second change
from C 2 to C 1 corresponds to the nonmonotonicity of student's understanding.

4 Nonmonotonic student modeling in multiple worlds
4.1 Inference process in THEMISThis subsection discusses both the modeling mechanism and the formulation of the modeling process
realized in THEMIS which consists of HSMIS and Multi-World Controller (MWC). MWC uses HSMIS
as a single world modeler capable of resolving single world contradictions. THEMIS is hence able
to represent student knowledge contradictions according to the multi-world logic, maintaining theconsistencies between model and oracles in each world. A formulation of the inference process is given
in detail in Appendix D.
Among student contradictions, the formulation of student knowledge contradictions is more complicated than formulations of the other two. The following two types of assumption are introduced toformulate student knowledge contradictions:belong(P; Wi ) which represents that the student is assumed to understand that problem P belongs
to world Wi.
discriminate(Wi ; Wj ) which represents that the student is assumed to be able to correctly discriminate between the two worlds Wi and Wj .

19

When a correct assumption belong(P; Wi ) is in , the student is expected to be able to correctly apply
a problem solving method , say, Mi , which is in the world Wi of the current model. If he does notdiscriminate between Wi and Wj , however, it can happen that he applies Mj which belongs to Wj
to the problem. A contradiction is derived from the assumptions belong(P; Wi ) which is pre-assumed
and belong(P; Wj ) which is newly assumed to cover his faulty answer. Another contradiction is also
derived from the assumption discriminate(Wi ; Wj ) and the datum indiscriminate(Wi; Wj ) which isderived from assumption belong(P; Wj ). In this case, oracles related to P are transferred from Wi to
Wj together with the belief revision of discriminate(Wi ; Wj ) to be out and the system revises the discrimination conditions which discriminate the two worlds so as to resolve these contradictions. Thus therevised student model represents the student knowledge contradiction caused by his undi erentiation.
Contradictions derived in the inference process of THEMIS are classi ed into the following three
types in addition to the contradictions formulated in HSMIS.
M1) Contradiction of belong
M2) Contradiction of discrimination
M3) Contradiction of model prediction and oracle
All these contradictions handled by MWC are resolved in a similar manner to contradictions of
the default environment, i.e., \the assumptions which were hypothesized in advance and which derived the faulty expectation is denied to be out , when a contradiction is informed." The assumption
belong which has been assumed becomes out in the case of type M1 contradictions. The assumption
discriminate and the assumption belong which has derived an expectation of a student answer also
become out in the case of type M2 and M3, respectively.
4.2 Modeling student knowledge contradictions

The formulation of student knowledge contradictions described earlier works well as a student modelingmethod by utilizing the heuristics which are also mentioned earlier. MWC is incorporated into THEMIS
to control multi-world inference. Concept discrimination trees are given in advance as a part of thedomain dependent knowledge. MWC is given the whole set of worlds which are handled in one course oftutoring, and it manages the status of each discrimination condition in the tree and each set of oracles
that belong to each world. MWC is able to retrieve all the clauses in a certain world which are uni ablewith a certain oracle in the world with the help of ATMS. Model diagnoses and revisions can be doneon the discrimination trees. In each world, the clause level student model is inductively inferred >fromthe oracles belonging to the world. It is realized by modifying the algorithm of the SMDL interpreter,
i.e., a clause C in a certain world W is uni able only with oracles belonging to W . Each clause level
student model can be consistently inferred using such a mechanism.
The construction process of the student model that represents student knowledge contradictions is
as follows:
1. The system assumes a student knowledge contradiction when newly obtained oracles are notsatis ed by any uni able clauses in the corresponding world in the model which are suciently
reliable.
2. The system tests whether the oracles are satis ed by the clauses that exist in another world byvisiting the worlds in turn in order of similarity to the correct world according to the structureof the tree.
3. When a clause explaining the oracle is found in some world, discrimination conditions that contribute to di erentiation of the two worlds are revised as depicted in Figure 3.
4. If no satis able world is found, the system considers the situation as a single world contradiction
and tries to revise the model in the correct world.
Such a decision is made based on the heuristics to detect a student knowledge contradiction mentioned in
Section 2.2. THEMIS calculates the certainty of each clause in its clause (method) level student model sothat it is able to apply the heuristics. The calculation is done by referring to various kinds of information,i.e., number of top-level traces that justify the clause, whether the oracles which consist of each top-leveltrace of the clause are correct answers or not, how old the oracles are, etc (Kono et al, 1993a).

20

IW , the set of instances whose every element originally belongs to a certain conceptual world W ,can be determined by applying CW which is the world predicate of W to I , the whole set of instances inthe domain. Clause level representations and oracles which justify the model are generated and storedin each world individually. Suppose that there are two worlds W1 and W2 which are brothers and thatthey have already obtained and involved oracle sets O~W 1 and O~W 2. Suppose also that clauses M1
and M2 are in W1 and W2, respectively. If M1 , that currently has high certainty, is refuted by theoracle set O~p, which is newly obtained from him, to the problem that naturally belongs to W1 , or if
M1 can not cover a certain goal in O~p, then the system hesitates to dismiss M1 and tries to interpretthe status of his conceptual discrimination as undi erentiated. If M2 satis es O~p , O~p is moved into
W2 and supports M2 there. Both discrimination conditions C1 and C2 , which are world predicatesof W1 and W2 , are revised to be C1 _C2 . If any clauses in any other worlds in the tree except the\another world" do not support O~p, it is assumed that he was thinking in the world that contains naive
buggy knowledge and has solved the problem informally. O~p is moved into the \another world" which
is prepared to cover his unformulated problem solving, if one of the buggy clauses, prepared in theworld in advance, satis es O~p .
In our example, the student correctly answered several questions including Question 1 in the past,so that the student model had the correct clause to get the force which an object in uniformly accelerated motion receives. He made the wrong answer utilizing his naive physical world to Question
3 later. HSMIS receives oracles made from his answer, e.g., oracle(subtract(19.6,0,19.6),true), oracle(subtract(2,0,2),true). The above clause in the world of uniformly accelerated motion does notsatisfy these oracles and derives an answer di erent from that of him. HSMIS recognizes the needfor a new clause whose head is get direction of force to satisfy the oracles. There exists the correctclause, however, which should have been applied to the problem, in the world of uniformly accelerated
motion in the student model. The clause is reliable enough because the student correctly answeredsome questions using the method corresponding to the clause. The student, however, does not apply
the method to the latest question. Therefore, it is unreasonable to assume he solved the problem inthis world.
For this reason, THEMIS does not choose to resolve the inconsistency in the single world. Instead,
it considers the situation as a multi-world contradiction and it searches for the world that alreadycontains the clause which satis es the oracles. If the search fails, THEMIS tests \another world"which represents students' naive problem solving. In this example, the system nds out the clause that
represents his erroneous \motion implies force" misconception prepared in the naive world in advance.
The system revises discrimination conditions that partition the concept of motion into the world of
formulated physics and that of naive physics. It can explain his discrimination status, that he unstably
applies physics formulas and naive knowledge.

4.3 Correcting student knowledge contradictions

By modeling student knowledge contradictions, the system is able to realize very e ective and \real"
Socratic tutoring as follows:
1. Give him a problem such that he tries to solve it in his naive world and fails to get a correct
solution.
2. Remind him of the correct answer to the problem he obtained in Question 1.
3. Point out the inconsistency between the two results.
4. Explain the causes and guide him to build a correct concept.
In this way, he can correctly identify attributes necessary for building the concept, which we callworld predicates, and establish relationships between them. Thus he can appropriately conceptualize
the knowledge in both worlds. Obtaining the student model that represents the student knowledge
contradiction, the system becomes able to generate an e ective tutoring dialogue as in Figure 11.
The mechanism for single world contradictions explained earlier and the framework to handle multiworld contradictions explained in Section 4 are integrated into THEMIS. It gives up constructing a
uni ed consistent model and dares to build a model in multiple worlds, when newly obtained data
deny the reliable current model. The control mechanism guarantees the delity and the accuracy of21

Tutor:Tutor:

Solve this problem. (Give a problem similar to Question 1 again)
The student correctly answers.

You answered in Question 3 that the direction of the force which the sphere receives is upward at
t=1s, because it is still moving upwards then.
If that was correct, why didn't you say that thesphere in Question 1 receives force to the right?
Student: Because it was moving upwards, so it is hardly possible that it continued receiving force downward.
Tutor: The two problems are completely the same, e.g., speed at each time, etc., except for the directionof motion. If direction of force were to be implied from motion, you should have naturally said
that the direction of the force is to the left in Question 1, but you didn't. (You should have``motion implies force'' misconception in your naive physical world. 1 1 1)

Figure 11: A hypothetical example of tutoring behavior using student knowledge contradiction.
the model in each world. Student's incorrect inference methods, such as the use of abduction in his
problem solving, can be formulated as contradictions. However, this topic has been kept for futurework.

5 Discussions
Here some basic issues of comparative student modeling methodologies are discussed.
One cannot model students without de ning a "bug" which is one of the key concepts of student
modeling. The de nition of bugs in turn de nes the search space for student modeling. Bugs arede ned as a mal-function or a mal-structure of the correct knowledge from the computational point ofview. By mal-function and mal-structure, we mean a state in which a component of knowledge does notrealize its function and a state in which the structure of knowledge is incorrect, i.e., some componentis missing or inserted, etc., respectively. >From this point of view, there are three types of model whichmodel:
1. what component of the correct knowledge is incorrect (mal-function-1)
2. how the component is incorrect (mal-function-2)
3. how the structure of the knowledge is incorrect (mal-structure)
Type 2 methods not only identify what component of the correct knowledge is incorrect in the student's
head but also model how it is incorrect in a limited way, e.g., using fault models of each component. It
cannot model, however, why the function is so incorrect. Needless to say, type 3 is the most powerfultype of modeling, since it models what, how, and why the component is incorrect by modeling theincorrect structure of the knowledge.
Although student modeling is generally viewed as an inductive process in which a representation
explaining observed data is built, we can nd another view, i.e., as the analysis of the expertise modelusing the observed data (Hoppe, 1994). Modeling methods which obtain information of the student's
understanding state by analyzing the correct knowledge based on the student behavior are called\analytic methods" here. A student model does not have to explain all the behavior of the student.
Considering that its function is to give necessary and sucient information to the tutoring module,
analytic methods work very well for many types of tutoring modules. Typical examples of analytic
methods are the overlay model (Carr et al, 1977), the logic programming method (Hoppe, 1994), andmodel-based cognitive diagnosis (Self, 1993a). This type of methods does not model mal-structure,
while inductive methods try to represent it. Typical examples of inductive methods are the buggy model(Burton, 1982), perturbation methods (Otsuki et al, 1985), ACM (Langley et al, 1984), and THEMIS.
Table 4 summarizes the characteristics of the methods discussed in this section.
Analytic methods

The Overlay model (Carr et al, 1977) is relatively easily used to control the modeling processes.
That is why the overlay model has been used in many ITSs. Since it cannot represent the student's
incorrect knowledge, the performance of overlay-model-based ITSs is limited.
Hoppe (1991; 1994) proposes a method to analyze the correct knowledge represented as a Prolog
program by executing the program with the student answer as a goal. When the student answer is22

Table 4: Evaluation of student models
System name
Overlay(Hoppe, 1994)(Self, 1993a)
IDEBUGGY
Perturbation
ACM/DPFTHEMIS

Analytic/
inductive
analytic
analytic
analytic
inductive
inductive
inductive
inductive

Malfunction-1
yes
yes
yes
yes
yes
yes
yes

Malfunction-2
no
yes
yes
yes
yes
yes
yes

Malstructure
no
no
no
yes
yes
yes
yes

Inconsistencynonono
partlynopartlyyes

Theoreticalfoundation
low
middlehighlowlow
middlehigh

Question
automatically
NA
NA
yes
yes
no
no
yes

incorrect, the execution fails if it is interpreted by a Prolog interpreter. In order to recover the execution
failure, he introduces a fail-safe meta-interpreter of Prolog and detects uncovered goals which potentiallycorrespond to the student's bug. Many uncovered goals are usually detected, so he employs the EBG(Explanation-Based Generalization) technique to formulate rules called error patterns which are used
to select the goals corresponding to the plausible bug. The search space of this method is small, since
it is restricted to the computation tree of the correct knowledge. This method requires pre-de ned
classi cation rules which roughly correspond to bug rules, though they are more abstract than bug
rules. It represents bugs of type mal-function-2. This method does not su er from the inconsistency
problem, because it builds a model from one datum.
Self (1993a) gives a characterization of student modeling as model-based cognitive diagnosis, making
an application of GDE (deKleer et al, 1987). GDE is essentially based on an exhaustive search overthe search space de ned as a set of all the combinations of possible faulty components with the aid ofATMS. The search mechanism, in principle, is hence to check what set of components are faulty and to
determine a minimum set of faulty components. Another advantage of GDE is its automatic question
generation mechanism for disambiguation of the fault hypotheses. It represents only mal-function-1,
although it does not require any bug library. Just a small extension, i.e., the introduction of fault
modes into each component, enables it to cover type mal-function-2 as Self indicates. It is sensitive toinconsistent data. The theoretical foundation becomes more rm and sound in this order, though there
is a large gap between the overlay model and Hoppe's method.
Inductive methods

IDEBUGGY (Burton, 1982) has many modular chunks of buggy procedures. It has the capability
to cope with the noise problem, however, it is not complete. Its searching strategies depend on theassumption that each individual buggy procedure can be extracted from a combined buggy procedure.
The burden of cataloging bugs is still left.
Bugs are viewed as variants of correct knowledge. They can be generated by applying perturbation
operators to correct procedures. Perturbation methods are based on this idea. Takeuchi and Otsuki(1987) utilize this type of method in their system BOOK (Otsuki et al, 1985) in which two types of
perturbation operators (domain-dependent and domain-independent ones) are introduced to augment
the modeling power. The search space of this method is dependent on the complexity of the perturbation
operators used, which is not usually so large. The method has no rm theoretical foundation for it but
does not su er from inconsistency of the data, since it builds a model from one observation.
Both ACM (Langley et al, 1984) and the authors' method THEMIS/HSMIS are based on the ideathat student modeling is viewed as inductive learning from a set of examples. These two methods arealmost equivalent in representation power of the student model. They can model not only mal-functions
but mal-structures in terms of pre-de ned primitives. Both methods act as domain-independent engines
and their capabilities contain those of both the overlay and buggy methods. Besides, both of them cancope with noisy data. In general, it seems that the method of inference in ACM is not so sophisticatedas that of HSMIS.
The major di erence is their searching and diagnostic strategies for ascertaining what part of themodel con icts with the student. HSMIS can prune the search space for new clauses in a re nement
graph, although ACM originally made a blind search of all its search space. To embody ecient
searching, Langley et al (1990) have been developing DPF (Dynamic Path Finder).
HSMIS can incrementally revise the model using newly obtained data. Although the path- nding23

algorithm is formulated by DPF, the rule- nding process is not formally de ned. HSMIS can distinguish between noisy data and bug migration (Kono et al, 1993a; Ikeda et al, 1993), while ACM cannot
currently (Langley et al, 1990). HSMIS asks questions which are logically required in consideration of
educational appropriateness, while ACM does not.
Other types of methods

Huang (1993) proposes a logic to capture the student's inconsistent knowledge. Surprisingly, only his
study, apart from THEMIS, has so far been carried out on modeling student knowledge contradictions.
Although it is well-de ned in terms of propositional calculus, it would be dicult to extend it to deal
with rst order predicate calculus.
The role of a student model is to provide a tutoring module with information necessary for generating
adaptive behavior. There is no need to produce precise information more than required. PROTO-TEG(Dillenbourg, 1989) is an interesting ITS based on this idea. It does not generate any structured
information that can be regarded as a student model, but generates heuristics to produce tutoring
behavior directly by incorporating one of the inductive learning theories, LEX (Mitchel et al, 1984). It
is successful in handling its simple didactic strategies.
Considering the functions the student model should perform and the intractability of modeling,
Ohlsson (1993) proposes a new approach to student modeling called constraint-based in which domain
knowledge is represented by a set of constraints and the student model is represented by constraint
violation. The idea seems good, since it can avoid many of the diculties which current modelingtechnologies are su ering from. One has to identify, however, sets of constraints which cover all theinformation the tutoring module requires which is not an easy task.

6 Concluding remarks
This paper has presented a comprehensive student modeling methodology and its use in an ITS. Contradictions we have to cope with during modeling students are rst de ned. As a result, we obtained
four types of contradiction, including contradictory knowledge possessed by students. The modelingsystem of such students has to model undi erentiated concepts and inconsistency as it is. A sophisticated control mechanism to deal with both single world and multi-world contradictions for THEMIS
has been developed.
Finally, THEMIS has been compared with other modeling systems from various viewpoints todemonstrate that it is a well-de ned and generic student modeling algorithm, which can build a student
model of high representation power. THEMIS has been implemented in Common-ESP(Extended Selfcontained Prolog) (AIR, 1990), and HSMIS is embedded in FITS, Framework for ITS. Two ITSs havebeen built using FITS, one on geography and the other on chemical reactions (Mizoguchi et al, 1987;
Mizoguchi et al, 1991; Ikeda et al, 1994).
References
AI Language Research Institute (ed). (1990). CESP Language Guide, 5-1-1, Ohuna, Kamakura, Kanagawa
247, Japan.
Burton, R. R. (1982). Diagnosing bugs in a simple procedural skill, In Sleeman, D. & Brown, J.S. (eds.),
Intelligent Tutoring Systems, Academic Press, London.
Carr, B. & Goldstein, I. (1977). Overlays:A theory of modeling for computer aided instruction, MIT AI Memo
406.
Clement, J. (1982). Students' preconceptions in introductory mechanics, American Journal of Physics, 50,
66{71.
de Kleer, J. (1986). An assumption-based TMS, Arti cial Intelligence, 28, 127{162.
de Kleer, J. & Williams, B. C. (1987). Diagnosing multiple faults, Arti cial Intelligence, 32, 97{130.
Dillenbourg, P. (1989). Designing a self-improving tutor: PROTO-TEG, Instructional Science, 18, 193{216.
Dillenbourg, P. & Self, J. (1992). A framework for learner modelling, Interactive Learning Environments, 2(2),111{137.
Hoppe, H. U. (1991). An analysis of EBG and its relation to partial evaluation: lessons learned, Arbeitspapiereder GMD.
Hoppe, H. U. (1994). Deductive error diagnosis and inductive error generation for intelligent tutoring systems,
Journal of Arti cial Intelligence in Education, (to appear).

24

Huang, X., McCalla, G. I., Greer, J. E. & Neufeld, E. (1991a). Revising deductive knowledge and stereotypicalknowledge in a student model, User Modeling and User-Adapted Interaction, 1, 87{115.
Huang, X., McCalla, G.I. & Neufeld, E. (1991b). Using attention in belief revision. In Proc. AAAI-91, 275{280.
Huang, X. (1993). Inconsistent beliefs, attention, and student modeling, Journal of Arti cial Intelligence in
Education, 3(4), 417{428.
Ikeda, M., Mizoguchi, R. & Kakusho, O. (1988). A hypothetical model inference system, Trans. of IEICE Japan, J71-D, 1761{1771 (in Japanese).
Ikeda, M., Mizoguchi, R. & Kakusho, O. (1989). Student model description language SMDL and student model
inference system SMIS, Trans. of IEICE Japan, J72-D-II, 112{120 (in Japanese).
Ikeda, M., Kono, Y. & Mizoguchi, R. (1993). Nonmonotonic model inference -A formalization of student
modeling-, In Proc. IJCAI'93, Chambery, France, 467-473.
Ikeda, M. & Mizoguchi, R. (1994). FITS: A framework for ITS { A computational model of tutoring {, Journalof Arti cial Intelligence in Education, 5, (to appear).
Kawai, K., Mizoguchi, R., Kakusho, O. & Toyoda, J. (1987). A framework for ICAI system based on inductive
inference and logic programming, New Generation Computing, 5(1), 115{129.
Kono, Y., Ikeda, M. & Mizoguchi, R. (1992). To contradict is human -Student modeling of inconsistency-, In
Frasson, C., et al. (eds.), Intelligent Tutoring Systems, ITS'92 Proceedings, 451{458, Springer-Verlag.
Kono, Y., Tokimori, T., Ikeda, M., Nomura, Y. & Mizoguchi, R. (1993a). A student model building method
based on formalization of nonmonotonicity, Journal of Japanese Society for Arti cial Intelligence, 8(4),488{498, (in Japanese).
Kono, Y., Ikeda, M. & Mizoguchi, R. (1993b). A modeling method for students with contradictions, In Proc.
AI-ED 93, Edinburgh, Scotland, 481{488.
Kono, Y., Ikeda, M. & Mizoguchi, R. (1994). An inductive student modeling method which deals with student
contradictions, IEICE Trans. on Information and Systems, E77-D(1), 39-48.
Langley, P. & Ohlsson, S. (1984). Automated cognitive modeling, In Proc. AAAI-84, 193{197.
Langley, P., Wogulis, J. & Ohlsson, S. (1990). Rules and principles in cognitive diagnosis, In Frederiksen, N.,et al. (eds.), Diagnostic Monitoring of Skill and Knowledge Acquisition, 217{250, Lawrence Erlbaum.
Mitchel, T., Utgo , P. & Benerji, R. (1984). Learning by experimentation: Acquiring and re ning problem
solving heuristics, In Michalski, R., et al. (eds.), Machine Learning, Springer-Verlag.
Mizoguchi, R., Ikeda, M. & Kakusho, O. (1987). An innovative framework for intelligent tutoring systems, In
Proc. IFIP TC3 Working Conference on AI Tools in Education, 105{120, Fascati, Italy.
Mizoguchi, R. & Ikeda, M. (1991). A generic framework for ITS and its evaluation, In Lewis, R. & Otsuki, S.
(eds.), Advanced Research on Computers in Education, 63{72, North-Holland.
Ohlsson, S. (1993). Constraint-based student modeling, Journal of Arti cial Intelligence in Education, 3(4),429{447.
Otsuki, S. & Takeuchi, A. (1985). Intelligent CAI system based on teaching strategy and learner model, In
Proc. WCCE 85, 463{468.
Self, J. (1988). Bypassing the intractable problem of student modelling, In Proc. ITS'88, 18{24, Montreal,
Canada.
Self, J. (1993a). Model-based cognitive diagnosis, User Modeling and User-Adapted Interaction, 3, 89{106.
Self, J. (1993b). Formal approaches to student modeling, In McCalla, G.I. & Greer, J. (eds.), Student Modelling,
Springer-Verlag.
Shapiro, E. Y. (1981). Inductive Inference of Theories from Facts, Yale University Research Report 192.
Shapiro, E. Y. (1982). Algorithmic Program Debugging, MIT Press.
Stevens, A. L., & Collins, A. (1977). The goal structure of a Socratic tutor, Proc. National ACM Conference,
256{263.
Takeuchi, A. & Otsuki, S. (1987). Formation of learner model by perturbation method and teaching knowledge,
Trans. Information Processing Society of Japan, 28(1), 54{63, (in Japanese).
Wenger, E. (1987). Arti cial Intelligence and Tutoring Systems, Morgan Kaufmann Publishers.
Woolf, B. P. & Murray, T. (1993). Using machine learning to advise a student model, Journal of Arti cialIntelligence in Education, 3(4), 401{416.

Acknowledgments
The authors would like to thank Takeo Tokimori for his contribution to this work. The authors are
grateful to Geo ry Webb for his comment which motivated the research on student contradictions.
The authors are also thankful to Heinz Ulrich Hoppe for his valuable comments. The authors greatly
appreciate the reviewers' precise and valuable comments. This work is supported in part by Grant-in
Aid for Scienti c Research on Priority Areas of the Ministry of Education, Science and Culture of Japan
under Grant: (No. 03245106).

25

Appendix
A Formal de nition of execution of SMDL program
The predicate of SMDL is of the form p(X1 ; X2 ; 1 1 1 ; 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 ; 1 1 1 ; Xm , isabbreviated as X~ . T is a truth valuable or one of four truth values.
The clause of SMDL is of the form: H ::-B1 ; B2 ; 1 1 1 ; Bn ; n  0, where H; Bi (1  i  n) are
predicates. In the case of n = 0, it is called a fact. The SMDL program P is a nite set of clauses.
~ T )::-q1(X~1 ; T1);
[De nition A.1 ] When a goal G = p(X~ 0 ; T 0 ) is given and there exist the clause C = p(X;
0
0
~
~
~
1 1 1 ; qk (Xk ; Tk ) 2 P and the substitution 0 such that p(X ; T ) = p(X; T )0 , a new goal G0 =fq1(X~1 ; T1); 1 1 1 ; qk (X~k ; Tk )g is resolved from the goal G and the clause C with . When k  1,
 = fT =(T1 ^ 1 1 1 ^Tk )g[ 0 . This operation is called weak resolution and denoted by a triple < G; ; C >.
G0 1 1 1 1 l01 is weakly-resolved from P , if there exists a sequence of the weak resolution: < G; 0 ; C0 >; < G1 ; 1 ; C1 >; 1 1 1 ; < ; l ; Cl > , where Gi is a goal weakly-derived from Gi01 and Ci01 with i01 ,Ci 2 P (0  i  l 0 1): 2[De nition A.2 ] For a given goal G = p(X~ 0 ; T 0 ), if there exist a maximal set of clauses S such that~i ; T )::-qi1(X~i1; Ti1 ); 1 1 1 ; qin (X~in ; Tin ) 2 P , p(X~ 0 ; T 0) = p(X~i ; Ti)i ; 1  i  m
S = fCi j Ci = p(Xand the most general uni er 0 of fp(X~ 0)g [ fp(X~i )j1  i  mg then a new goal G0 as shown below isresolved from G and S with 0 .
~ik ; Tik )j1  i  m; 1  k  ni g 0 ; where
G0 = fqik (X0 m00 = f(Ti = ^n
k=1 Tik )j1  i  mg [ fT =(_i=1 Ti )g [  :This operation is called strong resolution and denoted by a triple  G; 0 ; S . G0 ; 1 ; 1 1 1 ; l01 is
said to be strongly-resolved from P , if there exists a sequence of the strong resolution operations asshown below,:  G; 0 ; S0 ;  G1 ; 1; S1 ; 1 1 1 ;  ; l ; Sl , where Gi is a goal strongly-derived
from Gi01 and S with i01 , and Sr  P (0  r  l 0 1): 2[De nition A.3 ] When a goal G = p(X~ 0 ; T 0 ) and a SMDL program P are given, the result of
resolution is de ned as follows. (1) p(X~ 0 ; true) is derived from P i it is weakly-derived from P . (2)~ 0; f alse) is derived from P i it is strongly-derived from P . (3) p(X~ 0; unknown) is derived fromp( X
~ 0 ; f ail) is derived from P . 2
P i it is strongly-derived from P . (4) Otherwise, p(X
i

i

i

i

B Formal de nition of terms for SMIS
[De nition B.1 ] An oracle is of the form < p(X~ 0 ; T ); T 0 >; where X~ 0 is a sequence of ground terms,
T is a truth variable and T 0 2 f true; f alse; unknown g . 2~ T )::-q1(X~1 ; T1); q2 (X~2; T2 ); 1 1 1 ; qk (X~k ; Tk ) 2 P is said to[De nition B.2 ] The clause C = p(X;00~coverVp(X ; T ), when there exist  such that C = p(X~ 0; T 0)::-q1 (X~10 ; T10 ); q2(X~20 ; T20 ); 1 1 1 ; qk (X~k0 ; Tk0 ),k~ 0; T ); T 0 >g [ f< qi(X~i0; Ti ); Ti0 > j1  i  kg  . The q1 (X~10 ; T10 ); 1 1 1 ;T 0 ＝ i=1 Ti0 and f< p(X00~k ; Tk ) is called a top-level trace of C for p(X~ 0; T 0). 2
qk ( X[De nition B.3 ] The model P is said to be too weak, if there exists an oracle < p(X~ 0 ; T ); T 0 > and~ 0; T 0) is not weakly-derived from the current model P . 2p( X[De nition B.4 ] T1  T2 i

2_

T1 = T1 T2 ,where T1 ; T2 2 ftrue; f alse; unknowng and T1 6= T2 .

[De nition B.5 ] Assume that < p(X~ 0 ; T ); T 0 >2 and T 0 2 funknown; f alseg. The model P issaid to be too strong if p(X~ 0 ; T g) such that T g  T 0 is weakly-derived from P . 2

26

~ T )::-q1 (X~1 ; T1 ); 1 1 1 ; qk (X~k ; Tk ) is said to be -refuted, if[De nition B.6 ] The clause C = p(X;V
00there exist < p(X~ ; T ); T >2 and f< qi(X~i0; Ti ); Ti0 > j1  i  kg  , where T 0  ki01 Ti0.
~ T 0 )::-q1 (X~10 ; T10 ); 1 1 1 ; qk (X~k0 ; Tk0 ) is called -refutation for C . 2
p(X;[De nition B.7 ] The model P is said to be incomplete if < p(X~ 0 ; T ); T 0 >2 and p(X~ 0 ; f ail) is

derived from P 2

C ATMS
C.1 Data structure of ATMS

ATMS records a datum in the following form,f< D; E1 ; E2 ;1 1 1 ; Ek g; fJ1 ; J2 ; 1 1 1 ; Jm g >where D is the datum used in the reasoning system. Ei is an environment where D is derived and theset fEi j1  i  kg is called a label of D. Ji is a justi cation informed of by the reasoning system. The
data recorded in this form is called an ATMS node, which is classi ed into the 3 type, i.e. a premisenode, an assumed node, and a derived node.
The premise node includes an empty environment in the label: < D; ffg; 1 1 1g; f1 1 1g >. The assumed
node has the same set composed of a single identi er as a label and justi cation: < D; ffaigg; ffaig; 1 1 1g >,where ai is a identi er of assumption ( in this paper, the identi er of the assumption will be expressedwith the suxed letter a). Nodes except premise nodes and assumption nodes are derived nodes. ATMS
updates the labels of the individual nodes, based on the justi cations informed from the reasoning system.
C.2 Detection and resolution of contradiction

A situation in the problem solving process is called a context, which is de ned with a set of data holdon the situation. An environment deriving all the data included in the context is called a characteristic
environment of the context.
When the contradicted data D1 ; D2 ; :::; Dn are detected in a context, the reasoning system informs
it to ATMS in the following form.
D1 ; D2 ;1 1 1 ; Dn )?

When derivation of inconsistency is informed, ATMS calculates and records the label of ? . The
reasoning system ceases to solve the problem in the contradicted context and transfer to a new consistentcharacteristic environment.
With regard to the nodes that have been derived until that time, ATMS determines whether thenodes holds (in ) or does not hold (out ) in the new characteristic environment in accordance with theconditions shown below. Thus a new context is composed with a set of in nodes.
[Condition 1] Let the label of the node n be L and the characteristic environment be Ce.
if

9 E (E 2 L and E  Ce)
thenstatus of n := inelse
status of n := out

2

D Formulation of the inference process of THEMIS
D.1 Description of model inference process of SMIS

~ T ) ::-q1 (X~1 ; T1 ); 1 1 1 ; qk (X~k ; Tk ) to a model can
Conditions for HSMIS to add a new clause C = p(X;be described as shown below.
if cond1: (< p(X~ 0 ; T ); T 0 >2 ~ ) andcond2: (C is -consistent ) andcond3: (C covers p(X~ 0 ; T 0) ) andcond4: (C is the most general clause )

27

then

( add C to the model )The conditions, i.e. cond1 through cond4, are described as follows.
cond1: To cope with nonmonotonicity of student's answers, the oracle is dealt with as the following
assumed node of ATMS.
~ 0 ; T ); T 0); ffaigg; ffaigg > 3< oracle(p(Xcond2: The -consistency, which means there is no refutation for C , is also dealt with as the assumption
node as shown below.
< -consistent(C ); ffai gg; ffai gg >cond3: The condition means that C has a correct top-level trace for p(X~ 0 ; T 0 ) in ~ . HSMIS informs
ATMS of its existence in the following form.
9
oracle(p(X~ 0 ; T ); T 0 )>=oracle(q1 (X~ 10 ; T1 ); T10 ) >~ T 0 ))
) cover(C; p(X;
..
>
.
>
;
oracle(qk (X~ k0 ; Tk ); Tk0 )V
where T 0 = ki=1 Ti0 and (q1 (X~1 ; T1); 1 1 1 ; qk (X~k ; Tk )) is a correct top-level trace of the clause C for~ 0; T 0).
p( XATMS produces a node in the following form.
~ 0 ; T ); T 0 );< cover (C; A0 ); f1 1 1g; fforacle(p(Xoracle(q1 (X~ 1 ; T1 ); T10 ); 1 1 1 ; oracle(qk (X~ k ; Tk ); Tk0 )gg >cond4: When C is added to the model, it has to be guaranteed that its ancestor clause in the re nement
graph, which is more general than C , does not exist in the current model. However, an ancestor clausemay 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.
< general(C ); ffai gg; ffai gg >Addition of C to the model is informed ATMS in a style as shown below.
9
oracle(p(X~ 0 ; T ); T 0 ) >>-consistent(C ) = ) model(C )general(C )>~ 0 ; T 0 )) ;cover (C; p(XATMS generates the following ATMS node based on the justi cation.

f1 1 1g;
fforacle(p(X~ 0 ; T ); T 0); -consistent(C ); general(C ); cover(C; p(X~ 0 ; T 0 ))g >< model(C );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 identi ed by the SMDS, it is informed ATMS in the followingform.
9
oracle(p(X~ 0 ; T ); T 0 ) >>oracle(q1 (X~ 10 ; T1 ); T10 ) =) -ref utation(C ))
..
>
>
.
>
;
oracle(qk (X~ k0 ; Tk ); Tk0 )where p(X~ 0; T 0 )::-q1 (X~10 ; T10 ); 1 1 1 ; qk (X~k0 ; Tk0 ) is a refutation for C .
ATMS produces the following ATMS node.
3 An ATMS node is a triple < D; L; J >, where D is the datum used in the reasoning system, L is a label, which isa set of environment the datum holds and J is a set of justi cations. An assumed node has the same set composed of asingle identi er as a label and a justi cation( in this paper, the identi er of the assumption will be expressed with ai ).

28

<-ref utation(C ); f1 1 1g;
fforacle(p(X~ 0 ; T ); T 0); oracle(q1 (X~10 ; T1 ) ; T10 ); 1 1 1 ; oracle(qk (X~k0 ; Tk ); Tk0 )gg >When it is found that C 0 does not cover p(X~ 0 ; T 0 ), HSMIS informs ATMS of it as an assumption.
~ 0; T 0)); ffaigg; ffaigg >< uncover(C 0 ; p(XD.2 Controlling mechanisms of the modeling process
D.2.1 Virtual Oracles~ T )::-q1(X~1 ; T1); 1 1 1 ; qk (X~k ; Tk ) which is either correct knowledge or
Let C be an SMDL clause p(X;plausible buggy knowledge in the teaching material. When the student makes an answer p(X~ 0 ; T 0 ) forthe head of C and C is supported by p(X~ 0 ; T 0 ) and a set of correct answers concerning C , ATMS isinformed of an assumption trust(C ), which means \C is reliable." When trust(C) is in the current
environment, Virtual oracle generator generates a set of virtual oracles, that is, f< q1 (X~10 ; T1 ); T10 >~k0 ; Tk ); Tk0 >g. The virtual oracles together with p(X~ 0 ; T 0) construct a correct top-level; 1 1 1 ; < qk (Xtrace of C and are correct answers of the teaching material. For each virtual oracle < qi (X~i0 ; Ti); Ti0 >,ATMS is informed its generation according to the following justi cation:trust(C )0~0oracle(p(X~ 0 ; T ); T 0 ) ) v oracle(qi (Xi ; Ti ); Ti ))SMIS treats oracles and v oracles in the same manner.
D.2.2 Meta-Oracles

When the clause C is added to the model based on a \meta-oracle", HSMIS informs ATMS of thefollowing justi cation.
9
metaOracle(C; yes) =-consistent(C ) ; ) model(C )general(C )Similarly, when the clause C is removed from the model based on a \meta-oracle", HSMIS informs
ATMS of the following justi cation.
metaOracle(C; no) ) -refutation(C )The meta-oracle is dealt with as the following assumption node of ATMS.
< metaOracle(C; V ); ffai gg; ffai gg >D.3 Formulation for multi-world model inference

Here explains the extended formulation of modeling process in THEMIS.
A set of instantiations for the input arguments of the top level goal is called a problem. When thesystem assumes that the student understands that a problem P~ belongs to a certain world W1 , ATMS
is informed of the following assumption:< belong(P~ ; W1 ); ffai gg; ffai gg >A clause which is added to the model should be dealt with separately in each world. Thus, each
ATMS node \model" has an
9 additional justi ed assumption \belong" in9its each justi cation.
oracle(p(X~ 0 ; T ); T 0 ) >>metaOracle(C; yes) >>-consistent(C ) >==consistent(C)
general(C ))model(C; W1 )) model(C; W1 )general(C )>>>>belong(P~ ; W1 );>belong(P~ ; W1 )~ 0; T 0)) ;cover(C; p(XWhen it is found that the student applied clauses that belong to W2 to P~ which should havebeen solved in W1 , ATMS is informed of it and it generates an assumption belong(P~ ; W2 ), and further
ATMS is informed of that the student does not yet discriminate between W1 and W2 with the following
justi cation.

29

belong(P~ ; W2 ) ) indiscriminate(W1 ; W2 )It is assumed in advance that the student correctly discriminates a certain pair of worlds:< discriminate(W1 ; W2 ); ffai gg; ffai gg >Assume that the system is going to give the student a problem P~ that belongs to the world W1 . If
discriminate(W1 ; W2 ) is in, The student is expected to solve P~ in W1 and ATMS is informed of it in
the following form.

belong(P~ ; W1 )~discriminate(W1 ; W2 ) ) solveIn(P ; W1 )When an ATMS node solveIn(P~ ; W1 ) is derived and is in , and a reliable clause C in the model
which belongs to W1 is uni able with P~ , the system predicts student's answer, i.e., an oracle, andATMS node modelP rediction(P~0) is derived in the following form.

solveIn(P~ ; W1 )) modelP rediction(P~0 )model(C; W1 )D.4 Detection of contradiction

The contradiction derived in the inference process of HSMIS is classi ed into the following ten types.
S1) Contradiction of -consistency: When a refutation for the clause, whose correctness has been
assumed, is detected due to appearance of new oracles, the contradiction is detected by thefollowing rule.
-consistent(C ) & -ref utation(C ) ) ?
S2) Contradiction of cover test: When a correct top level trace is found for the clause due to appearance of new oracles, the contradiction is detected by the following rule.
uncover(C; A) & cover(C; A) ) ?
S3) Contradiction of generality: When both of clauses C and C 0 , which suces the relation C ! C 0 ,are in the current model, the inconsistency is detected by the following rule.
general(C 0 ) & model(C ) ) ?
S4) Contradiction of trust: trust(C ) & -ref utation(C ) ) ?
S5) Contradiction of meta-oracle: metaOracle(C; yes) & -ref utation(C ) ) ?
S6) Contradiction of oracle: When < A; T1 > 2 ~ , < A; T2 > 2 ~ and T1 6= T2, the oracle environment is evidently inconsistent. The inconsistency detecting rule is as follow.
oracle(A; T10 ) & oracle(A; T20 ) & T10 6= T20 ) ?
S7) Failure of search: When search for a clause to cover an uncovered goal turns out a failure, thefailure is dealt with as contradiction. For each clause Ci (1  i  m) searched for to cover0< A; T 0 >: &m
i=1 ( uncover(Ci ; A ) or -ref utation(Ci )) ) ?
M1) Contradiction of belong: belong(P~ ; W1 ) & belong(P~ ; W2 ) & W1 6= W2 ) ?
M2) Contradiction of discrimination: discriminate(W1 ; W2 ) & indiscriminate(W1 ; W2 ) ) ?
M3) Contradiction of model prediction and oracle: oracle(P~0 ) & modelP rediction(P~0 ) & P~0 6= P~0 )?

When any types of the contradiction is detected, ATMS is informed of it and updates the nogood
record.

30