\author{The \isac-Team\\

 \author{Alexandra Hirn und Eva Rott\\

 In diesem Kapitel werden alle schon zur Verf\"ugung stehenden Schritte aufgelistet. Diese Liste kann sich auf Grund von weiteren Entwicklungen von \isac{} noch \"andern.

 In diesem Kapitel werden alle schon zur Verf\"ugung stehenden Schritte aufgelistet. Diese Liste kann sich auf Grund von weiteren Entwicklungen von \isac{} noch \"andern.\

 \newline \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion} gibt die eingegebenen Befehle weiter an die mathematic engine, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler die Taktik verwendet.

 \newline \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion} gibt die eingegebenen Befehle weiter an die mathematic engine, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler tactic verwendet.\

 \newline \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.

 \newline \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\

 \newline \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"u das Umformen.

 \newline \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"u das Umformen.\

 \newline \textbf{Add\_Given, Add\_Find, Add\_Relation formula} f\"ugt eine Formel in ein bestimmtes Feld eines Modells ein. Dies ist notwendig, solange noch kein Objekt f\"ur den Benutzer vorhanden ist, in dem man die Formel eingeben kann, und nicht die gew\"unschte Taktik und Formel von einer Liste w\"ahlen will.

 \newline \textbf{Add\_Given, Add\_Find, Add\_Relation formula} f\"ugt eine Formel in ein bestimmtes Feld eines Modells ein. Dies ist notwendig, solange noch kein Objekt f\"ur den Benutzer vorhanden ist, in dem man die Formel eingeben kann, und nicht die gew\"unschte tactic und Formel von einer Liste w\"ahlen will.\

 \newline \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.

 \newline \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\

 \newline \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.

 \newline \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\

 \newline \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.

 \newline \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\

 \newline \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe eine method.

 \newline \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe eine method.\

 \newline \textbf{Rewrite theorem} bef\"ordert ein theorem in die aktuelle Formel und wandelt es demenetsprechend um. Wenn dies nicht m\"oglich ist, kommt eine Meldung mit ''error``.

 \newline \textbf{Rewrite theorem} bef\"ordert ein theorem in die aktuelle Formel und wandelt es demenetsprechend um. Wenn dies nicht m\"oglich ist, kommt eine Meldung mit ''error``.\

 \newline \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des Theorems, anstatt diese zu sch\"atzen.

 \newline \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des Theorems, anstatt diese zu sch\"atzen.\

 \newline \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von Theorems, dem rule set.

 \newline \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von Theorems, dem rule set.\

 \newline \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen Taktiken, ersetzt aber Konstanten in der Theorem, bevor es zu einer Anwendung kommt.

 \newline \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen tactics, ersetzt aber Konstanten in der Theorem, bevor es zu einer Anwendung kommt.\

 \newline \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\

 \newline \textbf{Substitute substitution} f\"ugt substitution der momentanen Formel hinzu und wandelt es um.\

 \newline \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\

 \newline \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\

 \newline \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\

 \newline \textbf{Split\_And, Conclude\_And, Split\_Or, Conclude\_Or, Begin\_Trans, End\_Trans, Begin\_Sequ, End\_Sequ, Split\_Intersect, End\_Intersect} betreffen den Bau einzelner branches des proof trees. Normalerweise werden sie vom dialog guide verdr\"angt.\

 \newline \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\

 \newline \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\

 \newline \textbf{Check\_postcond:} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim beenden des subproblem.\

 \newpage

 \newline \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.

 ------------------------------- ALTER TEXT -------------------------------

 \section{Die Funktionsweise der mathematic engine}

 \chapter{Do a calculational proof}

 Ein proof (= Beweis) wird in der mathematic engine {\tt me} von der tactic {\tt Init\_Proof} gestartet und wird wechselwirkend mit anderen tactics vornagebracht. Auf den input (= das, was eingegeben wurde) einzelner tactics folgt eine Formel, die von der {\tt me} ausgegeben wird, und die darauf folgende tactic gilt. Der proof ist beendet, sobald die {\tt me} {\tt End\_Proof} als n\"achste tactic vorschl\"agt.

 First we list all the tactics available so far (this list may be extended during further development of \isac).

 \newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird. 

 {\footnotesize\begin{verbatim}

 \section{Tactics for doing steps in calculations}

 ??????????????????????????????????????????????????????????????????????????????????   

 \input{tactics}

 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",

 \section{The functionality of the math engine}

 A proof is being started in the math engine {\tt me} by the tactic

 \footnote{In the present version a tactic is of type {\tt mstep}.}

  {\tt Init\_Proof}, and interactively promoted by other tactics. On input of each tactic the {\tt me} returns the resulting formula and the next tactic applicable. The proof is finished, when the {\tt me} proposes {\tt End\_Proof} as the next tactic.

 We show a calculation (calculational proof) concerning equation solving, where the type of equation is refined automatically: The equation is given by the respective formalization ...

 {\footnotesize\begin{verbatim}

    ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",

 \end{verbatim}}%size

 \end{verbatim}

 ... and the specification {\tt spec} of a domain {\tt dom}, a problem type {\tt pbt} and a method {\tt met}. Note that the equation is such, that it is not immediatly clear, what type it is in particular (it could be a polynomial of degree 2; but, for sure, the type is some specialized type of a univariate equation). Thus, no method ({\tt no\_met}) can be specified for solving the problem.

 \section{Der Beginn einer Rechnung}

 Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.

 Um einen neuen proof beginnen zu k\"onnen, werden folgende Schritte durchgef\"uhrt:

 Der proof state wird von einem proof tree und einer position ausgegeben. Beide sind zu Beginn leer. Die tactic {\tt Init\_Proof} ist, wie alle anderen tactics auch, an einen string gekoppelt.

 \footnotesize\begin{verbatim}

 \section{Initialize the calculation}

 ???????????????????????????????????????????????????????????????????????????????????????????? 

 The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ptree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons.

 ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));

 {\footnotesize\begin{verbatim}

    ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));

    \end{verbatim}}%size

 \end{verbatim}

 The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ptree}, {\tt pos'}).

 Die mathematics engine gibt etwas mit dem type {\tt mout} aus, was in unserem Fall ein Problem darstellt. Sobald die Schriftgr\"osse ge\"andert wird, m\"usste dieses jedoch gel\"ost sein.

 \footnotesize\begin{verbatim}

 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:

 ?????????????????????????????????????????????????????????????????????????????????????????????

 {\footnotesize\begin{verbatim}

 \end{verbatim}}%size

 \end{verbatim}

 Recall, please, the format of a problem as presented in sect.\ref{pbl} on p.\pageref{pbl}; such an 'empty' problem can be found above encapsulated by several constructors containing additional data (necessary for the dialog guide, not relevant here).\\

 {\footnotesize\begin{verbatim}

 ?????????????????????????????????????????????????????????????????????????????????????????????

 {\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\

 In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.

 {\footnotesize\begin{verbatim}

 \end{verbatim}}%size

 \end{verbatim}

 \section{The phase of modeling}

 \section{The phase of modeling} 

 Dieses Kapitel besch\"aftigt sich mit dem input der Einzelheiten bei einem Problem. Die {\tt me} kann dabei helfen, wenn man die formalization durch {\tt Init\_Proof} darauf hinweist. Normalerweise weiss die mathematic engine die n\"achste gute tactic.

 comprises the input of the items of the problem; the {\tt me} can help by use of the formalization tacitly transferred by {\tt Init\_Proof}. In particular, the {\tt me} in general 'knows' the next promising tactic; the first one has been returned by the (hidden) tactic {\tt Model\_Problem}.

 {\footnotesize\begin{verbatim}

 ?????????????????????????????????????????????????????????????????????????????????????????????

 {\footnotesize\begin{verbatim}

 \end{verbatim}}%size

 \end{verbatim}

 \noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more.

 {\footnotesize\begin{verbatim}

 {\footnotesize\begin{verbatim}

 ?????????????????????????????????????????????????????????????????????????????????????????????

 \end{verbatim}}%size

 \end{verbatim}

 %One of the input items is considered {\tt Superfluous} by the {\tt me} consulting the problem type {\tt ["univariate","equation"]}. The {\tt ErrorBound}, however, could become important in case the equation only could be solved by some iteration method.

 \section{The phase of specification} 

 \section{The phase of specification}

 This phase provides for explicit determination of the domain, the problem type, and the method to be used. In particular, the search for the appropriate problem type is being supported. There are two tactics for this purpose: {\tt Specify\_Problem} generates feedback on how a candidate of a problem type matches the current problem, and {\tt Refine\_Problem} provides help by the system, if the user gets lost.

 Diese phase liefert eindeutige Bestimmungen einer Domäne, den problem type und die method damit man sie verwenden kann. F\"ur gew\"ohnlich wird die Suche nach dem richtigen problem type unterst\"utzt. Dazu sind zwei tactics verwendbar: {\tt Specify\_Problem} entwickelt ein Feedback, wie ein problem type bei dem jetzigen Problem zusammenpasst und {\tt Refine\_Problem} stellt Hilfe durch das System bereit, falls der Benutzer die \"Ubersicht verliert.

 {\footnotesize\begin{verbatim}

 {\footnotesize\begin{verbatim}

 ML> nxt;

 ??????????????????????????????????????????????????????????????????????????????????????????

    ML> nxt;

 \end{verbatim}}%size

 \end{verbatim}

 The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows.

 Die {\tt me} erkennt den richtigen Problem type und arbeitet so weiter:

 {\footnotesize\begin{verbatim}

 {\footnotesize\begin{verbatim}

 ?????????????????????????????????????????????????????????????????????????????????????????

 \end{verbatim}}%size

 \end{verbatim}

 Again assuming that the dialog guide hide the next tactic proposed by the {\tt me}, and the student gets lost, {\tt Refine\_Problem} always 'knows' the way out, if applied to the problem type {\tt["univariate","equation"]}.

 Wir nehmen wieder an, dass der dialog guide die n\"achsten tactics, veranlasst von der mathematic engine, versteckt und der Sch\"uler Hilfe ben\"otigt. Dann muss {\tt Refine\_Problem} angewandt werden. Dieser Befehl findet immer den richtigen Weg, wenn man es auf den problem type bezieht [''univariate``, ''equation``].

 {\footnotesize\begin{verbatim}

 {\footnotesize\begin{verbatim}

 ????????????????????????????????????????????????????????????????????????????????????????????

 \end{verbatim}}%size

 \end{verbatim}

 The tactic {\tt Refine\_Problem} returns all matches to problem types along the path traced in the problem hierarchy (anlogously to the authoring tool for refinement in sect.\ref{refine} on p.\pageref{refine}) --- a lot of information to be displayed appropriately in the hiearchy browser~!

 Die tactic {\tt Refine\_Problem} wandelt alle matches wieder in problem types um und sucht in der problem hierachy weiter.

 \section{The phase of solving} 

 This phase starts by invoking a method, which acchieves the normal form within two tactics, {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}:

 \section{The phase of solving}

 Diese phase beginnt mit dem Aufruf einer method, die eine normale form innarhalb einer tactic ausf\"uhrt: {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}:

 \end{verbatim}}%size

 \end{verbatim}

 Now the normal form {\tt \#-6 + \#3 * x = \#0} is the input to a subproblem, which again allows for specification of the type of equation, and the respective method:

 Die Formel $-6 + 3 * x = 0$ ist die Eingabe eine subproblems, das wiederum gebraucht wird, um die Gleichungsart zu erkennen und die entsprechende method auszuf\"uhren:

 \end{verbatim}}%size

 \end{verbatim}

 As required, the tactic {\tt Refine ["univariate","equation"]} selects the appropriate type of equation from the problem hierarchy, which can be seen by the tactic {\tt Model\_Problem ["linear","univariate","equation"]} prosed by the system.

 {\tt Refine [''univariate``, ''equation``]} sucht die passende Gleichungsart aus der problem hierachy heraus, welche man mit {\tt Model\_Problem [''linear``, ''univariate``, ''equation``]} \"uber das System ansehen kann.

 Nun folgt erneut die phase of modeling und die phase of specification.

 Again the whole phase of modeling and specification follows; we skip it here, and \isac's dialog guide may decide to do so as well.

 \section{The final phase: \"Uberpr\"ufung der ''post-condition``}

 Die gezeigten problems, die durch \isac{} gel\"ost wurden, sind so genannte 'example construction problems'. Das massivste Merkmal solcher problems ist die post-condition. Im Umgang mit dieser gibt es in diesem Zusammenhang noch offene Fragen.

 \section{The final phase: check the post-condition}

 Dadurch wird die post-condition im folgenden Beispiel als problem und subproblem erw\"ahnt.

 The type of problems solved by \isac{} are so-called 'example construction problems' as shown above. The most characteristic point of such a problem is the post-condition. The handling of the post-condition in the given context is an open research question.

 Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem:

 \end{verbatim}}%size

 \end{verbatim}

 The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\

 Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\

 {\it The tactics proposed by the system need {\em not} be followed by the user; the user is free to choose other tactics, and the system will report, if this is applicable at the respective proof state, or not~! The reader may try out~!}

 {\it Die tactics, die vom System vorgeschlagen werden, m\"ussen vom Benutzer nicht angewendet werden. Er kann selbstverst\"andlich auch andere tactics verwenden und das System wird melden, ob dieser Befehl zutreffend ist oder nicht. Man sollte unbedingt selbst verschiedene Beispiele ausprobieren!}

 \part{Systematische Beschreibung}

 \part{Systematic description}

 \chapter{Die Struktur des Grundlagenwissens}

 \chapter{The structure of the knowledge base}

 \section{Taktiken und Daten}

 Zuerst betrachten wir das ME von außen. Wir sehen uns Taktiken und an und verbinden sie mit unserem Grundwissen (KB). Im Bezug auf das KB befassen wir uns mit den kleinsten Teilchen, die von den Autoren des KB sehr genau durchgef\"uhrt werden m\"ussen.

 \section{Tactics and data}

 Diese Teile sind in alphabetischer Anordnung in Tab.\ref{kb-items} auf Seite \pageref{kb-items} aufgelistet.

 First we view the ME from outside, i.e. we regard tactics and relate them to the knowledge base (KB). W.r.t. the KB we address the atomic items which have to be implemented in detail by the authors of the KB

 \footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.}

 . The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}.

 \caption{Atomic items of the KB} \label{kb-items}

 \caption{Kleinste Teilchen des KB} \label{kb-items}

 abbrevation & description \\

 Abk\"urzung & Beschreibung \\

 & associationlist of the evaluation-functions {\it eval\_fn}\\

 & gesammelte Liste von allen ausgewerteten Funktionen {\it eval\_fn}\\

 & evaluation-function for numerals and for predicates coded in SML\\

 & ausgewertete Funktionen f\"r Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\

 {\it eval\_rls   }

 {\it eval\_rls }

 & ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\

 & Regelsatz {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\

 & formalization, i.e. a minimal formula representation of an example \\

 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\

 & a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\

 & eine Methode d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer Phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\

 & reference to a {\it met}\\

 & bezieht sich auf {\it met}\\

 & operator as key to an {\it eval\_fn} in a {\it calc\_list}\\

 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\

 & problem, i.e. a node in the problem-hierarchy\\

 & Problem d.h. der Knotenpunkt in der Hierarchie von Problemen\\

 & reference to a {\it pbl}\\

 & bezieht sich auf {\it pbl}\\

 & rewrite-order\\

 & Anordnung beim Rewriting\\

 & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\

 & Regelsatz, d.h. eine Datenstruktur, die Theoremss {\it thm} und Operatoren {\it op} zur Vereinfachuing (mit {\it rew\_ord}) enth\"alt \\

 & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\

 & Regelsatz f\"ur das 'reverse rewriting' (eine \isac-Technik, die das schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\

 & script describing algorithms by tactics, part of a {\it met} \\

 & Skript, das die Algorithmen durch Anwenden von Taktiken beschreibt und ein Teil von {\it met} ist \\

 & special ruleset calculating a normalform, associated with a {\it thy}\\

 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\

 & specification, i.e. a tripel ({\it thyID, pblID, metID})\\

 & Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\

 & substitution, i.e. a list of variable-value-pairs\\

 & Ersatz, z.B. eine Liste von Variablen und ihren jeweiligen Werten\\

 & Isabelle term, i.e. a formula\\

 & Term von Isabelle, z.B. eine Formel\\

 & theorem\\     

 & theorem\\

 & theory\\

 & Theorie\\

 & reference to a {\it thy} \\

 & im Bezug auf {\it thy} \\

 \end{tabular}\end{center}\end{table}

 \end{tabular}\end{center}\end{table}}

 }

 The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}.

 Die Verbindung zwischen Taktiken und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.

 {\def\arraystretch{1.2}

 \caption{Which tactic uses which KB's item~?} \label{tac-kb}

 \caption{Welche Taktiken verwenden die Teile des KB~?} \label{tac-kb}

 tactic  &input &    &    &    &norm\_&   &rew\_&rls &eval\_&eval\_&calc\_&   \\

 Taktik &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\

         &      &thy &scr &Rrls&rls  &thm &ord  &Rrls&fn    &rls   &list  &dsc\\

 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\

         &fmz   & x  &    &    & x   &    &     &    &      &      &      & x \\

 &fmz & x & & & x & & & & & & & x \\

         &spec  &    &    &    &     &    &     &    &      &      &      &   \\

 &spec & & & & & & & & & & & \\

 Add\_*  &term  & x  &    &    & x   &    &     &    &      &      &      & x \\

 Add\_*

 FormFK  &model & x  &    &    & x   &    &     &    &      &      &      & x \\

 &term & x & & & x & & & & & & & x \\

 FormFK &model & x & & & x & & & & & & & x \\

 Specify\_Theory 

 Specify\_Theory

         &thyID & x  &    &    & x   &    &     &    & x    & x    &      & x \\

 &thyID & x & & & x & & & & x & x & & x \\

 Specify\_Problem 

 Specify\_Problem

         &pblID & x  &    &    & x   &    &     &    & x    & x    &      & x \\

 &pblID & x & & & x & & & & x & x & & x \\

 Refine\_Problem 

 Refine\_Problem

            &pblID & x  &    &    & x   &    &     &    & x    & x    &      & x \\

 &pblID & x & & & x & & & & x & x & & x \\

 Specify\_Method 

 Specify\_Method

         &metID & x  &    &    & x   &    &     &    & x    & x    &      & x \\

 &metID & x & & & x & & & & x & x & & x \\

 Apply\_Method 

 Apply\_Method

         &metID & x  & x  &    & x   &    &     &    & x    & x    &      & x \\

 &metID & x & x & & x & & & & x & x & & x \\

 Rewrite,\_Inst 

 Rewrite,\_Inst

         &thm   & x  & x  &    &     & x  &met  &    & x    &met   &      &   \\

 &thm & x & x & & & x &met & & x &met & & \\

         &thm   & x  & x  &    &     & x  &rls  &    & x    &rls   &      &   \\

 &thm & x & x & & & x &rls & & x &rls & & \\

         &thm   & x  & x  &    &     & x  &Rrls &    & x    &Rrls  &      &   \\

 &thm & x & x & & & x &Rrls & & x &Rrls & & \\

         &rls   & x  & x  &    &     &    &     & x  & x    & x    &      &   \\

 &rls & x & x & & & & & x & x & x & & \\

 Calculate  

 Calculate

         &op    & x  & x  &    &     &    &     &    &      &      & x    &   \\

 &op & x & x & & & & & & & & x & \\

 Substitute 

 Substitute

         &subs  & x  &    &    & x   &    &     &    &      &      &      &   \\

 &subs & x & & & x & & & & & & & \\

         &      &    &    &    &     &    &     &    &      &      &      &   \\

 & & & & & & & & & & & & \\

 SubProblem 

 SubProblem

         &spec  & x  & x  &    & x   &    &     &    & x    & x    &      & x \\

 &spec & x & x & & x & & & & x & x & & x \\

         &fmz   &    &    &    &     &    &     &    &      &      &      &   \\

 &fmz & & & & & & & & & & & \\

 \end{tabular}\end{center}\end{table}

 \end{tabular}\end{center}\end{table}}

 }

 \section{\isac's theories}

 \section{Die theories von \isac{}}

 \isac's theories build upon Isabelles theories for high-order-logic (HOL) up to the respective development of real numbers ({\tt HOL/Real}). Theories have a special format defined in \cite{Isa-ref} and the suffix {\tt *.thy}; usually theories are paired with SML-files having the same filename and the suffix {\tt *.ML}.

 Die theories von \isac{} basieren auf den theories f\"ur HOL und Real von Isabelle. Diese theories haben eine spezielle Form, die durch die Endung {\tt *.thy} definiert sind; normalerweise werden diese theories zusammen mit SML verwendet, und dann haben sie den selben Dateinamen, aber die Endung {\tt *.ML}.

 Die theories von \isac{} representieren den folgenden Teil vom Basiswissen von \isac{}, die Hierarchie von den zwei theories ist demnach strukturiert. Die {\tt *.ML} Dateien beinhalten {\em alle} Daten von den anderen zwei Hauptlinien des Basiswissens, die Probleme und die Methoden(ohne ihre jeweilige Struktur, die von den Problem Browsern und den Methode Browsern gemacht wird, zu pr\"asentieren.

 \isac's theories represent the deductive part of \isac's knowledge base, the hierarchy of theories is structured accordingly. The {\tt *.ML}-files, however, contain {\em all} data of the other two axes of the knowledge base, the problems and the methods (without presenting their respective structure, which is done by the problem browser and the method browser, see \ref{pbt}).

 Die Tab.\ref{theories} auf Seite \pageref{theories} listet die basis theories auf, die geplant sind in der Version \isac{} 1 angewendet zu werden. Wir erwarten, dass die Liste erweitert wird in n\"aherer Zukunft, und wir werden uns auch den theorie Browser genauer ansehen.

 Die ersten drei theories auf der Liste geh\"oren {\em nicht} zum Grundwissen von \isac{}; sie besch\"aftigen sich mit der Skriptsprache f\"ur Methoden und ist hier nur zur Vollst\"andigkeit angef\"uhrt.

 Tab.\ref{theories} on p.\pageref{theories} lists the basic theories planned to be implemented in version \isac.1. We expext the list to be expanded in the near future, actually, have a look to the theory browser~!

 The first three theories in the list do {\em not} belong to \isac's knowledge base; they are concerned with \isac's script-language for methods and listed here for completeness.

 \caption{Theories in \isac-version I} \label{theories}

 \caption{Theorien von der ersten Version von \isac} \label{theories}

 theory & description \\

 Theorie & Beschreibung \\

 & assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\

 & ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind zu, und (intermediatly~?) definiert einige weitere Listen von Funktionen\\

 & {\tt eval\_fn} for the additional list functions\\

 & {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\

 & functions required for the evaluation of scripts\\

 & Funktion, die f\"ur die Auswertung von Skripten ben\"otigt wird\\

 & the respective {\tt eval\_fn}s\\

 & bezieht sich auf {\tt eval\_fn}s\\

 & prerequisites for scripts: types, tactics, tacticals,\\

 & Vorraussetzung f\"ur Skripten: Typen, Taktiken, tacticals\\

 & sets of tactics and functions for internal use\\

 & eine Reihe von Taktiken und Funktionen f\"ur den internen Gebrauch\\

 & an intermediate hack for escaping type errors\\

 & fortgeschrittener Austritt, um den type Fehlern zu entkommen\\

 & {\it description}s for the formulas in {\it model}s and {\it problem}s\\

 & {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\

 & (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\

 & Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; Theorems f\"ur {\tt eval\_rls}\\

 & floating point numerals\\

 & Gleitkommerzahlendarstellung\\

 & basic notions for equations and equational systems\\

 & grunds\"atzliche Vorstellung f\"ur  Gleichungen und Gleichungssysteme\\

 & polynomials\\

 & Polynome\\

 & polynomial equations and equational systems \\

 & polynomiale Gleichungen und Gleichungssysteme \\

 & additional theorems for rationals\\

 & zus\"atzliche Theorems f\"ur Rationale Zahlen\\

 & cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\

 & abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\

 & equations on rationals\\

 & Gleichung mit rationalen Zahlen\\

 & radicals; calculate normalform; respective reverse rulesets\\

 & Radikanten; berechnen der Normalform; das betreffende umgekehrte Regelwerk\\

 & equations on roots\\

 & Gleichungen mit Wurzeln\\

 & equations on rationals and roots (i.e. on terms containing both operations)\\

 & Gleichungen mit rationalen Zahlen und Wurzeln (z.B. mit Termen, die beide Vorg\"ange enthalten)\\

 & vector analysis\\

 & Vektoren Analysis\\

 & trigonometriy\\

 & Trigonometrie\\

 & logarithms and exponential functions\\

 & Logarithmus und Exponentialfunktionen\\

 & nonstandard analysis\\

 & nicht der Norm entsprechende Analysis\\

 & differentiation\\

 & Differenzierung\\

 & applications of differentiaten (maxima-minima-problems)\\

 & Anwendungen beim Differenzieren (Maximum-Minimum-Probleme)\\

 & (old) data for the test suite\\

 & (alte) Daten f\"ur Testfolgen\\

 & collects all \isac-theoris.\\

 & enth\"alt alle Theorien von\isac{}\\

 \end{tabular}\end{center}\end{table}

 \end{tabular}\end{center}\end{table}}

 }

 \section{Daten in {\tt *.thy} und {\tt *.ML}}

 \section{Data in {\tt *.thy}- and {\tt *.ML}-files}

 Wie schon zuvor angesprochen, haben die arbeiten die theories von *.thy und *.ML zusamnmen und haben deswegen den selben Dateiname. Wie diese Daten zwischen den zwei Dateien verteilt werden wird in der

 As already mentioned, theories come in pairs of {\tt *.thy}- and {\tt *.ML}-files with the same respective filename. How data are distributed between the two files is shown in Tab.\ref{thy-ML} on p.\pageref{thy-ML}.

 Tab.\ref{thy-ML} auf Seite \pageref{thy-ML} gezeigt. Die Ordnung von den Dateinteilchen in den theories sollte an der Ordnung von der Liste festhalten.

 \caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML}

 \caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML}

 file & data & description \\

 Datei & Daten & Beschreibung \\

 & consts 

 & consts

 & operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}')

 & Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}')

 & rules  

 & rules

 & theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I}

 & theorems: \isac{} verwendet die Theorems von Isabelle, wenn m\"oglich; zus\"atzliche Theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt

 & {\tt theory' :=} 

 & {\tt theory' :=}

 & the theory defined by the actual {\tt *.thy}-file is made accessible to \isac

 & Die Theorie, die 

 abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht

 & evaluation function for operators and predicates, coded on the meta-level (SML); the identifier of such a function is a combination of the keyword {\tt eval\_} with the identifier of the function as defined in {\tt *.thy}

 & die Auswertungsfunktion f\"ur die Operatoren und Eigenschaften, kodiert im meta-Level (SML); die Bezeichnugn von so einer Funktion ist eine Kombination von Schl\"usselw\"ortern {\tt eval\_} und einer Bezeichnung von der Funktion, die in in {\tt *.thy} erkl\"art ist\\

 \\

 & {\tt *\_simplify}

 & {\tt *\_simplify} 

 & der automatisierte Vereinfacher f\"ur die tats\"achliche Theorie, z.B. die Bezeichnung von diesem Regelwerk ist eine Kombination aus den Theorienbezeichnungen und dem Schl\"usselwort {\tt *\_simplify}

 & the canonical simplifier for the actual theory, i.e. the identifier for this ruleset is a combination of the theories identifier and the keyword {\tt *\_simplify}

 & the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac

 & der automatisierte Vereinfacherthe {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac zug\"anglich ist

 & the same for rewrite orders, if needed outside of one particular ruleset

 & das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird

 & the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls})

 & dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls})

 & the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script)

 & dasselbe f\"ur {\tt eval\_fn}s, wenn es ausserhalb eines bestimmten Regelwerks gebraucht wird (wenn es ausserhalb eines bestimmten Regelwerks ben\"otigt wird) (z.B. f\"ur eine Taktik {\tt Calculate} in einem Skript)

 & problems defined within this {\tt *.ML}-file are made accessible for \isac

 & Probleme, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}

 & methods defined within this {\tt *.ML}-file are made accessible for \isac

 & Methoden, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}

 \end{tabular}\end{center}\end{table}

 \end{tabular}\end{center}\end{table}}

 }

 The order of the data-items within the theories should adhere to the order given in this list.

 \section{Formale Beschreibung der Hierarchie von Problemen}

 \section{Formal description of the problem-hierarchy}

 \section{Skripttaktiken}

 %for Richard Lang

 Tats\"achlich sind es die Taktiken, die die Berechnungen vorantreiben: im Hintergrund bauen sie den ''Prooftree`` und sie \"ubernehmen die wichtigsten Aufgaben w\"ahrend der Auswertung bei der der ''script-interpreter`` zur Steuerung des Benutzers transferiert wird. Hier beschreiben wir nur den Syntax von den Taktiken; die Semantik ist beschrieben etwas weiter unten im Kontext mit den Taktiken, die die Benutzer/Innen dieses Programmes verwenden: da gibt es einen Schriftverkehr zwischen den Benutzer Taktiken und den Skripttaktiken.

 \section{Script tactics}

 The tactics actually promote the calculation: they construct the prooftree behind the scenes, and they are the points during evaluation where the script-interpreter transfers control to the user. Here we only describe the sytax of the tactics; the semantics is described on p.\pageref{user-tactics} below in context with the tactics the student uses ('user-tactics'): there is a 1-to-1 correspondence between user-tactics and script-tactics.