1 \chapter{List of terms used in the \isac-project}\label{app.terms}
5 \item{\bf Active formula (Aktive Formel)} is the unique formula marked on the \see worksheet, where the next step of calculation will be performed. If another item on the worksheet is marked, the formula closest (.. to be specified) to the marked item is the active formula. If the calculation is finished, the result of the calculation is the active formula. Also \see context position.
8 \item{\bf Browser (Browser):}\label{browser} There are browsers for \see theories, \see problems, \see methods and \see examples. %The browser generates the html-representation of the respective \see browser-window, and handles the respective http-requests.
9 \item{\bf Browser dialog (Browser-Dialog)} is the part of the \see dialog guide which is concerned with the access to the \see KE-store.
10 \item{\bf Browser-Window (Browser-Window)}\label{browser-window} is the presentation of data generated by the \see browser, which also handles the http requests generated by the browser window. (The browser-window is that what usually is called a 'browser').
13 \item{\bf Calc-head (Rechnungskopf)} is the first (highly structured) element in a \see calculation (i.e. a 'root-problem') and in a subproblem. It consists of a \see headline, a \see model and of a \see specification. On the \see worksheet it is represented only by the headline.
14 \item{\bf Calc-state (Rechenzustand)} is given by an internal calc-tree (partially represented on the \see worksheet) and a \see active formula.
15 \item{\bf Calculation (Rechengang)} leads from the \see description of an \see example via the \see modeling phase, the \see specification phase and the \see solving phase to the result.
16 \item{\bf Calculator (Rechner)} is that part of the \see SML-kernel which does single steps of calculation without touching the \see proofstate.
18 \item{\bf Course admin (Kurs-Administrator)} is a person administering the use of \isac{} for learning within a group of \see learners.
20 \item{\bf Course designer (Kurs-Designer)} edits the \see example collection which can be solved by a given \see math knowledge base (edited by a \see mathematics author) and/or edits \see explanations within the \see math knowledge base.
21 \item{\bf Context (Kontext)} is a relation between the \see context position in a certain \see calculation and a part of the \see math knowledge.
22 \item{\bf Context position (Kontext Position)} is a uniquely formula in a \see calculation giving one side of a \see context.
25 \item{\bf Decorated knowledge (Erweitertes Mathematik-Wissen)} is the \see mathemath knowledge(base) plus \see explanations. Each element of the math knowledge can have $0\dots n$ explanations (usually specific for courses).
26 \item{\bf Description (Beschreibung)} of an \see example consists of \see formulas, eventually of text and/or a figure. The \see modeling phase transforms the description into a \see model.
29 \item{\bf Dialog atom (Dialog-Atom)} is a predefined, minimal unit of interaction between the \see learner and \isac. These atoms are symmetrical w.r.t. the two dialog partners.
30 \item{\bf Dialog author (Dialog-Autor)} an expert in learning theory who adapts and extends the \see dialog guide.
31 \item{\bf Dialog guide (Dialog-Komponente)} is a component of \isac{} which %combines \see dialog atoms to dialog strategies in order to adapt \isac's behaviour to different user models and learning situations. It
32 consists of the \see worksheet-dialog and the \see browser-dialogs.
33 \item{\bf Dialog mode (Dialog-Modus)} is assembled from \see dialog patterns and supports certain learning strategies, e.g. exploratory learning, written examniation etc. Dialog patterns are designed and implementd by a \see dialog author. \item{\bf Dialog pattern (Dialog-Muster)} is assembled from \see dialog atoms such that it can adapt to certain situations in a dialog, e.g. if the \see learner produces many errors. Dialog patterns are designed and implementd by a \see dialog author.
34 \item{\bf Dialog profile (Dialog-Profil)} defines certain \see dialog modes for examples in the example collection for a certain course. A dialog profile is defined by a \see course designer and set/reset for a specified duration during a course by the \see course admin.
37 \item{\bf Example (Beispiel)} is a unit to be calculated and solved separated from others. In general, they are prepared by an author in an \see example collection. It consists of an explanation (analoguous to \see explanation of an element of the math knowledge), a \see formalization and a \see specification.
38 \item{\bf Example browser (Beispiels-Browser)} is an interactive representation of the \see example collection within the \see front-end.
39 \item{\bf Example collection (Beispielsammlung)} contains \see examples, each of them consisting of formulas, of a hidden \see formalization and \see specification, and eventuallly of text and a figure.
40 \item{\bf Example profile (Beispiels-Profil)} describes the structure of an\see example collection; this structure provides data for the \see dialog guide.
42 \item{\bf Explanation (Erkl\"arung)} is an optional addon (text, formulas, figures, movies, links, \see examples and any combination of these) to elements of the \see math knowledge base.
44 \item{\bf Formalization (Formalisierung)} contains the formulas in a minimal structure necessary for automated generation of a \see model of an example. Together with a \see specification this information is sufficient for automatically solve the example.
46 \item{\bf Formula (Formel)} consists of variables, constants and functions constants (for logical, algebraic etc. operators); all these parts, however are not yet structured as a (typed) \see term.
48 %\item{\bf Front-end (Frontend)} consists of the \see worksheet, the \see theory browser, the \see problem browser, the \see method browser and the \see example browser.
49 \item{\bf Guard (Guard)} of a \see method: prevents the method's script to be applied to an inappropriate problem. The guard has the same structure as a \see modelpattern (and thus sometimes is called a 'guardpattern').
51 \item{\bf Headline (Problem-Kopf)} represents a \see calc-head on the worksheet; it either looks like {\it Problem (Reals, [univariate,equations])} or an Algebrasystem function like {\it solve(}$x^2+x+1=0, \;x${\it )}.
54 \item{\bf Interpreter (Interpreter)} comprises the modules \see math engine and the \see calculator.
56 \item{\bf Isabelle} is the name of one of the most successful interactive theorem provers; Isabelle provides the \see theories containing the deductive part of \isac's knowledge base.
58 \item{\bf Item (Item)} of a \see model, which can be an input item (in the field 'given'), a precondition (in the field 'where'), an ouput item (in the field 'find') or a relation (in the field 'relate'). 'Given', 'find'and 'relate' may be input by the user, where 'where' is supplied by the system. An item consists of the \see item-description and the \see item-data.
59 \item{\bf Item-data (Item-Daten)} are the formulas following the \see item-description.
60 \item{\bf Item-description (Item-Beschreibung)} is an identifier heading each \see item in the fields 'given', 'find' and 'relate'. It indicates the kind of data to be input to the respective item by the users, serves typechecking of the data etc.
61 \item{\bf Item-status (Item-Status)} gives feedback to each item of a \see model with {\em one} of the following kinds of status: correct, true, false, missing, incomplete, superfluous, syntaxerror.
63 \item{\bf KE-store (KE-Basis)} is the \see decorated \see math knowledge plus the \see example collection.
65 \item{\bf Kernel (SML-Kern)} comprises the \see interpreter and the \see knowledge base, all written in SML.
67 \item{\bf Knowledge base} \see mathematics knowledge base
68 \item{\bf Knowledge browser} is one of the \see theory brosers, \see problem browser, \see method browser.
70 \item{\bf Learner (Lernender)} a user of \isac, who uses \isac{} for learning and exercising, i.e. who calculates \see examples by use of the \see math knowledge base.
71 \item{\bf Learner model (Lernprofil)} is an abstraction over all interactions of a certain learner with {\sisac} during a course; this abstraction serves to adapt \sisac's behaviour to the personal needs of the learner.
73 \item{\bf Match (Matchen):} the \see model of an example (or a subproblem) matches the \see modelpattern of a problem, or not. This kind of matching is different from the matching-algorithm of symbolic computation: it checks if all \see items are input, and evaluates the predicates in 'where'.
75 \item{\bf Math engine (Mathematik-Maschine)} provides for all functions doing \see calculations: for applying \see tactics, for input \see formulas, for calculating resulting formulas, for proposing the next tactic, and for doing calculations automatically; it maintains a \see proofstate for each calculation.
76 \item{\bf Mathematics author (Mathematik-Autor)} an expert in computer mathematics who adapts and extends the \see mathematics knowledge base.
77 \item{\it Mathematics kernel (Mathematik-Kern)} replaced by \see math engine; please, dont't use anymore~!
78 \item{\bf Mathematics knowledge base (Mathematische Wissensbasis)} is stored in three SML-datastructures, in an acyclic graph of \see theories, in a hierarchy of \see problems, and in a hierarchy of \see methods. It is extensible by \see math authors and can be both, read by \see learners and interpreted by \isac. Short form is math knowledge. See also \see decorated math knowledge.
80 \item{\bf Method (Methode)} contains a \see script describing the algorithm for calculating the result, and a guard structured like a \see modelpattern in order to inhibit inappropriate application of the script.
81 \item{\bf Method browser (Methoden-Browser)}
83 \item{\bf Model (Modell)} is a part of the \see calc-head. It consists of \see items (as well as the \see modelpattern).
84 \item{\bf Modelpattern (Modell-Pattern)} is the part of a \see problem.
85 %\item{\bf Model context (Modell-Kontext)} comprises all the information handled in the \see modeling phase as represented on the worksheet. This is at least one of the folloging items: a \see model (of a problem and/or of a method), a \see theory, a \see problem, a \see method.
86 \item{\bf Modeling phase (Modellierungs-Phase)} is the initial phase in problem solving. In this phase either the system automatically transforms a \see formalization of an example into a \see model or the user inputs the \see items into the model.
88 \item{\bf Parsing (Parsen)} is the process of transforming an 'plain' formula into a typed term. Parsing requires the specification of a \see theory containing information about infix position of operators etc.
90 \item{\bf Problem browser (Problem-Browser)}
91 \item{\bf Problem (Problem)} consists of a \see modelpattern and some technical elements (\see methods solving this problem, rule sets for evaluating the precondition in \see matching etc.)
93 \item{\it Proofstate (Beweiszustand)} replaced by \see calc-state; please, don't use anymore~!
95 \item{\bf Rewriting (Rewriting)} transforms a formula into a new one by application of a \see theorem. \isac{} provides conditional as well as ordered rewriting.
97 \item{\bf Script (Skript)} describes the algorithm solving a particular problem; a script contains \see tactics, expressions for guiding the flow of evaluation, and eventually subproblems.
99 \item{\bf Selection-tool (Auswahls-Tool)} displays the contents of either the \see example collection, or the dependency graph of \see theories, or the hierarchy of \see problems, or the hierarchy of \see methods; and it allows to select a respective item for detailed display.
101 \item{\bf SML-kernel} \see kernel
103 \item{\bf Solving phase (L\"osungs-Phase)} is the final phase in problem solving, which generates the solution from the \see model and the \see specification; this phase may comprise all problem solving phases for one or more subproblems.
105 \item{\bf Specification (Spezifikation)} relates a \see model (or a \see guard) of a calc-head to the \see modelpattern (or guradpattern) of the respective \see problem (or \see method) while determining a \see theory, \see a problem and a \see method.
106 \item{\bf Specification phase (Spezifikations-Phase)} is the second phase in problem solving, which determines the \see theory, \see the problem and the \see method. This phase can be done automatically and hidden from the user, if the \see dialog guide decides to do so. Sometimes, if it is clear from the context, this phase also comprises the \see modeling phase.
108 \item{\bf Step ((Rechen-) Schritt)} propagates a \see calculation and involves both partners once, i.e. the \see learner and the \see dialog guide. A step is represented by one of the \see dialog atoms.
110 \item{\bf Tactic (Taktik)} is applicable or not to the current \see formula within the current proofstate, and generates a new formula accordingly.
112 \item{\bf Term (Term)} is an Isabelle term (simple typed lambda calculus) generated from a \see formula by \see parsing.
114 \item{\bf Theorem (Theorem)} is a predicate proven true by \see Isabelle w.r.t. certain preconditions. Theorems are applied by \see rewriting.
116 \item{\bf Theory (Theorie)} is the part of the \see math knowledge base which defines (function) constants and axioms. Within a theory usually the related \see theorems are being proven by \see Isabelle and stored.
117 \item{\bf Theory Browser (Theorie-Browser)}
119 \item{\bf User (Benutzer)} of \isac{} may be one of the following: \see visitor, \see learner, \see math author, \see dialog author, \see course designer, or \see course admin.
121 \item{\bf Visitor (Besucher)} a user of \isac, which occasionaly browses an \isac-site, i.e. the \see knowledge base and the \see example collection.
123 \item{\bf Worksheet (Arbeitsblatt)} contains the \see calculation of an \see example eventually leading to a result.
125 \item{\bf Worksheet dialog (Arbeitsblatt-Dialog)} is the part of the \see dialog guide which is concerned with the interaction between learner (see chapter \ref{kinds-users} on p.\pageref{kinds-users}) and \see math engine.