Macroplanning with a Cognitive Architecture 
for the Adaptive Explanation of Proofs 
Armin Fiedler 
FB Informatik, Universitiit des Sa~rlandes 
Postfach 15 11 50, D-66041 Saarbr/icken, Germany 
afiedler~cs, uni-sb, de 
Abstract 
In order to generate high quality explanations in technical or mathematical domains, the 
presentation must be adapted to the knowledge of the intended audience. Current proof pre- 
sentation systems only communicate proofs on a fixed degree of abstraction independently of 
the addressee's knowledge. 
in this paper that describes ongoing research, we propose an architecture for an interactive 
proof explanation system, called P. rex. Based on the theory of human cognition AcT-R, its 
dialog planner exploits a cognitive model, in which both the user's knowledge and his cognitive 
processes are modeled. By this means, his cognitive states are traced during the explanation. 
The explicit representation of the user's cognitive states in AcT-R allows the dialog planner to 
choose a degree of abstraction tailored to the user for each proof step to be explained. 
1 Introduction 
A )erson who explains to another person a technical device or a logical line of reasoning adapts 
his explanations to the addressee's knowledge. A computer program designed to take over the 
explaining part should also adopt this principle. 
Assorted systems take into account the intended audience's knowledge in the generation of expla- 
nations (see e.g. \[Cawsey, 1990, Paris, 1991, Wahlster et al., 1993\]). Most of them adapt to the ad- 
dressee by choosing between different discourse strategies: Since proofs areinherently rich in infer - 
ences, their explanation must also consider which inferences the audience can make \[Hora~ek, 1997, 
Zukerman and McConachy, 1993\]. However, because of the constraints of the human memory, 
inferences are not chainable without costs. The explicit representation of the addressee's cognitive 
states proves to be useful in choosing the information to convey \[Walker and Rambow, 1994\]. 
While a mathematician communicates a proof on a level of abstraction that is tailored to the au- 
dience, state-of-the-art proof presentation systems such as PROVERB \[Huang and Fiedler, 1997\] 
verbalize proofs in a nearly textbook'like style on a fixed degree of abstraction given by the initial 
representatio n of the proof. Nevertheless, PROVERB is not restricted to the presentation on a 
certain level of abstraction. Adaptation to the reader's knowledge may still take place by providing 
the appropriate level of abstraction in the initial representation of the proof. 
Drawing on results from cognitive science, we are Currently developing an interactive proof 
explanation system~ called P. rez (for proof explainer). In this paper, we propose an architecture 
for its dialog planner based on the theory of human cognition AcT-R \[Anderson, 1993\]. The 
latter explicitly represents the addressee's knowledge in a declarative memory and his cognitive 
88 
! 
! 
!| 
! 
i| 
skills in procedural production rules. This cognitive model enables the dialog planner to trace the 
addressee's cognitive states during the explanation. Hence, it can choose for each proof step as an 
appropriate explanation its most abstract justification known by the addressee. 
The architecture of P. rex, which is sketched in Section 3, is designed to allow for multimodal 
generation. The dialog planner is described in detail in Section 4. Since it is necessary to know 
some of the concepts in ACT-R to understand the macroplanning process, the cognitive architecture 
is •first introduced in the next section. 
2 AcT-R: A Cognitive Architecture 
In cognitive science, there is a consensus that production systems are an adequate framework to_ 
describe the functionality of the cognitive apparatus. Production systems that model human cogni- 
tion are called cognitive architectures. In this section We describe the •cognitive architecture ACTrR 1 .... 
\[Anderson, 1993\], which is well suited for user adaptive explanation generation because of its con- 
flict resolution mechanism. Further examples for cognitive architectures are SOAR \[Newell, 1990\] 
and EPIC \[Meyer and Kieras, 1997\]. 
AcT-R has two types of knowledge bases, or memories, to store permanent~ knowledge in: 
declarative and procedural representations of knowledge are explicitly separated into the declarative 
memory and the procedural production rule base, but are intimately connected. 
Procedural knowledge is represented in production rules (or simply:productions) xvhose con- 
ditions and actions are defined in terms of declarative structures. A production can only apply, 
if its conditions are satisfied by the knowledge currently available in the declarative memory. An 
item in the declarative memory is annotated with an activation that influences its retrieval. The 
application of a production modifies the declarative memory, or it results in an observable event. 
The set of applicable productions is called the conflict set. A conflict resolution heuristic derived 
from a rational analysis of human cognition determines which production in the conflict set will 
eventually be applied. 
In order to allow for a goal-oriented behavior of the system, ACT-R manages goals in a goal 
stack. The current goal is that on the top of the stack. Only productions that match the current 
goal are applicable. 
2.1 Declarative Knowledge 
Declarative knowledge is represented in terms of chunks in the declar- :fe.atFsubsetG 
ative memory. On the right is an example for a chunk encoding the ±sa subset-fact 
fact that F C_ G, where subset-fact is a concept and F and G are setl F 
contextual chunks associated to ~actFsubsetG. Chunks are anno- set2 G 
tated with continuous activations that influence their retrieval..The activation Ai of a chunk Ci is 
defined as 
Ai = Si + ~WjSjl (1) 
J 
where Bi is the base-level activation, Wj is the weighting of a contextual chunk Cj, and Sji is 
the strength of the association of C/ with Cj. In Bi, which is defined such that it decreases 
logarithmically when Ci is not used, AcT-R models the forgetting of declarative knowledge. Note 
IActually, I am discussing AcT-R 4.0, which has some substantial changes to older versions. The acronym ACT 
denotes adaptive control of thought, R refers to the rational analysis that influenced the theory. 
89 
that the definition of the activation establishes a spreading activation to adjacent chunks, but not 
further; multi-link-spread is not supported. 
The constraint on the capacity of the human working memory is approached by defining a 
retrieval threshold r, where only those chunks Ci can be matched whose activation Ai is higher 
than r. Chunks with an activation less than ~- are considered as forgotten. 
:New declarative knowledge is acquired when a new chunk is stored in the declarative memory, 
as is always the case when a goal is popped from the goal stack. The application of a production 
may also cause a new chunk tobe Stored if required by the production's action part. 
2.2 Procedural Knowledge 
The operational knowledge of ACT:R is formalized in terms of productions. Productions generally 
consist of a condition part and an •action part, and can be appliedl if the condition part is fulfilled. 
In AcT-R both parts are defined in terms of chunk patterns. The condition is fulfilled if its first 
chunk pattern matches the current goal and the remaining chunk patterns match chunks in the 
declarative memory. An example for a production is 
.IF: the current goal is to show that x E $2 and it is known that x E S1 and $1 .C_ $2 
• THEN conclude that x ES2 by the definition of C: " 
• Similar to the base-level activation of chunks, the strength of a production is defined such 
that it decreases logarithmically when the production is ,not used. The time spent to match a 
production with a chunk depends on the activation of the chunk. 2 It is defined such that it is 
negative exponential to the sum of the activation of the chunk and the strength of the production. 
Hence, the higher the activation of the chunk and the strength of the production, the faster the 
production matches the chunk. Since the activation must be greater •than the retrieval threshold 
r; T constrains the time maximally available to match a production with a chunk. 
: The conflict resolution heuristic starts from assumptions on the probability P that the applica- 
tion of the current production leads to the goal and on the costs C of achieving that goal by this 
means. • Moreover G is the time maximally available to fulfill the goal. The net utility E of the 
application of a production is defined as 
.. - . . . . ~ • 
E = PG- C, (2) 
We do not go into detail on how P, G and C are calculated. For the purposes of this paper, it is 
sufficient to note that G only depends on the goal, but not on the production, and that the costs C 
depend among other things On the time to match a production. The faster the production matches, 
i.e. the stronge r it is and the greater the activations of the matching chunks are, the lower are the 
costs. . 
To sum up, in AcT-R the choice of a production to apply is as follows: 
1. The conflict set•is determined by testing the match of the productions with the current goal. 
2. The production p with the highest utility is chosen. 
3. The actual instantiation of p is determined via the activations of the corresponding chunks. If 
no instantiation is possible (because of v), p is removed from the conflict set and the algorithm 
resumes in step 2, otherwise the instantiation of p is appiied. 
21n this context, time does not mean the CPU time needed to calculate the match, but the time a human would 
need for the match according to the cognitive model. 
•90 
I 
I 
I 
I 
I 
I 
I 
I 
ill 
i,| 
II 
I 
! 
I 
1 
AcT-R provides a learning mechanism, called knowledge compilation, which allows for the 
learning of new productions. We are currently exploring this mechanism for its utility for the 
explanation of proofs. 
I 
I 
I 
I 
I 
I 
I 
I 
I 
I 
I 
I 
I 
I 
I 
I 
3 The Architecture of P. rex 
P.rex is planned as a generic explanation system that can be connected to different theorem 
provers. It adopts the following features of the interactive proof development environment f~MC.GA 
\[Benzmiiller et at., 1997\]: 
• Mathematical theories are organized in a hierarchical knowledge base. Each theory in it may 
contain axioms, definitions, theorems along with proofs, as well as proof methods, and Control 
rules how to apply proof methods. 
• A proof of a theorem is represented in a hierarchical data structure called proof plan data 
structure :(PDS). The PDS makes explicit the various levels of abstraction by providing sev- 
eral justifications for a single proof node, where each justification belongs to a different lexiel 
of abstraction. The least abstract level corresponds to a proof in Gentzen's natural de- 
duction (ND) calculus \[Gentzen, 1935\]. Candidates for higher levels are:proof plans, where 
justifications are mainly given by more abstract proof methods that belong to the theorem's 
mathematical theory or to an ancestor theory thereof. 
An example for a PDS is given below on the left. Each line consists of four elements (label, an- 
tecedent, succedent, and justification) and describes a node in the PDS. The label is used as a refer- 
ence for the node. The antecedent is a list of labels denoting the hypotheses under which the formula 
in the node, the succedent, holds, a This relation between antecedent and succedent is denoted by F-. 
Label Antecedent Succedent Justification 
Lo ~-aEUVaEV Jo 
H1 H1 I- a E U HYP 
L1 H1 I- a E U U V DeflA(H1) 
H~ H2 h a E V HYP 
L2 H2 I-- a E U U V DetU(H,2_) 
L3 I- a E U U V U-Lemma(Lo) 
- CASE(L0, Lx, L2) 
• We call A I- ~ the fact in the node. The proof 
of the fact in the node is given by its justifi- 
cation. A justification consists of a rule and 
a list of labels, the premises of the node. Ji 
denotes an unspecified justification. HYP and 
DefU stand for a hypothesis and the definition 
of U, respectively. L3 has two justifications on 
different levels of abstraction: the least abst- 
ract justification with the ND-rule CASE (i.e. the rule for case analyses) and the more abstract 
justification with the rule U-Lemma that stands for an already proven lemma about a property of 
U. By agreement, if a node has more than one justification, these are sorted from most abstract to 
least abstract. 
The proof is as follows: From a E U V a E V we can conclude that a E U U V by the U-Lemma. 
If we do not know the U-Lemma, we can come to the conclusion by considering the case analysis 
with the cases that a E U or a E V, respectively. In each case, we can derive that a E U O V by 
the definition of U. 
A formal language for specifying •PDSs is the interface by which theorem provers can be con- 
nected to P. rez. An overview of the architecture of P. rex is provided i n Figure 1. 
The crucial component of the system is the dialog planner. It is based on AcT-R, i.e. its 
operators are defined in terms of productions and the discourse history is represented in the declar- 
ative memory by storing conveyed information as chunks (details are given in Section 4). Moreover, 
3As notation we use A and F for emtecedents and ~ and q, for succedents. 
91 
! 
   gP'anner ' 
" | 
Figure 1: The Architecture of P. rex 
presumed declarative and procedural knowledge of the •user is encoded in the declarative memory 
and the:production rule base, respectively.' 
• In order to explain a particular proof, the dialog planner first assumes the user's supposed H 
cognitive state by Updating its declarative and procedural memories. This is done by looking up g 
the user's presumed knowledge in the user model, which was recorded during a previous session. ! 
An individual model for each user persists between the sessions. ! 
The user model contains assumptions on the knowledge of the user that are relevant to proof 
explanation. In particular, it makes assumptions on which mathematical theories the user knows, 
whiChhe hasdefiniti°nS'alreo;dy learned:Pr°°fs' proof methods and mathematical facts he knows, and which productions !' wg 
• After updating the declarative and procedural memories, the dialog planner sets the global 
goal tO show the conclusion of the PDS's theorem. ACT-R tries to fulfill this goal by successively ' • 
applying productions that decompose or fulfill goals. Thereby, the dialog planner not only produces 
a multimodal dialog plan (see Section 4.1), but also traces the user's • cognitive states in the course 
of the explanation. • This allows the system both to always choose an explanation adapted to the ~ • 
user (see Section 4.2), and to react to theuser's interactions in a flexible way: The dialogplanner | 
analyzes the interaction in terms of applications of productions. Then it plans an appropriate 
response. I 
The dialog plan produced by the dialog planner is passedon to the multimodal presentation 
componen~ which supports the modalities graphics, text, and speech. It consists of the following 
subcomponents: D 
A multimodal microplanner to be designed plans the scope of the sentences and their internal 
structure, as well as their graphical arrangement. It also decides, whether a graphical or a textual 
realization is preferred. Textual parts are passed on to a linguistic realizer that generates the nab 
surface sentences: Then a planned layout component displays the text and graphics, while a speech | 
system outputs the sentences in speech. Hence, the system should provide the user with text and 
graphics, as well as a spoken output. The metaphor we have in mind is the teacher who explains I 
what he is writing on the board. • 
An analyzer :to be designed receives the •user's interactions and passes them on to the dialog i 
planner. .! 
92 
I 
I 
I 
4 The Dialog Planner 
In the community of NLG, there is a broad consensus that the generation of natural language should 
be done in three major steps \[Reiter, 1994\]. First a macroplanner (text planner) determines what 
to say, i.e. content and order of the information to be conveyed. Then a microplanner (sentenCe 
planner) determines how to say it, i.e. it plans the scope and the internal structure of the sentences. 
Finally, a realizer (surface generator) produces the surface text. In this classification, the dialog 
planner is a macroplanner for managing dialogs. 
As Wahlster et al. argued, such a three-staged architecture is also appropriate for muitimodal 
generation \[Wahlster et al., 1993\]. By defining the operators and the dialog plan such that they 
are independent of the communication mode, our dialog planner plans text, graphics and speech. 
Since the dialog planner in P. rex is based on AcT-R, the plan operators are defined as produc- 
tions. A goal is the task to show the fact in a node n of the PDS. A production fulfills the goal 
directly by communicating the derivation of the fact in 7z from already known •facts or splits the 
goal into new subgo~ls such as to show the facts in the premises of n. The derivation of a fact is 
conveyed by so-called mathematics communicating acts (MCAs) and accompanied by storing the 
fact as a chunk in the declarative memory. Hence the discourse history is represented in the declar- 
ative memory. AcT-R's conflict resolution mechanism and the activation of the chunks ensure an 
explanation tailored to the user. The produced dialog plan is represented in terms of MCAs. 
4.1 Mathematics Communicating Acts 
Mathematics communicating acts (MCAs) are the primitive actions planned by the dialog planner. 
They are derived from PROVERB's proof communicative acts \[Huang, 1994\]. MCAs are viewed as 
• speech acts that are independent of the modality to be chosen. • Each MCAat least can be realized 
as a portion of text. Moreover some MCAs manifest themselves in the graphical arrangement of 
the text (see below for examples). 
In P. rez we distinguish between two types of MCAs: 
• MCAs of the first type, called derivational MCAs, convey a step of the derivation. An example 
for a derivati0n~l MCA with a possible verbalization is: 
.(Derive :Reasons (a 6 U, U C_ V) :Conclusion a 6 V :Method Deft) 
"Since a is an element of U and U is a subset of V, a is all element of V by the 
definition of subset." 
A graphical realization is shown in Figure 2(a). 
• • MCAs of the second type, called structural MCAs, communicate information about the struc- 
ture of a proof. For example case analyses are introduced by: 
(Case-Analysis :Goal ¢ :Cases (%01, %02)) " 
"To prove ¢, let us consider the two cases by assuming T1 and %02." 
Unless the two cases only enclose a few steps each, the graphical realization shown in Fig- 
ure 2(b) should be preferred for the visual presentation. 
93 
(a) aeU U cV (b) \/ /\ 
! ! a E V (by Def_C) , , 
! I 
V 
• Figure 2: Graphical realizations of MCAs. The dashed lines indicate not yet explained parts of the 
proof. 
4.2 Plan Operators - 
Operational knowledge concerning the presentation is encoded as productions in AcT-R that are 
independent from the modality to be chosen. In this paper, we concentrate on production s which 
allow for the explanatio n of a proof. We omit productions to react to the user's interactions. 
Each production either fulfills the current goal directlyor splits it into subgoals. Let us assume 
that the following nodes are in the current PDS: 
Label Antecedent Succedent Justification 
I)1 A1 • ~1 J1 
P, An b ~,~ J~ 
C F • ¢ R(Pi,..., Pn) 
An example for a production is: 
(P1) IF The current goal is to show F • ¢ 
and R is the most abstract known rule justifying the current goal 
and A 1 I- ~01,... , A n • ~n are known 
THEN produce MCA (Derive :Keasons (~i,--,~n) :Conclusion~b :Method R) 
and pop the current goal (thereby storing F I- ¢ in the declarative memory) 
• By producing the MCA the current goal is fulfilled and can be popped from the goal stack. An 
example for a production decomposing the current goal into several subgoals is: 
(P2) IF " The current goal is to show F I- ¢ 
and R is the most abstract known rule justifying • the current goal 
and (I) = {~oiiA i • ~i is unknown for 1 < i < n} ~ 0 
THEN for each 9i E (I) push the goal to show Ai t-- 9i 
Note that the Conditions of (P1) and (P2) only differ in the knowledge of the premises 9i for rule 
R. (P2) introduces the subgoals to prove the unknown premises in (I). As soon as those are derived, 
(P1) can apply and derive the Conclusion. 
Now assume that the following nodes are in the current PDS: 
Label . Antecedent 
Po F t- 
. H1 H1 t- 
P1 F, Hi" I- 
H2 H2 b 
P2 F, H2 • 
C F • 
Suceedent Justification 
~1 V ~o~ Jo 
~1 HYP 
f dl 
~2 HYP 
¢ J2 
¢ CASE(P0, PI, P2) 
94 
I 
I 
!1 
I 
I 
I 
'1 
'| 
( 
1 
I 
I 
I -} 
I 
I 
I 
/ 
I 
! 
| 
I 
I 
I 
i 
I 
I 
I 
I 
I 
i 
I 
I 
I 
! 
A specific production managing• such a case analysis is the following: 
(P3) IF The current goal is to show F I- ¢ 
and CASE is the most abstract known rule justifying the current goal 
and F I- ~o 1 V ~0 2 is known 
and r, H1 ~- ¢ and F, H2 ~- ¢ are unknown 
THEN push the goals to show F, H1 ~- ¢ and F,//2 h 
and produce MCA (Case-Analysis :Goal ¢ :Cases (~1,~2)) 
This production introduces new subgoalS and ,motivates them by producing the MCA. 
Since more specific rules treat common communicative standards used in mathematical presen- 
tations, they are assigned a higher strength than more general rules. Therefore, the strength of 
(P3) is higher than the strength of (P2), since (P3) has fewer variables. 
Moreover, it is supposed that each user knows all natural deduction (ND) rules. This is rea- 
sonable, since ND-rules are the least abstract possible logical rules in proofs. Hence, for each 
production p that is defined such that its goal is justified by an ND-rule in the PDS, the probabil- 
ity Pp that the application of p leads to the goal to explain that proof step equals one. •Therefore, 
since CASE is such an ND-rule, P(P3) = 1. 
hrorder to elucidate how a proof is explained by Rrex let us consider the following situation: 
•Tlie following nodes are in tile current PDS: 
Label Antecedent Succedent Justi ficatio~ 
Lo ba6UVa6V Jo 
H1 H1 h a 6 U HYP 
L1 Hi h a 6 U O V DefU(H1) 
H2 H2 ~- a 6 V HYP 
L_'2 H:~ ' I- a 6 U O V DefU(H.-,) 
L3 t- a 6 U U V O-Lemma(Lo) 
CASE(Lo, L1, L2) 
• the current goal is to show the fact in L3, 
• the rules HYP, CASE, Defo, and U-Lemma are known, 
• the fact in Lo is known, the facts in H,, La, H2, and L2 are unknown. 
The only applicable production is (P1). Since o-Lemma is more abstract than CASE and both 
are known, it has a higher activation and thus is chosen to instantiate (P1). Hence, the dialog 
planner produces the MCA 
(Derive :Reasons (a 6 U V a 6 V) :Conclusion a 6 UU V :Method U-Lemma) 
that could be verbalized as "Since a 6 U or a 6 V, a 6 U u V by the O-Lemma." 
Suppose now that the user interrupts the explanation throwing in that he did not understand 
this step. Then the system invokes productions that account for the following: The assumption 
that O-Lemma is known is revised by decreasing its base-level activation (cf. equation 1). Similarly, 
the just stored chunk for h a 6 U U V is erased from the declarative memory. Then the goal to 
show ~- a 6 U u V is again pushed on the goal stack. 
Now, since CASE is the most abstract known rule justifying the current goal, both decomposing 
productions (P2) and (P3) are applicable. Recall that the conflict resolution mechanism chooses 
the production with the highest utility E (cf. equation 9). Since P(P3) = 1 and Pp < 1 for all 
• • 95 
productions p, P(P3) ~ P(P2). Since the application of (P2) or (P3) would servethe same goal, 
G(p3) = G(p2). Since (P3) is stronger than (P3) because it is more specific, and since both 
production match the same chunks, C(p3} < C(p2). Thus 
E(p3) : P(pa)G(p3) - C(p3) > P(p2)G(p2) -- C(p2) ---- E(p2) 
Therefore, the dialog planner chooses (P3) for the explanation, thus producing ghe MCA 
(Case-Analysis :Goal a E UUV :Cases (a E U,a E V)) 
that could be realized as "To prove a E U O V let us consider the two cases by assuming a E U and 
a E V," and then explains both cases. This dialog could take place as follows: 
P. rez: Since a E U or a EV, a E UO V by the O-Lemma. 
User:. Why does this follow? • 
R fez: To prove a E U U V let us consider the two cases by assuming a E U and a E I/. If 
a E U, then aE U O V by the definition of 0. Similarly, if a E V, then a E U tO V. 
This example shows how a production and an instantiation are chosen by P. rex. While th, 
example elucidates the case that a more detailed explanation is desired, the system can similarly 
choose a more abstract explanation if needed. Hence, modeling the addressee's knowledge in AGT- 
1~ allows P. rex to explain the proof adapted to the user's knowledge by switching between the levels 
in the PDS as needed. 
5 Conclusion and Future Work 
in this paper, we proposed to combine thetraditional design of a dialog planner with a cognitive 
architecture in order to strive for an optimal user adaptation. In the interactive proof explaining 
system P. rex, the dialog planner is based on the theory of cognition AcT-R. 
Starting from certain assumptions about the addressee's knowledge (e.g. which facts does he 
know, which definitions, lemmasl etc.) built up in the user model during previous sessions, the 
dialog planner decides on which level of abstraction• to begin the explanation. Since AcT-R traces 
the user's Cognitive states during the explanation, the dialog planner can choose an appropriate 
degree of abstraction for each proof step to be explained. The rationale behind this architecture 
should prove to be useful for explanation systems in general. 
Moreover since this architecture can predict what is salient for the user and what he can infer, it 
could be used as a basis to decide whether or not to include optional information 
\[Walker and Rambow, 1994\]. 
P. rex is still in the design stage. As soon as the dialog planner is implemented the requirements 
will be met to compare P. rex's dialog plans with PROVERB's text plans in order to evaluate the 
architecture. Furthermore ' the presentation component and the analyzer are to be designed in 
more •detail. 
Currently, we are examining the knowledge compilation mechanism of AcT-R that Could enable 
the system to model the user's acquisition of proving skills. This could pave the way towards a 
tutorial system that not only explains )roofs, but also teaches concepts and proving methods and 
strategies. 
I 
/ I 
I 
I 
I 
I 
I 
I 
I 
ii 
i 
I 
1 
I 
I 
96 • 
I 
I 
l 
I 
I 
I 
I 
I 
I 
! 
I 
I 
I 
I 
I 
I 
I 
I 
Acknowledgements 
Many thanks go to JSrg Siekmann, Michael Kohlhase, Dieter WMlach, Helmut Hora~ek, Frank 
Pfenning, and Ken Koedinger for their help in the research and/or the writing of this pape r. I also 
want to thank the anonymous reviewers for their useful comments. 

References 
\[Anderson, 1993\] J. R. Anderson. Rules of the Mind. Lawrence Erlbaum Associates, Hillsdale, N J, 1993. 
\[Benzmiiller et al., 1997\] C. Benzmiiller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, 
M. I<ohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. f2MEOA; 
Towards a mathematical assistant. In W. McCune, editor, Proceedings of the 14th Conference on Auto- 
mated Deduction,•number 1249 in LNAI, pages 252-255, Townsville, Australia, I997. Springer Verlag. 
\[Cawsey, 1990\] A. Cawsey. Generating explanatory discourse. In R. Dale, C. Mellish, and M. Zock, editors, 
Current Research in Natural Language Generation , number 4 in Cognitive Science Series, pages 75-10i. 
Academic Press, San Diego, CA, 1990. 
\[Gentzen, 1935\] G. Gentzen. Untersuchungen fiber das logische Schliegen I & II. Mathemadsehe Zeitschrift, 
39:176-210,572-595, 1935. 
\[Horacek, 1997\] H. Horacek. A model for adapting explanations to the user's likely inferences. User Modelin 9 
and User-Adapted Interaction, 7:1-55, 1997. 
\[Huang and Fiedler, 1997\] X. Huang and A. Fiedler. Pr0of verbalization as an application of NLG. In M. E. 
Pollack.. editor, Proceedings of the 15th International joint Conference on Artificial Intelligence (!JCAI), 
pages 965-970, Nagoya, Japan, 1997. Morgan Kaufinann. 
\[Huang, 1994\] X. Huang. Planning argumentative texts. In Proceedings of the 15th International Conference 
on Computational Linguistics, pages 329-333, Kyoto, Japan, 1994. 
\[INLG, 1994\] Proceedings of the 7th International Worksho p on Natural Language• Generation, Kenneb- 
unkport, Maine, USA, 1994. 
\[Meyer and Kieras, 1997\] D. E. Meyer and D. E. Kieras. EPIC: A computational theory of executive 
cognitive processes and multiple-task performance: Part 1. Psychological Review, 104:3-65, 1997. 
\[Newell, 1990\] A. Newell. Unified Theories of Cognition. Havard University Press, Cambridge, MA, 1990. 
\[Paris, 1991\] C. Paris. The role 0f the user's domain knowledge in generation. Computational Intelligence, 
7:71-93, 1991. 
\[Reiter, 1994\] E. Reiter. Has a consensus NL generation architecture appeared, and is it psycho linguistically 
plausible? In \[INLG, 1994\], pages 163-170. 
\[Wahlster et ai., 1993\] W. Wahlster, E. Andre, W. Finkler, H.-J. Profitlich, and T. Rist. Plan-based inte- 
gration of natural language and graphics generation, Artificial Intelligence, 63:387-427, 1993. 
\[Walker and Rambow, 1994\] M. A. Walker and O. Rambow. The role of cognitive modeling in achieving 
communicative intentions. In \[INLG, 1994\], pages 171-180. , 
\[Zukerman and McConachy, 1993\] I. Zukerman and R. McConachy. Generating concise discourse that ad- 
dresses a user's inferences. In R. Bajcsy, editor, Proceedings of the 13th International Joint Conference 
on Artificial Intelligence (IJCAI), pages 1202-1207, Chambery, France, 1993. Morgan Kaufmann, San 
Mateo, CA. 
