1.1 --- a/doc-src/isac/mat-eng-de.tex Wed Jul 28 13:26:19 2010 +0200
1.2 +++ b/doc-src/isac/mat-eng-de.tex Thu Jul 29 14:12:11 2010 +0200
1.3 @@ -14,7 +14,7 @@
1.4 and\\[1.0ex]
1.5 Tools for Experiments in\\
1.6 Symbolic Computation\\[1.0ex]}
1.7 -\author{The \isac-Team\\
1.8 +\author{Alexandra Hirn und Eva Rott\\
1.9 \tt isac-users@ist.tugraz.at\\[1.0ex]}
1.10 \date{\today}
1.11
1.12 @@ -765,45 +765,37 @@
1.13
1.14
1.15 \chapter{Befehle von \isac{}}
1.16 -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.
1.17 -\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.
1.18 -\newline \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.
1.19 -\newline \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"u das Umformen.
1.20 -\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.
1.21 -\newline \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.
1.22 -\newline \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.
1.23 -\newline \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.
1.24 -\newline \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe eine method.
1.25 -\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``.
1.26 -\newline \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des Theorems, anstatt diese zu sch\"atzen.
1.27 -\newline \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von Theorems, dem rule set.
1.28 -\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.
1.29 +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.\
1.30 +\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.\
1.31 +\newline \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\
1.32 +\newline \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"u das Umformen.\
1.33 +\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.\
1.34 +\newline \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\
1.35 +\newline \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\
1.36 +\newline \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\
1.37 +\newline \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe eine method.\
1.38 +\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``.\
1.39 +\newline \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des Theorems, anstatt diese zu sch\"atzen.\
1.40 +\newline \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von Theorems, dem rule set.\
1.41 +\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.\
1.42 +\newline \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\
1.43 +\newline \textbf{Substitute substitution} f\"ugt substitution der momentanen Formel hinzu und wandelt es um.\
1.44 +\newline \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\
1.45 +\newline \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\
1.46 +\newline \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\
1.47 +\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.\
1.48 +\newline \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\
1.49 +\newline \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\
1.50 +\newline \textbf{Check\_postcond:} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim beenden des subproblem.\
1.51 +\newline \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.
1.52
1.53 +\section{Die Funktionsweise der mathematic engine}
1.54 +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.
1.55 +\newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird.
1.56 +{\footnotesize\begin{verbatim}
1.57 +??????????????????????????????????????????????????????????????????????????????????
1.58
1.59 -
1.60 -
1.61 -
1.62 -
1.63 -
1.64 -
1.65 -
1.66 -\newpage
1.67 -------------------------------- ALTER TEXT -------------------------------
1.68 -
1.69 -\chapter{Do a calculational proof}
1.70 -First we list all the tactics available so far (this list may be extended during further development of \isac).
1.71 -
1.72 -\section{Tactics for doing steps in calculations}
1.73 -\input{tactics}
1.74 -
1.75 -\section{The functionality of the math engine}
1.76 -A proof is being started in the math engine {\tt me} by the tactic
1.77 -\footnote{In the present version a tactic is of type {\tt mstep}.}
1.78 - {\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.
1.79 -
1.80 -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 ...
1.81 -{\footnotesize\begin{verbatim}
1.82 - ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
1.83 +ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
1.84 "errorBound (eps=#0)","solutions L"];
1.85 val fmz =
1.86 ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
1.87 @@ -814,16 +806,14 @@
1.88 val dom = "SqRoot.thy" : string
1.89 val pbt = ["univariate","equation"] : string list
1.90 val met = ("SqRoot.thy","no_met") : string * string
1.91 -\end{verbatim}}%size
1.92 -... 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.
1.93 +\end{verbatim}
1.94
1.95 -Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.
1.96 -
1.97 -
1.98 -\section{Initialize the calculation}
1.99 -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.
1.100 -{\footnotesize\begin{verbatim}
1.101 - ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
1.102 +\section{Der Beginn einer Rechnung}
1.103 +Um einen neuen proof beginnen zu k\"onnen, werden folgende Schritte durchgef\"uhrt:
1.104 +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.
1.105 +\footnotesize\begin{verbatim}
1.106 +????????????????????????????????????????????????????????????????????????????????????????????
1.107 +ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
1.108 val mID = "Init_Proof" : string
1.109 val m =
1.110 Init_Proof
1.111 @@ -840,11 +830,10 @@
1.112 (PblObj
1.113 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.114 result=#,spec=#},[]) : ptree
1.115 - \end{verbatim}}%size
1.116 -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'}).
1.117 -
1.118 -We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
1.119 -{\footnotesize\begin{verbatim}
1.120 +\end{verbatim}
1.121 +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.
1.122 +\footnotesize\begin{verbatim}
1.123 +?????????????????????????????????????????????????????????????????????????????????????????????
1.124 ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
1.125 val it = () : unit
1.126 ML>
1.127 @@ -857,13 +846,9 @@
1.128 {Find=[Incompl "solutions []"],
1.129 Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
1.130 Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
1.131 -\end{verbatim}}%size
1.132 -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).\\
1.133 -
1.134 -{\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\
1.135 -
1.136 -In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.
1.137 +\end{verbatim}
1.138 {\footnotesize\begin{verbatim}
1.139 +?????????????????????????????????????????????????????????????????????????????????????????????
1.140 ML> nxt;
1.141 val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1.142 : string * mstep
1.143 @@ -873,13 +858,12 @@
1.144 : string * mstep
1.145 ML>
1.146 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.147 -\end{verbatim}}%size
1.148 +\end{verbatim}
1.149
1.150 -
1.151 -\section{The phase of modeling}
1.152 -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}.
1.153 -
1.154 +\section{The phase of modeling}
1.155 +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.
1.156 {\footnotesize\begin{verbatim}
1.157 +?????????????????????????????????????????????????????????????????????????????????????????????
1.158 ML> nxt;
1.159 val it =
1.160 ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
1.161 @@ -893,9 +877,9 @@
1.162 ML>
1.163 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.164 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1.165 -\end{verbatim}}%size
1.166 -\noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more.
1.167 +\end{verbatim}
1.168 {\footnotesize\begin{verbatim}
1.169 +?????????????????????????????????????????????????????????????????????????????????????????????
1.170 ML> Compiler.Control.Print.printDepth:=8;
1.171 ML> f;
1.172 val it =
1.173 @@ -906,13 +890,14 @@
1.174 {Find=[Correct "solutions L"],
1.175 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.176 Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
1.177 -\end{verbatim}}%size
1.178 -%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.
1.179 +\end{verbatim}
1.180
1.181 -\section{The phase of specification}
1.182 -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.
1.183 +
1.184 +\section{The phase of specification}
1.185 +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.
1.186 {\footnotesize\begin{verbatim}
1.187 -ML> nxt;
1.188 +??????????????????????????????????????????????????????????????????????????????????????????
1.189 + ML> nxt;
1.190 val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
1.191 ML>
1.192 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.193 @@ -924,9 +909,10 @@
1.194 (PblObj
1.195 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.196 result=#,spec=#},[]) : ptree
1.197 -\end{verbatim}}%size
1.198 -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.
1.199 +\end{verbatim}
1.200 +Die {\tt me} erkennt den richtigen Problem type und arbeitet so weiter:
1.201 {\footnotesize\begin{verbatim}
1.202 +?????????????????????????????????????????????????????????????????????????????????????????
1.203 ML> val nxt = ("Specify_Problem",
1.204 Specify_Problem ["polynomial","univariate","equation"]);
1.205 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.206 @@ -949,9 +935,10 @@
1.207 Where=[False
1.208 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1.209 With=[]}))) : mout
1.210 -\end{verbatim}}%size
1.211 -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"]}.
1.212 +\end{verbatim}
1.213 +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``].
1.214 {\footnotesize\begin{verbatim}
1.215 +????????????????????????????????????????????????????????????????????????????????????????????
1.216 ML> val nxt = ("Refine_Problem",
1.217 Refine_Problem ["linear","univariate","equation
1.218 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.219 @@ -1005,11 +992,12 @@
1.220 {Find=[Correct "solutions L"],
1.221 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.222 Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
1.223 -\end{verbatim}}%size
1.224 -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~!
1.225 +\end{verbatim}
1.226 +Die tactic {\tt Refine\_Problem} wandelt alle matches wieder in problem types um und sucht in der problem hierachy weiter.
1.227
1.228 -\section{The phase of solving}
1.229 -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}:
1.230 +
1.231 +\section{The phase of solving}
1.232 +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}:
1.233 {\footnotesize\begin{verbatim}
1.234 ML> nxt;
1.235 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
1.236 @@ -1031,8 +1019,8 @@
1.237 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.238 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
1.239 val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
1.240 -\end{verbatim}}%size
1.241 -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:
1.242 +\end{verbatim}
1.243 +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:
1.244 {\footnotesize\begin{verbatim}
1.245 ML> nxt;
1.246 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1.247 @@ -1046,16 +1034,13 @@
1.248 ML>
1.249 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.250 val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
1.251 -\end{verbatim}}%size
1.252 -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.
1.253 +\end{verbatim}
1.254 +{\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.
1.255 +Nun folgt erneut die phase of modeling und die phase of specification.
1.256
1.257 -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.
1.258 -
1.259 -
1.260 -\section{The final phase: check the post-condition}
1.261 -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.
1.262 -
1.263 -Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem:
1.264 +\section{The final phase: \"Uberpr\"ufung der ''post-condition``}
1.265 +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.
1.266 +Dadurch wird die post-condition im folgenden Beispiel als problem und subproblem erw\"ahnt.
1.267 {\footnotesize\begin{verbatim}
1.268 ML> nxt;
1.269 val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
1.270 @@ -1068,262 +1053,256 @@
1.271 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.272 val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
1.273 val nxt = ("End_Proof'",End_Proof') : string * mstep
1.274 -\end{verbatim}}%size
1.275 -The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\
1.276 +\end{verbatim}
1.277 +Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\
1.278
1.279 -{\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~!}
1.280 +{\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!}
1.281
1.282
1.283 +\part{Systematische Beschreibung}
1.284
1.285 -\part{Systematic description}
1.286 +\chapter{Die Struktur des Grundlagenwissens}
1.287
1.288 +\section{Taktiken und Daten}
1.289 +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.
1.290 +Diese Teile sind in alphabetischer Anordnung in Tab.\ref{kb-items} auf Seite \pageref{kb-items} aufgelistet.
1.291
1.292 -\chapter{The structure of the knowledge base}
1.293 -
1.294 -\section{Tactics and data}
1.295 -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
1.296 -\footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.}
1.297 -. The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}.
1.298 {\begin{table}[h]
1.299 -\caption{Atomic items of the KB} \label{kb-items}
1.300 +\caption{Kleinste Teilchen des KB} \label{kb-items}
1.301 %\tabcolsep=0.3mm
1.302 \begin{center}
1.303 \def\arraystretch{1.0}
1.304 \begin{tabular}{lp{9.0cm}}
1.305 -abbrevation & description \\
1.306 +Abk\"urzung & Beschreibung \\
1.307 \hline
1.308 &\\
1.309 {\it calc\_list}
1.310 -& associationlist of the evaluation-functions {\it eval\_fn}\\
1.311 +& gesammelte Liste von allen ausgewerteten Funktionen {\it eval\_fn}\\
1.312 {\it eval\_fn}
1.313 -& evaluation-function for numerals and for predicates coded in SML\\
1.314 -{\it eval\_rls }
1.315 -& ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\
1.316 +& ausgewertete Funktionen f\"r Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\
1.317 +{\it eval\_rls }
1.318 +& Regelsatz {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\
1.319 {\it fmz}
1.320 -& formalization, i.e. a minimal formula representation of an example \\
1.321 +& Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\
1.322 {\it met}
1.323 -& a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\
1.324 +& eine Methode d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer Phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\
1.325 {\it metID}
1.326 -& reference to a {\it met}\\
1.327 +& bezieht sich auf {\it met}\\
1.328 {\it op}
1.329 -& operator as key to an {\it eval\_fn} in a {\it calc\_list}\\
1.330 +& ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\
1.331 {\it pbl}
1.332 -& problem, i.e. a node in the problem-hierarchy\\
1.333 +& Problem d.h. der Knotenpunkt in der Hierarchie von Problemen\\
1.334 {\it pblID}
1.335 -& reference to a {\it pbl}\\
1.336 +& bezieht sich auf {\it pbl}\\
1.337 {\it rew\_ord}
1.338 -& rewrite-order\\
1.339 +& Anordnung beim Rewriting\\
1.340 {\it rls}
1.341 -& ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\
1.342 +& Regelsatz, d.h. eine Datenstruktur, die Theoremss {\it thm} und Operatoren {\it op} zur Vereinfachuing (mit {\it rew\_ord}) enth\"alt \\
1.343 {\it Rrls}
1.344 -& ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\
1.345 +& Regelsatz f\"ur das 'reverse rewriting' (eine \isac-Technik, die das schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
1.346 {\it scr}
1.347 -& script describing algorithms by tactics, part of a {\it met} \\
1.348 +& Skript, das die Algorithmen durch Anwenden von Taktiken beschreibt und ein Teil von {\it met} ist \\
1.349 {\it norm\_rls}
1.350 -& special ruleset calculating a normalform, associated with a {\it thy}\\
1.351 +& spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\
1.352 {\it spec}
1.353 -& specification, i.e. a tripel ({\it thyID, pblID, metID})\\
1.354 +& Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\
1.355 {\it subs}
1.356 -& substitution, i.e. a list of variable-value-pairs\\
1.357 +& Ersatz, z.B. eine Liste von Variablen und ihren jeweiligen Werten\\
1.358 {\it term}
1.359 -& Isabelle term, i.e. a formula\\
1.360 +& Term von Isabelle, z.B. eine Formel\\
1.361 {\it thm}
1.362 -& theorem\\
1.363 +& theorem\\
1.364 {\it thy}
1.365 -& theory\\
1.366 +& Theorie\\
1.367 {\it thyID}
1.368 -& reference to a {\it thy} \\
1.369 -\end{tabular}\end{center}\end{table}
1.370 -}
1.371 -The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}.
1.372 -{\def\arraystretch{1.2}
1.373 +& im Bezug auf {\it thy} \\
1.374 +\end{tabular}\end{center}\end{table}}
1.375 +
1.376 +Die Verbindung zwischen Taktiken und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.
1.377 +
1.378 +
1.379 \begin{table}[h]
1.380 -\caption{Which tactic uses which KB's item~?} \label{tac-kb}
1.381 +\caption{Welche Taktiken verwenden die Teile des KB~?} \label{tac-kb}
1.382 \tabcolsep=0.3mm
1.383 \begin{center}
1.384 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1.385 -tactic &input & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1.386 - & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1.387 +Taktik &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1.388 +& &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1.389 \hline\hline
1.390 Init\_Proof
1.391 - &fmz & x & & & x & & & & & & & x \\
1.392 - &spec & & & & & & & & & & & \\
1.393 +&fmz & x & & & x & & & & & & & x \\
1.394 +&spec & & & & & & & & & & & \\
1.395 \hline
1.396 \multicolumn{13}{|l|}{model phase}\\
1.397 \hline
1.398 -Add\_* &term & x & & & x & & & & & & & x \\
1.399 -FormFK &model & x & & & x & & & & & & & x \\
1.400 +Add\_*
1.401 +&term & x & & & x & & & & & & & x \\
1.402 +FormFK &model & x & & & x & & & & & & & x \\
1.403 \hline
1.404 \multicolumn{13}{|l|}{specify phase}\\
1.405 \hline
1.406 -Specify\_Theory
1.407 - &thyID & x & & & x & & & & x & x & & x \\
1.408 -Specify\_Problem
1.409 - &pblID & x & & & x & & & & x & x & & x \\
1.410 -Refine\_Problem
1.411 - &pblID & x & & & x & & & & x & x & & x \\
1.412 -Specify\_Method
1.413 - &metID & x & & & x & & & & x & x & & x \\
1.414 -Apply\_Method
1.415 - &metID & x & x & & x & & & & x & x & & x \\
1.416 +Specify\_Theory
1.417 +&thyID & x & & & x & & & & x & x & & x \\
1.418 +Specify\_Problem
1.419 +&pblID & x & & & x & & & & x & x & & x \\
1.420 +Refine\_Problem
1.421 +&pblID & x & & & x & & & & x & x & & x \\
1.422 +Specify\_Method
1.423 +&metID & x & & & x & & & & x & x & & x \\
1.424 +Apply\_Method
1.425 +&metID & x & x & & x & & & & x & x & & x \\
1.426 \hline
1.427 \multicolumn{13}{|l|}{solve phase}\\
1.428 \hline
1.429 -Rewrite,\_Inst
1.430 - &thm & x & x & & & x &met & & x &met & & \\
1.431 +Rewrite,\_Inst
1.432 +&thm & x & x & & & x &met & & x &met & & \\
1.433 Rewrite, Detail
1.434 - &thm & x & x & & & x &rls & & x &rls & & \\
1.435 +&thm & x & x & & & x &rls & & x &rls & & \\
1.436 Rewrite, Detail
1.437 - &thm & x & x & & & x &Rrls & & x &Rrls & & \\
1.438 +&thm & x & x & & & x &Rrls & & x &Rrls & & \\
1.439 Rewrite\_Set,\_Inst
1.440 - &rls & x & x & & & & & x & x & x & & \\
1.441 -Calculate
1.442 - &op & x & x & & & & & & & & x & \\
1.443 -Substitute
1.444 - &subs & x & & & x & & & & & & & \\
1.445 - & & & & & & & & & & & & \\
1.446 -SubProblem
1.447 - &spec & x & x & & x & & & & x & x & & x \\
1.448 - &fmz & & & & & & & & & & & \\
1.449 +&rls & x & x & & & & & x & x & x & & \\
1.450 +Calculate
1.451 +&op & x & x & & & & & & & & x & \\
1.452 +Substitute
1.453 +&subs & x & & & x & & & & & & & \\
1.454 +& & & & & & & & & & & & \\
1.455 +SubProblem
1.456 +&spec & x & x & & x & & & & x & x & & x \\
1.457 +&fmz & & & & & & & & & & & \\
1.458 \hline
1.459 -\end{tabular}\end{center}\end{table}
1.460 -}
1.461 +\end{tabular}\end{center}\end{table}}
1.462
1.463 -\section{\isac's theories}
1.464 -\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}.
1.465
1.466 -\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}).
1.467 +\section{Die theories von \isac{}}
1.468 +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}.
1.469 +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.
1.470 +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.
1.471 +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.
1.472
1.473 -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~!
1.474 -
1.475 -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.
1.476 {\begin{table}[h]
1.477 -\caption{Theories in \isac-version I} \label{theories}
1.478 +\caption{Theorien von der ersten Version von \isac} \label{theories}
1.479 %\tabcolsep=0.3mm
1.480 \begin{center}
1.481 \def\arraystretch{1.0}
1.482 \begin{tabular}{lp{9.0cm}}
1.483 -theory & description \\
1.484 +Theorie & Beschreibung \\
1.485 \hline
1.486 &\\
1.487 ListI.thy
1.488 -& assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\
1.489 +& ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind zu, und (intermediatly~?) definiert einige weitere Listen von Funktionen\\
1.490 ListI.ML
1.491 -& {\tt eval\_fn} for the additional list functions\\
1.492 +& {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\
1.493 Tools.thy
1.494 -& functions required for the evaluation of scripts\\
1.495 +& Funktion, die f\"ur die Auswertung von Skripten ben\"otigt wird\\
1.496 Tools.ML
1.497 -& the respective {\tt eval\_fn}s\\
1.498 +& bezieht sich auf {\tt eval\_fn}s\\
1.499 Script.thy
1.500 -& prerequisites for scripts: types, tactics, tacticals,\\
1.501 +& Vorraussetzung f\"ur Skripten: Typen, Taktiken, tacticals\\
1.502 Script.ML
1.503 -& sets of tactics and functions for internal use\\
1.504 +& eine Reihe von Taktiken und Funktionen f\"ur den internen Gebrauch\\
1.505 & \\
1.506 \hline
1.507 & \\
1.508 Typefix.thy
1.509 -& an intermediate hack for escaping type errors\\
1.510 +& fortgeschrittener Austritt, um den type Fehlern zu entkommen\\
1.511 Descript.thy
1.512 -& {\it description}s for the formulas in {\it model}s and {\it problem}s\\
1.513 +& {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\
1.514 Atools
1.515 -& (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\
1.516 +& Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; Theorems f\"ur {\tt eval\_rls}\\
1.517 Float
1.518 -& floating point numerals\\
1.519 +& Gleitkommerzahlendarstellung\\
1.520 Equation
1.521 -& basic notions for equations and equational systems\\
1.522 +& grunds\"atzliche Vorstellung f\"ur Gleichungen und Gleichungssysteme\\
1.523 Poly
1.524 -& polynomials\\
1.525 +& Polynome\\
1.526 PolyEq
1.527 -& polynomial equations and equational systems \\
1.528 +& polynomiale Gleichungen und Gleichungssysteme \\
1.529 Rational.thy
1.530 -& additional theorems for rationals\\
1.531 +& zus\"atzliche Theorems f\"ur Rationale Zahlen\\
1.532 Rational.ML
1.533 -& cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\
1.534 +& abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\
1.535 RatEq
1.536 -& equations on rationals\\
1.537 +& Gleichung mit rationalen Zahlen\\
1.538 Root
1.539 -& radicals; calculate normalform; respective reverse rulesets\\
1.540 +& Radikanten; berechnen der Normalform; das betreffende umgekehrte Regelwerk\\
1.541 RootEq
1.542 -& equations on roots\\
1.543 +& Gleichungen mit Wurzeln\\
1.544 RatRootEq
1.545 -& equations on rationals and roots (i.e. on terms containing both operations)\\
1.546 +& Gleichungen mit rationalen Zahlen und Wurzeln (z.B. mit Termen, die beide Vorg\"ange enthalten)\\
1.547 Vect
1.548 -& vector analysis\\
1.549 +& Vektoren Analysis\\
1.550 Trig
1.551 -& trigonometriy\\
1.552 +& Trigonometrie\\
1.553 LogExp
1.554 -& logarithms and exponential functions\\
1.555 +& Logarithmus und Exponentialfunktionen\\
1.556 Calculus
1.557 -& nonstandard analysis\\
1.558 +& nicht der Norm entsprechende Analysis\\
1.559 Diff
1.560 -& differentiation\\
1.561 +& Differenzierung\\
1.562 DiffApp
1.563 -& applications of differentiaten (maxima-minima-problems)\\
1.564 +& Anwendungen beim Differenzieren (Maximum-Minimum-Probleme)\\
1.565 Test
1.566 -& (old) data for the test suite\\
1.567 +& (alte) Daten f\"ur Testfolgen\\
1.568 Isac
1.569 -& collects all \isac-theoris.\\
1.570 -\end{tabular}\end{center}\end{table}
1.571 -}
1.572 +& enth\"alt alle Theorien von\isac{}\\
1.573 +\end{tabular}\end{center}\end{table}}
1.574
1.575
1.576 -\section{Data in {\tt *.thy}- and {\tt *.ML}-files}
1.577 -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}.
1.578 +\section{Daten in {\tt *.thy} und {\tt *.ML}}
1.579 +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
1.580 +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.
1.581 +
1.582 {\begin{table}[h]
1.583 -\caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML}
1.584 +\caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML}
1.585 \tabcolsep=2.0mm
1.586 \begin{center}
1.587 \def\arraystretch{1.0}
1.588 \begin{tabular}{llp{7.7cm}}
1.589 -file & data & description \\
1.590 +Datei & Daten & Beschreibung \\
1.591 \hline
1.592 & &\\
1.593 {\tt *.thy}
1.594 -& consts
1.595 -& operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}')
1.596 +& consts
1.597 +& Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}')
1.598 \\
1.599 -& rules
1.600 -& theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I}
1.601 +& rules
1.602 +& theorems: \isac{} verwendet die Theorems von Isabelle, wenn m\"oglich; zus\"atzliche Theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt
1.603 \\& &\\
1.604 {\tt *.ML}
1.605 -& {\tt theory' :=}
1.606 -& the theory defined by the actual {\tt *.thy}-file is made accessible to \isac
1.607 +& {\tt theory' :=}
1.608 +& Die Theorie, die
1.609 +abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht
1.610 \\
1.611 & {\tt eval\_fn}
1.612 -& 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}
1.613 -\\
1.614 -& {\tt *\_simplify}
1.615 -& 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}
1.616 +& 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\\
1.617 +& {\tt *\_simplify}
1.618 +& 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}
1.619 \\
1.620 & {\tt norm\_rls :=}
1.621 -& the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac
1.622 +& der automatisierte Vereinfacherthe {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac zug\"anglich ist
1.623 \\
1.624 & {\tt rew\_ord' :=}
1.625 -& the same for rewrite orders, if needed outside of one particular ruleset
1.626 +& das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird
1.627 \\
1.628 & {\tt ruleset' :=}
1.629 -& the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls})
1.630 +& dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls})
1.631 \\
1.632 & {\tt calc\_list :=}
1.633 -& the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script)
1.634 +& 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)
1.635 \\
1.636 & {\tt store\_pbl}
1.637 -& problems defined within this {\tt *.ML}-file are made accessible for \isac
1.638 +& Probleme, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}
1.639 \\
1.640 & {\tt methods :=}
1.641 -& methods defined within this {\tt *.ML}-file are made accessible for \isac
1.642 +& Methoden, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}
1.643 \\
1.644 -\end{tabular}\end{center}\end{table}
1.645 -}
1.646 -The order of the data-items within the theories should adhere to the order given in this list.
1.647 +\end{tabular}\end{center}\end{table}}
1.648
1.649 -\section{Formal description of the problem-hierarchy}
1.650 -%for Richard Lang
1.651 +\section{Formale Beschreibung der Hierarchie von Problemen}
1.652
1.653 -\section{Script tactics}
1.654 -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.
1.655 -
1.656 -
1.657 +\section{Skripttaktiken}
1.658 +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.
1.659
1.660
1.661