\subsection{Related Projects and Products}

 \subsection{Related Projects and Products}

 To further illustrate the concept of \isac{}, a short comparison with related projects, products and technologies will be given, highlighting common grounds and substantial differences.

 To further illustrate the concept of \isac{}, a short comparison with related projects, products and technologies will be given, highlighting common grounds and substantial differences.

 A wealth of learning software has become available over the past decades, ranging from simple flashcard-like programs to elaborate interactive systems. An overview of readily available software is given in \cite{www:EduMath}.

 A wealth of learning software has become available over the past decades, ranging from simple flashcard-like programs to elaborate interactive systems. An overview of readily available software is given in \cite{www:EduMath}.

 \begin{description}

 \begin{description}

 \item[Common grounds:] \isac{} can be regarded as a math learning software insofar as we share the goal of extending the users' knowledge and ability to solve mathematical problems. We also share the methods of both presenting knowledge and practising examples in an interactive way.

 \item[Common grounds:] \isac{} can be regarded as a math learning software insofar as we share the goal of extending the users' knowledge and ability to solve mathematical problems. We also share the methods of both presenting knowledge and practising examples in an interactive way.

 \item[Major differences:] Most learning software works from pre-defined libraries of examples and lessons, and guides the user along didactically sophisticated, but fixed paths of interaction. \isac{} is extensible in both respects, offering support and learning experience even for user's examples not previously known to the system. Moreover, \isac{}'s paths of interaction are designed to be composed of so-called Dialog Atoms \ref{}, providing for user guidance configurable by a supporting teacher or even automatically adapting itself to the learner's behaviour.

 \item[Major differences:] Most learning software works from pre-defined libraries of examples and lessons, and guides the user along didactically sophisticated, but fixed paths of interaction. \isac{} is extensible in both respects, offering support and learning experience even for user's examples not previously known to the system. Moreover, \isac{}'s paths of interaction are designed to be composed of so-called Dialog Atoms \ref{}, providing for user guidance configurable by a supporting teacher or even automatically adapting itself to the learner's behaviour.

 A quotation from an internet-forum illustrates the problem:

 A quotation from an internet-forum illustrates the problem:

 \begin{quotation}

 \begin{quotation}

 Q: Hi, Can Mathematica show the steps that make to arrive at the answer, in a integration

 Q: Hi, Can Mathematica show the steps that make to arrive at the answer, in a integration

 A: Nope, sorry.  

 A: Nope, sorry.  

 \end{quotation}

 \end{quotation}

 Efforts to present intermediate results have been taken only recently. \isac{}, on the other hand, concentrates on making the process of solving transparent to the user. \isac{}'s mathematical knowledge is coded in the same rules and propositions used in teaching math and stored in a knowledge base browsable and comprehensible by the user. \isac{}'s computational algorithms are expressed using these rules and stored in so-called Methods \ref{}, which are accessible to the user as well. This provides not only for transparency, but also the flexibility to extend the knowledge used in obtaining a result and even changing the very way how a solution is obtained. \isac{}'s interactive tutoring capabilities going far beyond mere presentation of examples are based on this flexible concept.

 Efforts to present intermediate results have been taken only recently. \isac{}, on the other hand, concentrates on making the process of solving transparent to the user. \isac{}'s mathematical knowledge is coded in the same rules and propositions used in teaching math and stored in a knowledge base browsable and comprehensible by the user. \isac{}'s computational algorithms are expressed using these rules and stored in so-called Methods \ref{}, which are accessible to the user as well. This provides not only for transparency, but also the flexibility to extend the knowledge used in obtaining a result and even changing the very way how a solution is obtained. \isac{}'s interactive tutoring capabilities going far beyond mere presentation of examples are based on this flexible concept.

 In contrast to most available CAS, \isac{} is a networked application, allowing for mathematical knowledge and example libraries being shared across the internet.

 In contrast to most available CAS, \isac{} is a networked application, allowing for mathematical knowledge and example libraries being shared across the internet.

 While CAS can be used for learning purposes insofar as they facilitate exploration by taking the burden of calculation off the user, \isac{} can actively influence user interaction to achieve pedagogic goals.

 While CAS can be used for learning purposes insofar as they facilitate exploration by taking the burden of calculation off the user, \isac{} can actively influence user interaction to achieve pedagogic goals.

 \end{description}

 \end{description}

 The following programs are mentioned for their wide-spread use in educational and scientific institutions:

 The following programs are mentioned for their wide-spread use in educational and scientific institutions:

 \begin{description}

 \begin{description}

 \end{description}

 \end{description}

 \subsubsection{Theorem Provers}

 \subsubsection{Theorem Provers}

 \begin{description}

 \begin{description}

 %WN \sisac is designed to be responsible for correct results, too: it constructs the result of a calculation applying theorems proven by the theorem prover Isabelle \cite{Isa-intro}.

 %WN \sisac is designed to be responsible for correct results, too: it constructs the result of a calculation applying theorems proven by the theorem prover Isabelle \cite{Isa-intro}.

 %----

 %----

 %----

 %----

 \item[Major differences:] A theorem prover tries to answer the question 'Is the theorem true?'. A theorem prover's answer is yes or no. 

 \item[Major differences:] A theorem prover tries to answer the question 'Is the theorem true?'. A theorem prover's answer is yes or no. 

 \end{description}

 \end{description}

 \subsubsection{Expert Systems}

 \subsubsection{Expert Systems}

 \begin{description}

 \begin{description}

 \item[Common grounds:] \isac{}'s Knowledge Base could be regarded as a simple expert system for mathematical knowledge.

 \item[Common grounds:] \isac{}'s Knowledge Base could be regarded as a simple expert system for mathematical knowledge.

 \subsubsection{Standards and Tools Used}

 \subsubsection{Standards and Tools Used}

 Several evolving technologies are used in the \isac{} system, with their development closely observed and in some cases cooperatively influenced by \isac{}:

 Several evolving technologies are used in the \isac{} system, with their development closely observed and in some cases cooperatively influenced by \isac{}:

 \begin{description}

 \begin{description}

 \end{description}

 \end{description}

 \subsection{Status of the Project}

 \subsection{Status of the Project}

 %WN041008 bitte NICHT 'logic foundations' (dazu hab ich nur das allernotwendigste gemacht) und NICHT 'direction' (Du solltest das Einstandsgespraech mit dem naechsten Teammitglied mitgehoert haben!), sondern bitte Vorschlag unten ...

 %WN041008 bitte NICHT 'logic foundations' (dazu hab ich nur das allernotwendigste gemacht) und NICHT 'direction' (Du solltest das Einstandsgespraech mit dem naechsten Teammitglied mitgehoert haben!), sondern bitte Vorschlag unten ...

 \subsection{Structure of this Thesis}

 \subsection{Structure of this Thesis}

 requirements

 requirements

 implementation

 implementation

 \section{Introduction to Terms Used throughout this Thesis}\label{AK:intro:terms}

 \section{Introduction to Terms Used throughout this Thesis}\label{AK:intro:terms}

 In this section, terms describing basic concepts of \isac{} are explained. Please refer to the example in appendix \ref{use-expl} for a practical view, to appendix \ref{app.terms} for definitions of other terms and to \cite{wn:diss} for in-depth explanations.

 In this section, terms describing basic concepts of \isac{} are explained. Please refer to the example in appendix \ref{use-expl} for a practical view, to appendix \ref{app.terms} for definitions of other terms and to \cite{wn:diss} for in-depth explanations.

 % insert figure of the system

 % insert figure of the system

 %zB Klammerfehler werden vom Formeleditor behandelt: Syntaxfehler im FE, log Fehler (Typen, Vollst�digkeit von Model-Items etc.) im KE

 %zB Klammerfehler werden vom Formeleditor behandelt: Syntaxfehler im FE, log Fehler (Typen, Vollst�digkeit von Model-Items etc.) im KE

 \subsubsection{Knowledge Base}

 \subsubsection{Knowledge Base}

 \subsubsection{Knowledge Browser}

 \subsubsection{Knowledge Browser}

 The Knowledge Browser is the tool for searching and displaying knowledge from the Knowledge Base.

 The Knowledge Browser is the tool for searching and displaying knowledge from the Knowledge Base.

 \subsubsection{Worksheet}

 \subsubsection{Worksheet}

 The Worksheet is an abstraction of the traditional paper-and-pencil interface to calculations. It is the user's tool for viewing and manipulating calculations.

 The Worksheet is an abstraction of the traditional paper-and-pencil interface to calculations. It is the user's tool for viewing and manipulating calculations.

 \subsubsection{Dialog}

 \subsubsection{Dialog}

 \subsubsection{User Model}

 \subsubsection{User Model}

 The User Model is an abstraction of \isac{}'s experience with an individual user based on the history of interaction. In particular, the User Model keeps records of knowledge viewed or used by the user, the Dialog Atoms used and the user's success in this process.

 The User Model is an abstraction of \isac{}'s experience with an individual user based on the history of interaction. In particular, the User Model keeps records of knowledge viewed or used by the user, the Dialog Atoms used and the user's success in this process.

 Based on these data, the Dialog makes assumptions about the user's familiarity with mathematical concepts and guides him accordingly.

 Based on these data, the Dialog makes assumptions about the user's familiarity with mathematical concepts and guides him accordingly.

 \subsection{Key Elements in Calculations}

 \subsection{Key Elements in Calculations}

 \subsubsection{Formula}

 \subsubsection{Formula}

 A Formula is a formal text describing mathematical objects. From a practical point of view, a Formula in \isac{} is very much what you expect it to be.

 A Formula is a formal text describing mathematical objects. From a practical point of view, a Formula in \isac{} is very much what you expect it to be.

 \subsection{\isac{}'s Concept of Calculations}

 \subsection{\isac{}'s Concept of Calculations}

 \subsubsection{Calc Tree}

 \subsubsection{Calc Tree}

 \isac{} organizes calculations in Calculation Trees. The normal flow of an calculation alternates Formulas and Tactics transforming one Formula into the next one. This list-like structure branches where independent calculations have to be made to obtain intermediate results, such as finding the roots of the first derivative of a function to solve an optimization problem or to obtain several cases in a case-split.

 \isac{} organizes calculations in Calculation Trees. The normal flow of an calculation alternates Formulas and Tactics transforming one Formula into the next one. This list-like structure branches where independent calculations have to be made to obtain intermediate results, such as finding the roots of the first derivative of a function to solve an optimization problem or to obtain several cases in a case-split.

 \subsubsection{Subproblem}

 \subsubsection{Subproblem}

 \subsubsection{Calc Head}

 \subsubsection{Calc Head}

 A Calculation Header details all inputs, constraints and desired results necessary to start a calculation. 

 A Calculation Header details all inputs, constraints and desired results necessary to start a calculation. 

 Every Calc Tree has at least one Calc Head at its start, but may contain additional Calc Heads where Subproblems are started.

 Every Calc Tree has at least one Calc Head at its start, but may contain additional Calc Heads where Subproblems are started.

 \subsubsection{Specifiying Phase}

 \subsubsection{Specifiying Phase}

 The process of specifying all information necessary to start a calculation is called the Specifying Phase. Apart from the necessity of providing the information to the system, the Specifying Phase trains gaining insight into the nature of a mathematical problem before searching for a solution.

 The process of specifying all information necessary to start a calculation is called the Specifying Phase. Apart from the necessity of providing the information to the system, the Specifying Phase trains gaining insight into the nature of a mathematical problem before searching for a solution.

 \subsubsection{Solving Phase}

 \subsubsection{Solving Phase}

 In the Solving Phase, Formulas are repeatedly transformed into other Formulas by applying Tactics until eventually a solution is reached.

 In the Solving Phase, Formulas are repeatedly transformed into other Formulas by applying Tactics until eventually a solution is reached.

 \subsection{Mathematical Knowledge}

 \subsection{Mathematical Knowledge}

 \subsubsection{Problem}

 \subsubsection{Problem}

 A Problem describes the abstract common properties of a class of examples. A Problem describes the goal - what are we looking for - and which information has to be given to find a solution. Finding the roots of an equation is one Problem, finding the maximum of a function is another.

 A Problem describes the abstract common properties of a class of examples. A Problem describes the goal - what are we looking for - and which information has to be given to find a solution. Finding the roots of an equation is one Problem, finding the maximum of a function is another.

 Problems are contained in a hierarchy \isac{} uses for mechanical refinement of a problem (e.g. a type of equation, say 'univariate equation') to a more appropriate problem (say 'rational univariate equation').

 Problems are contained in a hierarchy \isac{} uses for mechanical refinement of a problem (e.g. a type of equation, say 'univariate equation') to a more appropriate problem (say 'rational univariate equation').

 \subsubsection{Formalization}

 \subsubsection{Formalization}

 A Formalization is a description of a real-world problem, which is normally stated in natural language, expressed in purely mathematical terms. 

 A Formalization is a description of a real-world problem, which is normally stated in natural language, expressed in purely mathematical terms. 

 %Statt dem obigen Satz (wobei die subsubsec auf Example folgt): A Formalization is the formal representation of an example; the representation is more general than the structure of a Model in order to be able to instantiate more than one Problem with the Formalization.

 %Statt dem obigen Satz (wobei die subsubsec auf Example folgt): A Formalization is the formal representation of an example; the representation is more general than the structure of a Model in order to be able to instantiate more than one Problem with the Formalization.

 A Formalization could consist of a formula, a indication of the solution sought and optionally additional formulas indicating contraints applying to valid solutions.% 'contraints' nein, diese werden im Zuge des 'instantiierens' aus dem Problem hinzugefuegt.

 A Formalization could consist of a formula, a indication of the solution sought and optionally additional formulas indicating contraints applying to valid solutions.% 'contraints' nein, diese werden im Zuge des 'instantiierens' aus dem Problem hinzugefuegt.

 \subsubsection{Specification}

 \subsubsection{Specification}

 \subsubsection{Description}

 \subsubsection{Description}

 In the context of \isac{}, the term Description applies only to descriptions of Examples, comprising text, formulas and figures, such a given in traditional math textbooks.

 In the context of \isac{}, the term Description applies only to descriptions of Examples, comprising text, formulas and figures, such a given in traditional math textbooks.