doc-isac/mat-eng-de.tex
author wneuper <Walther.Neuper@jku.at>
Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787 26037efefd61
parent 60650 06ec8abfd3bc
permissions -rw-r--r--
Doc/Specify_Phase 2: copy finished
     1 \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
     2 \usepackage{latexsym} 
     3 
     4 %\usepackage{ngerman}
     5 %\grmn@dq@error ...and \dq \string #1 is undefined}
     6 %l.989 ...tch the problem type \\{\tt["squareroot",
     7 %                                                  "univ
     8 \bibliographystyle{alpha}
     9 
    10 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    11 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    12 
    13 \title{\isac \\
    14   Experimente zur Computermathematik\\[1.0ex]
    15   und\\[1.0ex]
    16   Handbuch f\"ur Autoren der\\
    17   Mathematik-Wissensbasis\\[1.0ex]}
    18 \author{Alexandra Hirn und Eva Rott\\
    19   \tt isac-users@ist.tugraz.at\\[1.0ex]}
    20 \date{\today}
    21 
    22 \begin{document}
    23 \maketitle
    24 \newpage
    25 \tableofcontents
    26 \newpage
    27 \listoftables
    28 \newpage
    29 
    30 \chapter{Einleitung}
    31 Dies ist die \"Ubersetzung der dersten Kapitel einer englischen Version \footnote{http://www.ist.tugraz.at/projects/isac/publ/mat-eng.pdf}, auf den Stand von \sisac{} 2008 gebracht. Die \"Ubersetzung und Anpassung erfolgte durch die Autorinnen im Rahmen einer Ferialpraxis am Institut f\"ur Softwaretechnologie der TU Graz.
    32 
    33 Diese Version zeichnet sich dadurch aus, dass sie von ``Nicht-Computer-Freaks''  f\"ur ``Nicht-Computer-Freaks'' geschrieben wurde.
    34 
    35 \section{``Authoring'' und ``Tutoring''}
    36 \paragraph{TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
    37 Die Grundlage f\"ur \isac{} bildet Isabelle. Dies ist ein ``theorem prover'', der von L. Paulson und T. Nipkow entwickelt wird und Hard- und Software pr\"uft.
    38 \section{Der Inhalt des Dokuments}
    39 \paragraph{TO DO} {Als Anleitung:} Dieses Dokument beschreibt das Kerngebiet (KE) von \isac{}, das Gebiet der mathematics engine (ME) im Kerngebiet und die verschiedenen Funktionen wie das Umschreiben und der Vergleich.
    40 
    41 \isac{} und KE wurden in SML geschrieben, die Sprache in Verbindung mit dem Vorg\"anger des theorem Provers Isabelle entwickelt. So kam es, dass in diesem Dokument die Ebene ASCII als SML Code pr\"asentiert wird. Der Leser wird vermutlich erkennen, dass der \isac{} Benutzer eine vollkommen andere Sichtweise auf eine grafische Benutzeroberfl\"ache bekommt.
    42 
    43 Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (f\"ur eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
    44 
    45 %The interfaces will be moderately exended during the first phase of development of the mathematics knowledge. The work on the subprojects defined should {\em not} create interfaces of any interest to a user or another author of knowledge except identifiers (of type string) for theorems, rulesets etc.
    46 
    47 Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell.
    48 
    49 \paragraph{Versuchen Sie es!}  Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.
    50 
    51 \section{Gleich am Computer ausprobieren!}\label{get-started}
    52 \paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben:
    53 \begin{itemize}
    54  \item System starten
    55  \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.
    56  \item $>$  :  Hinter diesem Zeichen (``Prompt'') stehen jene, die Sie selbst eingeben bzw. mit Copy und Paste aus der Datei kopieren.
    57  \item Die Eingabe wird mit ``;'' und ``Enter'' abgeschlossen.
    58  \item Zeilen, die nicht mit Prompt beginnen, werden vom Computer ausgegeben.
    59  
    60 \end{itemize}
    61 
    62 \part{Experimentelle Ann\"aherung}
    63 
    64 \chapter{Terme und Theorien}
    65 Wie bereits erw\"ahnt, geht es um Computer-Mathematik. In den letzten Jahren hat die ``computer science'' grosse Fortschritte darin gemacht, Mathematik auf dem Computer verst\"andlich darzustellen. Dies gilt f\"ur mathematische Formeln, f\"ur die Beschreibung von Problemen, f\"ur L\"osungsmethoden etc. Wir beginnen mit mathematischen Formeln.
    66 
    67 \section{Von der Formel zum Term}
    68 Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:
    69 {\footnotesize\begin{verbatim}
    70    > "a + b * 3";
    71       val it = "a + b * 3" : string
    72 \end{verbatim}}
    73 \noindent ``a + b * 3'' ist also ein string (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt TermC.parse_test @{context}} (string to term) umrechnen:
    74 {\footnotesize\begin{verbatim}
    75    > TermC.parse_test @{context} "a + b * 3";
    76       val it =
    77          Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
    78                Free ("a", "RealDef.real") $
    79             (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
    80                ...) : Term.term
    81 \end{verbatim}}
    82 \noindent Diese Form heisst {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Isabelle braucht sie aber intern zum Rechnen. Wir wollen sie mit Hilfe von {\tt val} (value) auf der Variable {\tt t} speichern:
    83 {\footnotesize\begin{verbatim}
    84    > val t = TermC.parse_test @{context} "a + b * 3";
    85       val t =  
    86          Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
    87                Free ("a", "RealDef.real") $
    88             (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
    89                ...) : Term.term
    90 \end{verbatim}}
    91 Von dieser Variablen {\tt t} kann man den Wert jederzeit abrufen:
    92 {\footnotesize\begin{verbatim}
    93    > t;
    94       val it =
    95          Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
    96                Free ("a", "RealDef.real") $
    97             (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
    98                ...) : Term.term
    99 \end{verbatim}}
   100 Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt TermC.atom_trace_detail @{context}} \"ubergeben werden, die diesen in einer dritten Form zeigt:
   101 {\footnotesize\begin{verbatim}
   102    > TermC.atom_trace_detail \@\{context\} term;
   103  
   104    ***
   105    *** Const (op +, [real, real] => real)
   106    *** . Free (a, real)
   107    *** . Const (op *, [real, real] => real)
   108    *** . . Free (b, real)
   109    *** . . Free (3, real)
   110    ***
   111  
   112    val it = () : unit
   113 \end{verbatim}}
   114 Diese Darstellung nennt man ``abstract syntax'' und macht unmittelbar klar, dass man a und b nicht addieren kann, weil ein Mal vorhanden ist.
   115 \newline Es gibt noch eine vierte Art von Term, den cterm. Er wird weiter unten verwendet, weil er sich als string lesbar darstellt.
   116 
   117 \section{``Theory'' und ``Parsing``}
   118 Der Unterschied zwischen \isac{} und bisheriger Mathematiksoftware (GeoGebra, Mathematica, Maple, Derive etc.) ist, dass das mathematische Wissen nicht im Programmcode steht, sondern in sogenannten theories (Theorien).
   119 Dort wird das Mathematikwissen in einer f\"ur nicht Programmierer lesbaren Form geschrieben. Das Wissen von \isac{} ist in folgenden Theorien entahlten:
   120 {\footnotesize\begin{verbatim}
   121    > Isac.thy;
   122       val it =
   123          {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
   124          Sum_Type, Relation, Record, Inductive, Transitive_Closure,
   125          Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
   126          SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
   127          Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
   128          IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
   129          Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
   130          RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
   131          Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
   132          Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
   133          Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
   134          Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
   135          AlgEin, Test, Isac} : Theory.theory
   136 \end{verbatim}}
   137 {\tt ProtoPure} und {\tt CPure} enthalten diese logischen Grundlagen, die in {\tt HOL} und den nachfolgenden Theorien erweitert werden. \isac{} als letzte Theorie beinhaltet das gesamte Wissen.
   138 Dass das Mal vor dem Plus berechnet wird, ist so festgelegt:
   139 {\footnotesize\begin{verbatim}
   140    class plus =
   141    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
   142 
   143    class minus =
   144    fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
   145 
   146    class uminus =
   147    fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
   148 
   149    class times =
   150    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 
   151 \end{verbatim}}
   152 {\tt infix} gibt an, dass der Operator zwischen den Zahlen steht und nicht, wie in ''abstract syntax``, vorne oben.
   153 Die Zahlen rechts davon legen die Priorit\"at fest. 70 f\"ur Mal ist gr\"osser als 65 f\"ur Plus und wird daher zuerst berechnet.
   154 
   155 Wollen Sie wissen, wie die einzelnen Rechengesetze aussehen, k\"onnen Sie im Internet folgenden Link ansehen: http://isabelle.in.tum.de/dist/library/HOL/Groups.html
   156 
   157 \paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt TermC.parse_test @{context}} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.
   158 {\footnotesize\begin{verbatim}
   159    > parse Isac.thy "a + b";
   160       val it = Some "a + b" : Thm.cterm Library.option
   161 \end{verbatim}}
   162 Um sich das Weiterrechnen zu erleichtern, kann das Ergebnis vom Parsing auf eine Variable, wie zum Beispiel {\tt t} gespeichert werden:
   163 {\footnotesize\begin{verbatim}
   164    > val t = parse Isac.thy "a + b";
   165       val t = Some "a + b" : Thm.cterm Library.option
   166 \end{verbatim}}
   167 {\tt Some} bedeutet, dass das n\"otige Wissen vorhanden ist, um die Rechnung durchzuf\"uhren. {\tt None} zeigt uns, dass das Wissen fehlt oder ein Fehler aufgetreten ist. Daher sieht man im folgenden Beispiel, dass {\tt HOL.thy} nicht ausreichend Wissen enth\"alt:
   168 {\footnotesize\begin{verbatim}
   169    > parse HOL.thy "a + b";
   170       val it = None : Thm.cterm Library.option
   171 \end{verbatim}}
   172 Anschliessend zeigen wir Ihnen noch ein zweites Beispiel, bei dem sowohl ein Fehler aufgetreten ist, als auch das Wissen fehlt:
   173 {\footnotesize\begin{verbatim}
   174    > parse Isac.thy "a + ";
   175       *** Inner syntax error: unexpected end of input
   176       *** Expected tokens: "contains_root" "is_root_free" "q_" "M_b" "M_b'"
   177       *** "Integral" "differentiate" "E_" "some_of" "||" "|||" "argument_in"
   178       *** "filter_sameFunId" "I__" "letpar" "Rewrite_Inst" "Rewrite_Set"
   179       *** "Rewrite_Set_Inst" "Check_elementwise" "Or_to_List" "While" "Script"
   180       *** "\\" "\\" "\\" "CHR" "xstr" "SOME" "\\" "@"
   181       *** "GREATEST" "[" "[]" "num" "\\" "{)" "{.." "\\" "(|"
   182       *** "\\" "SIGMA" "()" "\\" "PI" "\\" "\\" "{" "INT"
   183       *** "UN" "{}" "LEAST" "\\" "0" "1" "-" "!" "?" "?!" "\\"
   184       *** "\\" "\\" "\\!" "THE" "let" "case" "~" "if" "ALL"
   185       *** "EX" "EX!" "!!" "_" "\\" "\\" "PROP" "[|" "OFCLASS"
   186       *** "\\" "op" "\\" "%" "TYPE" "id" "longid" "var" "..."
   187       *** "\\" "("
   188       val it = None : Thm.cterm Library.option
   189 \end{verbatim}}
   190 
   191 Das mathematische Wissen w\"achst mit jeder Theorie von ProtoPure bis Isac. In den folgenden Beispielen wird gezeigt, wie das Wissen w\"achst.
   192 
   193 {\footnotesize\begin{verbatim}
   194    > (*-1-*);
   195    > parse HOL.thy "2^^^3";
   196       *** Inner lexical error at: "^^^3"
   197       val it = None : Thm.cterm Library.option         
   198 \end{verbatim}}
   199 ''Inner lexical error`` und ''None`` bedeuten, dass ein Fehler aufgetreten ist, denn das Wissen \"uber {\tt *} findet sich erst in der {\tt theorie group}.
   200 
   201 {\footnotesize\begin{verbatim}
   202    > (*-2-*);
   203    > parse HOL.thy "d_d x (a + x)";
   204       val it = None : Thm.cterm Library.option               
   205 \end{verbatim}}
   206 Hier wiederum ist noch kein Wissen \"uber das Differenzieren vorhanden.
   207 
   208 {\footnotesize\begin{verbatim}
   209    > (*-3-*);
   210    > parse Rational.thy "2^^^3";
   211       val it = Some "2 ^^^ 3" : Thm.cterm Library.option               
   212 \end{verbatim}}
   213 
   214 {\footnotesize\begin{verbatim}
   215    > (*-4-*);
   216    > val Some t4 = parse Rational.thy "d_d x (a + x)";
   217       val t4 = "d_d x (a + x)" : Thm.cterm              
   218 \end{verbatim}}
   219 
   220 {\footnotesize\begin{verbatim}
   221    > (*-5-*);
   222    > val Some t5 = parse Diff.thy  "d_d x (a + x)";
   223       val t5 = "d_d x (a + x)" : Thm.cterm             
   224 \end{verbatim}}
   225 Die letzen drei Aufgaben k\"onnen schon gel\"ost werden, da {\tt Rational.thy} \"uber das n\"otige Wissen verf\"ugt.
   226 
   227 \section{Details von Termen}
   228 Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen Term umgewandelt werden kann.
   229 {\footnotesize\begin{verbatim}
   230    > term_of;
   231       val it = fn : Thm.cterm -> Term.term
   232 \end{verbatim}}
   233 Durch die Umwandlung eines cterms in einen Term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.
   234 {\footnotesize\begin{verbatim}
   235    > term_of t4;
   236       val it =
   237          Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
   238          ...: Term.term
   239 
   240 \end{verbatim}}
   241 In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert, der immer die selbe Funktion hat.
   242 {\footnotesize\begin{verbatim}
   243    > term_of t5;
   244       val it =
   245          Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
   246          ... : Term.term
   247 \end{verbatim}}
   248 Sollten verschiedene Teile des ''output`` (= das vom Computer Ausgegebene) nicht sichtbar sein, kann man mit einem bestimmten Befehl alles angezeigt werden.
   249 {\footnotesize\begin{verbatim}
   250    > print_depth;
   251       val it = fn : int -> unit
   252  \end{verbatim}}
   253 Zuerst gibt man den Befehl ein, danach den Term, der gr\"osser werden soll. Dabei kann man selbst einen Wert f\"ur die L\"ange bestimmen.
   254 {\footnotesize\begin{verbatim}
   255    > print_depth 10;
   256       val it = () : unit
   257    > term_of t4;
   258          val it =
   259             Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
   260                 Free ("x", "RealDef.real") $
   261             (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
   262                 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
   263          : Term.term
   264 
   265    > print_depth 10;
   266          val it = () : unit
   267    > term_of t5;
   268          val it =
   269             Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
   270                 Free ("x", "RealDef.real") $
   271             (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
   272                 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
   273          : Term.term
   274 \end{verbatim}}
   275 \paragraph{Versuchen Sie es!}
   276 Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende: 
   277 {\footnotesize\begin{verbatim}
   278    > (*-4-*) val thy = Rational.thy;
   279       val thy =
   280          {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
   281          Sum_Type, Relation, Record, Inductive, Transitive_Closure,
   282          Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
   283          SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
   284          Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
   285          IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
   286          Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
   287          RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
   288          Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
   289          Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
   290      : Theory.theory
   291    > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
   292  
   293       ***
   294       *** Free (d_d, [real, real] => real)
   295       *** . Free (x, real)
   296       *** . Const (op +, [real, real] => real)
   297       *** . . Free (a, real)
   298       *** . . Free (x, real)
   299       ***
   300  
   301       val it = () : unit
   302 
   303 
   304    > (*-5-*) val thy = Diff.thy;
   305       val thy =
   306          {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
   307          Sum_Type, Relation, Record, Inductive, Transitive_Closure,
   308          Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
   309          SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
   310          Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
   311          IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
   312          Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
   313          RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
   314          Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
   315          Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
   316          Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
   317          PolyEq, LogExp, Diff} : Theory.theory
   318  
   319    > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
   320  
   321       ***
   322       *** Const (Diff.d_d, [real, real] => real)
   323       *** . Free (x, real)
   324       *** . Const (op +, [real, real] => real)
   325       *** . . Free (a, real)
   326       *** . . Free (x, real)
   327       ***
   328  
   329       val it = () : unit
   330 \end{verbatim}}
   331 
   332 
   333 \chapter{''Rewriting``}
   334 \section{Was ist Rewriting?}
   335 Bei Rewriting handelt es sich um das Umformen von Termen nach vorgegebenen Regeln. Folgende zwei Funktionen sind notwendig:
   336 {\footnotesize\begin{verbatim}
   337    > rewrite;
   338       val it = fn
   339       :
   340       theory' ->
   341       rew_ord ->
   342       rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
   343 \end{verbatim}}
   344 Die Funktion hat zwei Argumente, die mitgeschickt werden m\"ussen, damit die Funktion arbeiten kann. Das letzte Element {\tt (cterm' * cterm' list) Library.option} im unteren Term ist das Ergebnis, das die Funktionen {\tt rewrite} zur\"uckgeben und die zwei vorhergehenden Argumente, {\tt theorem} und {\tt cterm}, sind die f\"ur uns wichtigen. {\tt Theorem} ist die Rechenregel und {\tt cterm} jene Formel auf die die Rechenregel angewendet wird.
   345 {\footnotesize\begin{verbatim}
   346    > rewrite_inst;
   347       val it = fn
   348       :
   349       theory' ->
   350       rew_ord ->
   351       rls' ->bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
   352 \end{verbatim}}
   353 Die Funktion {\tt rewrite\_inst} wird ben\"otigt, um Gleichungen, Rechnungen zum Differenzieren etc. zu l\"osen. Dabei wird die gebundene Variable (bdv) instanziiert, d.h. es wird die Variable angegeben, nach der man differenzieren will, bzw. f\"ur die ein Wert bei einer Gleichung herauskommen soll.
   354 Um zu sehen wie der Computer vorgeht nehmen wir folgendes Beispiel, dessen Ergebnis offenbar 0 ist, was der Computer jedoch erst nach einer Reihe von Schritten herausfindet.
   355 Im Beispiel wird differenziert, wobei \isac's Schreibweise jene von Computer Algebra Systemen (CAS) anzugleichen: in CAS wird differenziert mit $\frac{d}{dx}\; x^2 + 3 \cdot x + 4$, in \isac{} mit {\tt d\_d x (x \^{ }\^{ }\^{ } 2 + 3 * x + 4)}.
   356 Zuerst werden die einzelnen Werte als Variablen gespeichert:
   357 {\footnotesize\begin{verbatim}
   358    > val thy' = "Diff.thy";
   359       val thy' = "Diff.thy" : string
   360    > val ro = "tless_true";
   361       val ro = "tless_true" : string
   362    > val er = "eval_rls";
   363       val er = "eval_rls" : string
   364    > val inst = [("bdv","x::real")];
   365       val inst = [("bdv", "x::real")] : (string * string) list
   366    > val ct = "d_d x (a + a * (2 + b))";
   367       val ct = "d_d x (a + a * (2 + b))" : string
   368 \end{verbatim}}
   369 Nun wird die Rechnung nach den Regeln ausgerechnet, wobei am Ende mehrere Dinge zugleich gemacht werden.
   370 Folgende Regeln werden ben\"otigt: Summenregel, Produktregel, Multiplikationsregel mit einem konstanten Faktor und zum Schluss die Additionsregel.
   371 {\footnotesize\begin{verbatim}
   372    > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;
   373       val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
   374    > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_prod","") ct;
   375       val ct = "d_d x a + (d_d x a * (2 + b) + a * d_d x (2 + b))" : cterm'
   376    > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
   377       val ct = "d_d x a + (d_d x a * (2 + b) + a * 0) " : cterm'
   378    > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
   379       val ct = "d_d x a + (0 * (2 + b) + a * 0)" : cterm'
   380    > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
   381       val ct = "0 + (0 * (2 + b) + a * 0)" : cterm'
   382    > val Some (ct,_) = rewrite_set thy' true "make_polynomial" ct;
   383       val ct = "0" : string
   384 \end{verbatim}}
   385 Was {\tt rewrite\_set} genau macht, finden Sie im n\"achsten Kapitel.
   386 
   387 Dies w\"are ein etwas ernsthafteres Beispiel zum Differenzieren:
   388 {\footnotesize\begin{verbatim}
   389    > val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
   390    > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;
   391 \end{verbatim}}
   392 \paragraph{Versuchen Sie es,} diese Beispiel zu Ende zu f\"uhren! Die Regeln, die \isac{} kennt und zum Umformen verwenden kann, finden Sie im Internet \footnote{{\tiny\tt http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Diff.html}}.
   393 
   394 \section{Welche W\"unsche kann man an Rewriting stellen?}
   395 Es gibt verschiedene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
   396 {\tt rewrite\_ set} wandelt Terme in ein ganzes rule set um, die normalerweise nur mit einem Theorem vereinfacht dargestellt werden.
   397 Hierbei werden auch folgende Argumente verwendet:\\
   398 \tabcolsep=4mm
   399 \def\arraystretch{1.5}
   400 \begin{tabular}{lp{11.0cm}}
   401 {\tt theory} & Die Theory von Isabelle, die alle n\"otigen Informationen f\"ur das Parsing {\tt term} enth\"alt. \\
   402 {\tt rew\_ord}& die Ordnung f\"ur das geordnete Rewriting. F\"ur {\em no} ben\"otigt das geordnete Rewriting {\tt tless\_true}, eine Ordnung, die f\"ur alle nachgiebigen Argumente true ist \\
   403 {\tt rls} & Das rule set; zur Auswertung von bestimmten Bedingungen in {\tt thm} falls {\tt thm} eine conditional rule ist \\
   404 {\tt bool} & ein Bitschalter, der die Berechnungen der m\"oglichen condition in {\tt thm} ausl\"ost: wenn sie {\tt false} ist, dann wird die condition bewertet und auf Grund des Resultats wendet man {\tt thm} an, oder nicht; wenn {\tt true} dann wird die condition nicht ausgewertet, aber man gibt sie in eine Menge von Hypothesen \\
   405 {\tt thm} & das theorem versucht den {\tt term} zu \"uberschreiben \\
   406 {\tt term} & {\tt thm} wendet Rewriting m\"oglicherweise auf den Term an \\
   407 \end{tabular}\\
   408 
   409 {\footnotesize\begin{verbatim}
   410    > rewrite_set;
   411       val it = fn : theory' -> bool -> rls' -> ...
   412 \end{verbatim}}
   413 {\footnotesize\begin{verbatim}
   414    > rewrite_set_inst;
   415       val it = fn : theory' -> bool -> subs' -> .
   416 \end{verbatim}}
   417 Wenn man sehen m\"ochte wie Rewriting bei den einzelnen theorems funktioniert kann man dies mit {\tt trace\_rewrite} versuchen.
   418 {\footnotesize\begin{verbatim}
   419    > trace_rewrite := true;
   420       val it = () : unit
   421 \end{verbatim}}
   422 
   423 
   424 \section{Rule sets}
   425 Einige der oben genannten Varianten von Rewriting beziehen sich nicht nur auf einen theorem, sondern auf einen ganzen Block von theorems, die man als rule set bezeichnet.
   426 Dieser wird so lange angewendet, bis ein Element davon f\"ur Rewriting verwendet werden kann. Sollte der Begriff ''terminate`` fehlen, wird das Rule set nicht beendet und l\"auft weiter.
   427 Ein Beispiel f\"ur einen rule set ist folgendes:
   428 {\footnotesize\begin{verbatim}
   429 ???????????
   430 \end{verbatim}}
   431 
   432 {\footnotesize\begin{verbatim}
   433    > sym;
   434       val it = "?s = ?t ==> ?t = ?s" : Thm.thm
   435    > rearrange_assoc;
   436       val it =
   437          Rls
   438             {id = "rearrange_assoc",
   439                program = Script (Free ("empty_script", "RealDef.real")),
   440                calc = [],
   441                asm_rls =
   442                Rls
   443                   {id = "e_rls",
   444                      program = EmptyScr,
   445                      calc = [],
   446                      asm_rls = Erls,
   447                      prog_rls = Erls,
   448                      rules = [],
   449                      rew_ord = ("dummy_ord", fn),
   450                      preconds = []},
   451                prog_rls =
   452                Rls
   453                   {id = "e_rls",
   454                      program = EmptyScr,
   455                      calc = [],
   456                      asm_rls = Erls,
   457                      prog_rls = Erls,
   458                      rules = [],
   459                      rew_ord = ("dummy_ord", fn),
   460                      preconds = []},
   461                rules =
   462                [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"  [.]),
   463                   Thm
   464                      ("sym_rmult_assoc",
   465                         "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1"  [.])],
   466                rew_ord = ("Rewrite_Ord.id_empty", fn),
   467                preconds = []} : rls
   468 \end{verbatim}}
   469 
   470 
   471 \section{Berechnung von Konstanten}
   472 Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:
   473 {\footnotesize\begin{verbatim}
   474    > calculate;
   475       val it = fn
   476       :
   477          theory' ->
   478          string *
   479          (
   480          string ->
   481          Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
   482          cterm' -> (string * thm') Library.option
   483 
   484    > calculate_;
   485       val it = fn
   486       :
   487          Theory.theory ->
   488          string *
   489          (
   490          string ->
   491          Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
   492          Term.term -> (Term.term * (string * Thm.thm)) Library.option
   493 \end{verbatim}}
   494 Man bekommt das Ergebnis und das theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
   495 {\footnotesize\begin{verbatim}
   496    > calclist;
   497       val it =
   498          [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),
   499             ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),
   500             ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),
   501             ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),
   502             ("le", ("op <", fn)), ("leq", ("op <=", fn)),
   503             ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),
   504             ("Test.is_root_free", ("is'_root'_free", fn)),
   505             ("Test.contains_root", ("contains'_root", fn))]
   506       :
   507          (
   508          string *
   509          (
   510          string *
   511          (
   512          string ->
   513          Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
   514 \end{verbatim}}
   515 
   516 
   517 
   518 
   519 \chapter{Termordnung}
   520 Die Anordnungen der Begriffe sind unverzichtbar f\"ur den Gebrauch des Umschreibens von normalen Funktionen und von normalen Formeln, die n\"otig sind um passende Modelle f\"ur Probleme zu finden.
   521 
   522 \section{Beispiel f\"ur Termordnungen}
   523 Es ist nicht unbedeutend, eine Verbindung zu Termen herzustellen, die wirklich eine Ordnung besitzen. Diese Ordnungen sind selbstaufrufende Bahnordnungen:
   524 
   525 {\footnotesize\begin{verbatim}
   526    > sqrt_right;
   527       val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b       ool
   528    > tless_true;
   529       val it = fn : subst -> Term.term * Term.term -> bool
   530 \end{verbatim}}
   531 
   532 Das ''bool`` Argument gibt Ihnen die M\"oglichkeit, die Kontrolle zu den zugeh\"origen Unterordunungen zur\"uck zu verfolgen, damit sich die Unterordnungen, die 'true' sind, als strings anzeigen lassen.
   533 
   534 {\section{Geordnetes Rewriting}}
   535 Beim Rewriting entstehen Probleme, die vom ''law of commutativity`` (= Kommutativgesetz) durch '+' und '*' verursacht werden. Diese Probleme k\"onnen nur durch geordnetes Rewriting gel\"ost werden, da hier ein Term nur umgeschrieben wird, wenn ein kleinerer dadurch entsteht.
   536 
   537 
   538 \chapter{Problem hierachy}
   539 \section{''Matching``}
   540 Matching ist eine Technik von Rewriting, die von \isac{} verwendet wird, um ein Problem und den passenden problem type daf\"ur zu finden. Die folgende Funktion \"uberpr\"uft, ob Matching m\"oglich ist:
   541 {\footnotesize\begin{verbatim}
   542 > matches;
   543 val it = fn : Theory.theory -> Term.term -> Term.term -> bool
   544 \end{verbatim}}
   545 Die folgende Gleichung wird in Operatoren und freie Variablen zerlegt.
   546 {\footnotesize\begin{verbatim}
   547 > val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
   548 val t =
   549 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
   550 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
   551 Free ("3", "RealDef.real") $
   552 (Const
   553 ("Atools.pow",
   554 "[RealDef.real, RealDef.real] => RealDef.real") $
   555 Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $
   556 Free ("1", "RealDef.real") : Term.term
   557 \end{verbatim}}
   558 Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchf\"uhrt.
   559 {\footnotesize\begin{verbatim}
   560 > val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
   561 val p =
   562 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
   563 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
   564 Free ("a", "RealDef.real") $
   565 (Const
   566 ("Atools.pow",
   567 "[RealDef.real, RealDef.real] => RealDef.real") $
   568 Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $
   569 Free ("c", "RealDef.real") : Term.term
   570 \end{verbatim}}
   571 Dieses Modell enth\"alt sogenannte \textit{scheme variables}.
   572 {\footnotesize\begin{verbatim}
   573 > atomt p;
   574 "*** -------------"
   575 "*** Const (op =)"
   576 "*** . Const (op *)""*** . . Free (a, )"
   577 "*** . . Const (Atools.pow)"
   578 "*** . . . Free (b, )"
   579 "*** . . . Free (2, )"
   580 "*** . Free (c, )"
   581 "\n"
   582 val it = "\n" : string
   583 \end{verbatim}}
   584 Das Modell wird durch den Befehl \textit{mk_Var} erstellt.
   585 {\footnotesize\begin{verbatim}
   586 > mk_Var;
   587 val it = fn : Term.term -> Term.term
   588 > val pat = mk_Var p;
   589 val pat =
   590 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
   591 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
   592 Var (("a", 0), "RealDef.real") $
   593 (Const
   594 ("Atools.pow",
   595 "[RealDef.real, RealDef.real] => RealDef.real") $
   596 Var (("b", 0), "RealDef.real") $
   597 Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real")
   598 : Term.term
   599 > Sign.string_of_term (sign_of thy) pat;
   600 val it = "?a * ?b ^^^ 2 = ?c" : string
   601 \end{verbatim}}
   602 Durch \textit{atomt pat} wird der Term aufgespalten und in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt wird.
   603 {\footnotesize\begin{verbatim}
   604 > atomt pat;
   605 "*** -------------"
   606 "*** Const (op =)"
   607 "*** . Const (op *)"
   608 "*** . . Var ((a, 0), )"
   609 "*** . . Const (Atools.pow)"
   610 "*** . . . Var ((b, 0), )"
   611 "*** . . . Free (2, )"
   612 "*** . Var ((c, 0), )"
   613 "\n"
   614 val it = "\n" : string
   615 \end{verbatim}}
   616 Jetzt kann das Matching an den beiden vorigen Terme angewendet werden.
   617 {\footnotesize\begin{verbatim}
   618 > matches thy t pat;
   619 val it = true : bool
   620 > val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
   621 val t2 =
   622 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
   623 (Const
   624 ("Atools.pow",
   625 "[RealDef.real, RealDef.real] => RealDef.real") $
   626 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
   627 Free ("1", "RealDef.real") : Term.term
   628 > matches thy t2 pat;
   629 val it = false : bool
   630 > val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
   631 val pat2 =
   632 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
   633 (Const
   634 ("Atools.pow",
   635 "[RealDef.real, RealDef.real] => RealDef.real") $
   636 Var (("u", 0), "RealDef.real") $ Free ("2", "RealDef.real")) $
   637 Var (("v", 0), "RealDef.real") : Term.term
   638 > matches thy t2 pat2;
   639 val it = true : bool
   640 \end{verbatim}}
   641 
   642 \section{Zugriff auf die hierachy}
   643 Man verwendet folgenden Befehl, um sich Zugang zur hierachy von problem type zu verschaffen.
   644 {\footnotesize\begin{verbatim}
   645 > show_ptyps;
   646 val it = fn : unit -> unit
   647 > show_ptyps();
   648 [
   649 ["e_pblID"],
   650 ["simplification", "polynomial"],
   651 ["simplification", "rational"],
   652 ["vereinfachen", "polynom", "plus_minus"],
   653 ["vereinfachen", "polynom", "klammer"],
   654 ["vereinfachen", "polynom", "binom_klammer"],
   655 ["probe", "polynom"],
   656 ["probe", "bruch"],
   657 ["equation", "univariate", "linear"],
   658 ["equation", "univariate", "root", "sq", "rat"],
   659 ["equation", "univariate", "root", "normalize"],
   660 ["equation", "univariate", "rational"],
   661 ["equation", "univariate", "polynomial", "degree_0"],
   662 ["equation", "univariate", "polynomial", "degree_1"],
   663 ["equation", "univariate", "polynomial", "degree_2", "sq_only"],
   664 ["equation", "univariate", "polynomial", " 
   665  degree_2", "bdv_only"],
   666 ["equation", "univariate", "polynomial", "degree_2", "pqFormula"],
   667 ["equation", "univariate", "polynomial", "degree_2", "abcFormula"],
   668 ["equation", "univariate", "polynomial", "degree_3"],
   669 ["equation", "univariate", "polynomial", "degree_4"],
   670 ["equation", "univariate", "polynomial", "normalize"],
   671 ["equation", "univariate", "expanded", "degree_2"],
   672 ["equation", "makeFunctionTo"],
   673 ["function", "derivative_of", "named"],
   674 ["function", "maximum_of", "on_interval"],
   675 ["function", "make", "by_explicit"],
   676 ["function", "make", "by_new_variable"],
   677 ["function", "integrate", "named"],
   678 ["tool", "find_values"],
   679 ["system", "linear", "2x2", "triangular"],
   680 ["system", "linear", "2x2", "normalize"],
   681 ["system", "linear", "3x3"],
   682 ["system", "linear", "4x4", "triangular"],
   683 ["system", "linear", "4x4", "normalize"],
   684 ["Biegelinien", "
   685 MomentBestimmte"],
   686 ["Biegelinien", "MomentGegebene"],
   687 ["Biegelinien", "einfache"],
   688 ["Biegelinien", "QuerkraftUndMomentBestimmte"],
   689 ["Biegelinien", "vonBelastungZu"],
   690 ["Biegelinien", "setzeRandbedingungen"],
   691 ["Berechnung", "numerischSymbolische"],
   692 ["test", "equation", "univariate", "linear"],
   693 ["test", "equation", "univariate", "plain_square"],
   694 ["test", "equation", "univariate", "polynomial", "degree_two", "pq_formula"],
   695 ["test", "equation", "univariate", "polynomial", "degree_two", "abc_formula"],
   696 ["test", "equation", "univariate", "squareroot"],
   697 ["test", "equation", "univariate", "normalize"],
   698 ["test", "equation", "univariate", "sqroot-test"]
   699 ]
   700 val it = () : unit
   701 \end{verbatim}}
   702 
   703 \section{Die passende ''formalization`` f\"ur den problem type}
   704 Eine andere Art des Matching ist es die richtige ''formalization`` zum jeweiligen problem type zu finden. Wenn eine solche vorhanden ist, kann \isac{} selbstst\"andig die Probleme l\"osen.
   705 
   706 \section{''problem-refinement``}
   707 Will man die problem hierachy (= ) aufstellen, so ist darauf zu achten, dass man die verschiedenen Branches so konstruiert, dass das problem-refinement automatisch durchgef\"uhrt werden kann.
   708 {\footnotesize\begin{verbatim}
   709 > refine;
   710 val it = fn : fmz_ -> pblID -> SpecifyTools.match list
   711 > val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x 
   712 + sqrt (5 + x))",
   713 # "soleFor x","errorBound (eps=0)",
   714 # "solutions L"];
   715 val fmz =
   716 ["equality (sqrt(9 + 4 * x)=sqrt x + sqrt (5 + x))", "soleFor x",
   717 "errorBound (eps=0)", ...] : string list
   718 > refine fmz ["univariate","equation"];
   719 *** pass ["equation","univariate"]
   720 *** comp_dts: ??.empty $ soleFor x
   721 Exception- ERROR raised
   722 \end{verbatim}}
   723 Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, kommt die dritte zum Einsatz:
   724 {\footnotesize\begin{verbatim}
   725 > val fmz = ["equality (x + 1 = 2)",
   726 # "solveFor x","errorBound (eps=0)",
   727 # "solutions L"];
   728 val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...]
   729 : string list
   730 > refine fmz ["univariate","equation"];
   731 *** pass ["equation","univariate"]
   732 *** pass ["equation","univariate","linear"]
   733 *** pass ["equation","univariate","root"]
   734 *** pass ["equation","univariate","rational"]
   735 *** pass ["equation","univariate","polynomial" ]
   736 *** pass ["equation","univariate","polynomial","degree_0"]
   737 *** pass ["equation","univariate","polynomial","degree_1"]
   738 *** pass ["equation","univariate","polynomial","degree_2"]
   739 *** pass ["equation","univariate","polynomial","degree_3"]
   740 *** pass ["equation","univariate","polynomial","degree_4"]
   741 *** pass ["equation","univariate","polynomial","normalize"]
   742 val it =
   743 [Matches
   744 (["univariate", "equation"],
   745 {Find = [Correct "solutions L"], With = [...], ...}),
   746 NoMatch (["linear", "univariate", ...], {Find = [...], ...}),
   747 NoMatch (["root", ...], ...), ...] : SpecifyTools.match list
   748 \end{verbatim}}
   749 Der problem type wandelt $x + 1 = 2$ in die normale Form $-1 + x = 0$ um. Diese Suche nach der jeweiligen problem hierachy kann mit Hilfe eines ''proof state`` durchgef\"uhrt werden (siehe n\"achstes Kapitel).
   750 
   751 
   752 \chapter{''Methods``}
   753 Methods werden dazu verwendet, Probleme von type zu l\"osen. Sie sind in einer anderen Programmiersprache beschrieben. Die Sprache sieht einfach aus, betreibt aber im Hintergrund einen enormen Pr\"ufaufwand. So muss sich der Programmierer nicht mit technischen Details befassen, gleichzeitig k\"onnen aber auch keine falschen Anweisungen eingegeben werden.
   754 \section{Der ''Syntax`` des script}
   755 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
   756 Er kann so definiert werden:
   757 \begin{tabbing}
   758 123\=123\=expr ::=\=$|\;\;$\=\kill
   759 \>script ::= {\tt Script} id arg$\,^*$ = body\\
   760 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
   761 \>\>body ::= expr\\
   762 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
   763 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
   764 \>\>\>$|\;$\>listexpr\\
   765 \>\>\>$|\;$\>id\\
   766 \>\>\>$|\;$\>seqex id\\
   767 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
   768 \>\>\>$|\;$\>{\tt Repeat} seqex\\
   769 \>\>\>$|\;$\>{\tt Try} seqex\\
   770 \>\>\>$|\;$\>seqex {\tt Or} seqex\\
   771 \>\>\>$|\;$\>seqex {\tt @@} seqex\\
   772 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
   773 \>\>type ::= id\\
   774 \>\>tac ::= id
   775 \end{tabbing}
   776 
   777 \section{\"Uberpr\"ufung der Auswertung}
   778 Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:
   779 \begin{description}
   780 \item{{\tt while} prop {\tt Do} expr id} 
   781 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
   782 \end{description}
   783 W\"ahrend die genannten Befehle das Kontrollsystem durch Auswertung der Formeln ausl\"osen, h\"angen die anderen von der Anwendbarkeit der Formel in den entsprechenden Unterbegriffen ab:
   784 \begin{description}
   785 \item{{\tt Repeat} expr id}
   786 \item{{\tt Try} expr id}
   787 \item{expr {\tt Or} expr id}
   788 \item{expr {\tt @@} expr id}
   789 \item xxx
   790 \end{description}
   791 
   792 
   793 
   794 \chapter{Befehle von \isac{}}
   795 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.\
   796 \newline\linebreak \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion)} gibt die eingegebenen Befehle an die mathematic engine weiter, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler tactic verwendet.\
   797 \newline\linebreak \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\
   798 \newline\linebreak \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"ur das Umformen.\
   799 \newline\linebreak \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.\
   800 \newline\linebreak \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\
   801 \newline\linebreak \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\
   802 \newline\linebreak \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\
   803 \newline\linebreak \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe einer method.\
   804 \newline\linebreak \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``.\
   805 \newline\linebreak \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des theorems, anstatt diese zu sch\"atzen.\
   806 \newline\linebreak \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von theorems, dem rule set.\
   807 \newline\linebreak \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen tactics, ersetzt aber Konstanten im theorem, bevor es zu einer Anwendung kommt.\
   808 \newline\linebreak \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\
   809 \newline\linebreak \textbf{Substitute substitution} f\"ugt der momentanen Formel {\tt substitution} hinzu und wandelt es um.\
   810 \newline\linebreak \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\
   811 \newline\linebreak \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\
   812 \newline\linebreak \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\
   813 \newline\linebreak \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.\
   814 \newline\linebreak \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\
   815 \newline\linebreak \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\
   816 \newline\linebreak \textbf{Check\_postcond} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim Beenden des subproblem.\
   817 \newline\linebreak \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.
   818 
   819 \section{Die Funktionsweise der mathematic engine}
   820 Ein proof (= Beweis) wird in der mathematic engine me von der tactic {\tt Init\_Proof} gestartet und wird wechselwirkend mit anderen tactics vorangebracht. Auf den input (= das, was eingegeben wurde) einzelner tactics folgt eine Formel, die von der me ausgegeben wird, und die darauf folgende tactic gilt. Der proof ist beendet, sobald die me {\tt End\_Proof} als n\"achste tactic vorschl\"agt.
   821 \newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird. 
   822 {\footnotesize\begin{verbatim}
   823 ??????????????????????????????????????????????????????????????????????????????????   
   824 
   825 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
   826                   "errorBound (eps=#0)","solutions L"];
   827    val fmz =
   828      ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
   829       "solutions L"] : string list
   830    ML>
   831    ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
   832                                  ("SqRoot.thy","no_met"));
   833    val dom = "SqRoot.thy" : string
   834    val pbt = ["univariate","equation"] : string list
   835    val met = ("SqRoot.thy","no_met") : string * string
   836 \end{verbatim}}
   837 
   838 \section{Der Beginn einer Rechnung}
   839 
   840 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. Um einen neuen proof beginnen zu k\"onnen, werden folgende Schritte durchgef\"uhrt:
   841 {\footnotesize\begin{verbatim}
   842 ???????????????????????????????????????????????????????????????????????????????????????????? 
   843 ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
   844    val mID = "Init_Proof" : string
   845    val m =
   846      Init_Proof
   847        (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
   848          "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
   849    ML>
   850    ML>  val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
   851    val p = ([],Pbl) : pos'
   852    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
   853    val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
   854      : string * mstep
   855    val pt =
   856      Nd
   857        (PblObj
   858           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
   859            result=#,spec=#},[]) : ctree
   860 \end{verbatim}}
   861 Die mathematics engine gibt etwas mit dem type {\tt mout} aus, was in unserem Fall ein Problem darstellt. Sobald mehr angezeigt wird, m\"usste dieses jedoch gel\"ost sein.
   862 {\footnotesize\begin{verbatim}
   863 ?????????????????????????????????????????????????????????????????????????????????????????????
   864    ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
   865    val it = () : unit
   866    ML>
   867    ML> f;
   868    val it =
   869      Form'
   870        (PpcKF
   871           (0,EdUndef,0,Nundef,
   872            (Problem [],
   873             {Find=[Incompl "solutions []"],
   874              Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
   875              Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
   876 \end{verbatim}}
   877 {\footnotesize\begin{verbatim}
   878 ?????????????????????????????????????????????????????????????????????????????????????????????
   879    ML>  nxt;
   880    val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
   881      : string * mstep
   882    ML>
   883    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   884    val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
   885      : string * mstep
   886    ML>
   887    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   888 \end{verbatim}}
   889 
   890 \section{The phase of modeling}
   891 Dieses Kapitel besch\"aftigt sich mit dem input der Einzelheiten bei einem Problem. Die me kann dabei helfen, wenn man die formalization durch {\tt Init\_Proof} darauf hinweist. Normalerweise weiss die mathematics engine die n\"achste gute tactic.
   892 {\footnotesize\begin{verbatim}
   893 ?????????????????????????????????????????????????????????????????????????????????????????????
   894    ML>  nxt;
   895    val it =
   896      ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
   897      : string * mstep
   898    ML>
   899    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   900    val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
   901    ML>
   902    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   903    val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
   904    ML>
   905    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 
   906    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
   907 \end{verbatim}}
   908 {\footnotesize\begin{verbatim}
   909 ?????????????????????????????????????????????????????????????????????????????????????????????
   910    ML>  Compiler.Control.Print.printDepth:=8;
   911    ML>  f;
   912    val it =
   913      Form'
   914        (PpcKF
   915           (0,EdUndef,0,Nundef,
   916            (Problem [],
   917             {Find=[Correct "solutions L"],
   918              Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
   919                     Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
   920 \end{verbatim}}
   921 
   922 
   923 \section{The phase of specification}
   924 Diese phase liefert eindeutige Bestimmungen einer domain, 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.
   925 {\footnotesize\begin{verbatim}
   926 ??????????????????????????????????????????????????????????????????????????????????????????
   927    ML> nxt;
   928    val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
   929    ML>
   930    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   931    val nxt =
   932      ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
   933      : string * mstep
   934    val pt =
   935      Nd
   936        (PblObj
   937           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
   938               result=#,spec=#},[]) : ctree
   939 \end{verbatim}}
   940 Die me erkennt den richtigen Problem type und arbeitet so weiter:
   941 {\footnotesize\begin{verbatim}
   942 ?????????????????????????????????????????????????????????????????????????????????????????
   943    ML> val nxt = ("Specify_Problem",
   944                Specify_Problem ["polynomial","univariate","equation"]);
   945    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   946    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
   947    val nxt =
   948      ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
   949      : string * mstep
   950    ML>
   951    ML> val nxt = ("Specify_Problem",
   952                Specify_Problem ["linear","univariate","equation"]);
   953    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   954    val f =
   955      Form'
   956        (PpcKF
   957           (0,EdUndef,0,Nundef,
   958            (Problem ["linear","univariate","equation"],
   959             {Find=[Correct "solutions L"],
   960              Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
   961                     Correct "solveFor x"],Relate=[],
   962              Where=[False
   963                     "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
   964              With=[]}))) : mout 
   965 \end{verbatim}}
   966 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``].
   967 {\footnotesize\begin{verbatim}
   968 ????????????????????????????????????????????????????????????????????????????????????????????
   969    ML> val nxt = ("Refine_Problem",
   970                   Refine_Problem ["linear","univariate","equation
   971    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   972    val f = Problems (RefinedKF [NoMatch #]) : mout
   973    ML>
   974    ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
   975    val f =
   976      Problems
   977        (RefinedKF
   978           [NoMatch
   979              (["linear","univariate","equation"],
   980               {Find=[Correct "solutions L"],
   981                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
   982                       Correct "solveFor x"],Relate=[],
   983                Where=[False
   984                      "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
   985                With=[]})]) : mout
   986    ML>
   987    ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
   988    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   989    val f =
   990      Problems
   991        (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
   992      : mout
   993    ML>
   994    ML>
   995    ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
   996    val f =
   997      Problems
   998        (RefinedKF
   999           [Matches
  1000              (["univariate","equation"],
  1001               {Find=[Correct "solutions L"],
  1002                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1003                       Correct "solveFor x"],Relate=[],
  1004                Where=[Correct
  1005                With=[]}),
  1006            NoMatch
  1007              (["linear","univariate","equation"],
  1008               {Find=[Correct "solutions L"],
  1009                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1010                       Correct "solveFor x"],Relate=[],
  1011                Where=[False
  1012                       "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
  1013                   With=[]}),
  1014            NoMatch
  1015              ...
  1016              ...   
  1017            Matches
  1018              (["normalize","univariate","equation"],
  1019               {Find=[Correct "solutions L"],
  1020                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1021                       Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
  1022 \end{verbatim}}
  1023 Die tactic {\tt Refine\_Problem} wandelt alle matches wieder in problem types um und sucht in der problem hierachy weiter.
  1024 
  1025 
  1026 \section{The phase of solving}
  1027 Diese phase beginnt mit dem Aufruf einer method, die eine normale form innerhalb einer tactic ausf\"uhrt: {\tt Rewrite rnorm\_equation\_add} und {\tt Rewrite\_Set SqRoot\_simplify}:
  1028 {\footnotesize\begin{verbatim} 
  1029    ML> nxt;
  1030    val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
  1031      : string * mstep
  1032    ML>
  1033    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1034    val f =
  1035      Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
  1036    val nxt =
  1037      ("Rewrite", Rewrite
  1038         ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
  1039    ML>
  1040    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1041    val f =
  1042      Form' (FormKF (~1,EdUndef,1,Nundef,
  1043            "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
  1044    val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
  1045    ML>
  1046    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1047    val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
  1048    val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
  1049 \end{verbatim}}
  1050 Die Formel $-6 + 3\cdot x = 0$ ist die Eingabe eine subproblems, das wiederum gebraucht wird, um die Gleichungsart zu erkennen und die entsprechende method auszuf\"uhren:
  1051 {\footnotesize\begin{verbatim}
  1052    ML> nxt;
  1053    val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
  1054    ML>   
  1055    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1056    val f =
  1057      Form' (FormKF
  1058           (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
  1059      : mout
  1060    val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
  1061    ML>
  1062    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1063    val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
  1064 \end{verbatim}}
  1065 {\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.
  1066 Nun folgt erneut die phase of modeling und die phase of specification.
  1067 
  1068 \section{The final phase: \"Uberpr\"ufung der ''post-condition``}
  1069 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 noch offene Fragen.
  1070 Dadurch wird die post-condition im folgenden Beispiel als problem und subproblem erw\"ahnt.
  1071 {\footnotesize\begin{verbatim}
  1072    ML> nxt;
  1073    val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
  1074    ML>
  1075    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1076    val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
  1077    val nxt =
  1078      ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
  1079    ML>
  1080    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1081    val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
  1082    val nxt = ("End_Proof'",End_Proof') : string * mstep
  1083 \end{verbatim}}
  1084 Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\
  1085 
  1086 \paragraph{Versuchen Sie es!} 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.
  1087 
  1088 
  1089 \part{Handbuch f\"ur Autoren}
  1090 
  1091 \chapter{Die Struktur des Grundlagenwissens}
  1092 
  1093 \section{''tactics`` und Daten}
  1094 Zuerst betrachten wir die me von aussen. Wir sehen uns tactics 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.
  1095 Diese Teile sind in alphabetischer Anordnung in Tab.\ref{kb-items} auf Seite \pageref{kb-items} aufgelistet.
  1096 
  1097 {\begin{table}[h]
  1098 \caption{Kleinste Teilchen des KB} \label{kb-items}
  1099 %\tabcolsep=0.3mm
  1100 \begin{center}
  1101 \def\arraystretch{1.0}
  1102 \begin{tabular}{lp{9.0cm}}
  1103 Abk\"urzung & Beschreibung \\
  1104 \hline
  1105 &\\
  1106 {\it calc\_list}
  1107 & gesammelte Liste von allen ausgewerteten Funktionen\\
  1108 {\it eval\_fn}
  1109 & ausgewertete Funktionen f\"ur Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\
  1110 {\it eval\_rls }
  1111 & rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\
  1112 {\it fmz}
  1113 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\
  1114 {\it met}
  1115 & eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it program}, etc.)\\
  1116 {\it metID}
  1117 & bezieht sich auf {\it met}\\
  1118 {\it op}
  1119 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\
  1120 {\it pbl}
  1121 & Problem d.h. der Knotenpunkt in der problem hierachy\\
  1122 {\it pblID}
  1123 & bezieht sich auf {\it pbl}\\
  1124 {\it rew\_ord}
  1125 & Anordnung beim Rewriting\\
  1126 {\it rls}
  1127 & rule set, d.h. eine Datenstruktur, die theorems {\it thm} und Operatoren {\it op} zur Vereinfachung (mit {\it rew\_ord}) enth\"alt \\
  1128 {\it Rrls}
  1129 & rule set f\"ur das 'reverse rewriting' (eine \isac-Technik, die schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
  1130 {\it program}
  1131 & script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\
  1132 {\it norm\_rls}
  1133 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\
  1134 {\it spec}
  1135 & Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\
  1136 {\it subs}
  1137 & Ersatz, z.B. eine Liste von Variablen und ihren jeweiligen Werten\\
  1138 {\it Term}
  1139 & Term von Isabelle, z.B. eine Formel\\
  1140 {\it thm}
  1141 & theorem\\
  1142 {\it thy}
  1143 & theory\\
  1144 {\it thyID}
  1145 & im Bezug auf {\it thy} \\
  1146 \end{tabular}\end{center}\end{table}}
  1147 
  1148 Die Verbindung zwischen tactics und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.
  1149 
  1150 
  1151 \begin{table}[h]
  1152 \caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb}
  1153 \tabcolsep=0.3mm
  1154 \begin{center}
  1155 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
  1156 tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
  1157 & &thy &program &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
  1158 \hline\hline
  1159 Init\_Proof
  1160 &fmz & x & & & x & & & & & & & x \\
  1161 &spec & & & & & & & & & & & \\
  1162 \hline
  1163 \multicolumn{13}{|l|}{model phase}\\
  1164 \hline
  1165 Add\_*
  1166 &Term & x & & & x & & & & & & & x \\
  1167 FormFK &model & x & & & x & & & & & & & x \\
  1168 \hline
  1169 \multicolumn{13}{|l|}{specify phase}\\
  1170 \hline
  1171 Specify\_Theory
  1172 &thyID & x & & & x & & & & x & x & & x \\
  1173 Specify\_Problem
  1174 &pblID & x & & & x & & & & x & x & & x \\
  1175 Refine\_Problem
  1176 &pblID & x & & & x & & & & x & x & & x \\
  1177 Specify\_Method
  1178 &metID & x & & & x & & & & x & x & & x \\
  1179 Apply\_Method
  1180 &metID & x & x & & x & & & & x & x & & x \\
  1181 \hline
  1182 \multicolumn{13}{|l|}{solve phase}\\
  1183 \hline
  1184 Rewrite,\_Inst
  1185 &thm & x & x & & & x &met & & x &met & & \\
  1186 Rewrite, Detail
  1187 &thm & x & x & & & x &rls & & x &rls & & \\
  1188 Rewrite, Detail
  1189 &thm & x & x & & & x &Rrls & & x &Rrls & & \\
  1190 Rewrite\_Set,\_Inst
  1191 &rls & x & x & & & & & x & x & x & & \\
  1192 Calculate
  1193 &op & x & x & & & & & & & & x & \\
  1194 Substitute
  1195 &subs & x & & & x & & & & & & & \\
  1196 & & & & & & & & & & & & \\
  1197 SubProblem
  1198 &spec & x & x & & x & & & & x & x & & x \\
  1199 &fmz & & & & & & & & & & & \\
  1200 \hline
  1201 \end{tabular}\end{center}\end{table}
  1202 
  1203 
  1204 \section{Die theories von \isac{}}
  1205 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} gekennzeichnet sind; normalerweise werden diese theories zusammen mit SML verwendet. Dann haben sie den selben Dateinamen, aber die Endung {\tt *.ML}.
  1206 Die theories von \isac{} representieren den Teil vom Basiswissen von \isac{}, die hierachy von den zwei theories ist nach diesen strukturiert. Die {\tt *.ML} Dateien beinhalten {\em alle} Daten von den anderen zwei Hauptlinien des Basiswissens, die problems und methods (ohne ihre jeweilige Struktur, die von den problem Browsern und den method Browsern gemacht wird, zu pr\"asentieren.
  1207 Die Tab.\ref{theories} auf Seite \pageref{theories} listet die base 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.
  1208 Die ersten drei theories auf der Liste geh\"oren {\em nicht} zum Grundwissen von \isac{}; sie besch\"aftigen sich mit der Skriptsprache f\"ur methods und ist hier nur zur Vollst\"andigkeit angef\"uhrt.
  1209 
  1210 {\begin{table}[h]
  1211 \caption{theory von der ersten Version von \isac} \label{theories}
  1212 %\tabcolsep=0.3mm
  1213 \begin{center}
  1214 \def\arraystretch{1.0}
  1215 \begin{tabular}{lp{9.0cm}}
  1216 theory & Beschreibung \\
  1217 \hline
  1218 &\\
  1219 ListI.thy
  1220 & ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind, zu und (intermediatly~?) definiert einige weitere Listen von Funktionen\\
  1221 ListI.ML
  1222 & {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\
  1223 Tools.thy
  1224 & Funktion, die f\"ur die Auswertung von Skripten ben\"otigt wird\\
  1225 Tools.ML
  1226 & bezieht sich auf {\tt eval\_fn}s\\
  1227 Script.thy
  1228 & Vorraussetzung f\"ur script: types, tactics, tacticals\\
  1229 Script.ML
  1230 & eine Reihe von tactics und Funktionen f\"ur den internen Gebrauch\\
  1231 & \\
  1232 \hline
  1233 & \\
  1234 Typefix.thy
  1235 & fortgeschrittener Austritt, um den type Fehlern zu entkommen\\
  1236 Descript.thy
  1237 & {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\
  1238 Atools
  1239 & Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; theorems f\"ur {\tt eval\_rls}\\
  1240 Float
  1241 & Gleitkommerzahlendarstellung\\
  1242 Equation
  1243 & grunds\"atzliche Vorstellung f\"ur  Gleichungen und Gleichungssysteme\\
  1244 Poly
  1245 & Polynome\\
  1246 PolyEq
  1247 & polynomiale Gleichungen und Gleichungssysteme \\
  1248 Rational.thy
  1249 & zus\"atzliche theorems f\"ur Rationale Zahlen\\
  1250 Rational.ML
  1251 & abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\
  1252 RatEq
  1253 & Gleichung mit rationalen Zahlen\\
  1254 Root
  1255 & Radikanten; berechnen der Normalform; das betreffende umgekehrte Regelwerk\\
  1256 RootEq
  1257 & Gleichungen mit Wurzeln\\
  1258 RatRootEq
  1259 & Gleichungen mit rationalen Zahlen und Wurzeln (z.B. mit Termen, die beide Vorg\"ange enthalten)\\
  1260 Vect
  1261 & Vektoren Analysis\\
  1262 Trig
  1263 & Trigonometrie\\
  1264 LogExp
  1265 & Logarithmus und Exponentialfunktionen\\
  1266 Calculus
  1267 & nicht der Norm entsprechende Analysis\\
  1268 Diff
  1269 & Differenzierung\\
  1270 DiffApp
  1271 & Anwendungen beim Differenzieren (Maximum-Minimum-Probleme)\\
  1272 Test
  1273 & (alte) Daten f\"ur Testfolgen\\
  1274 Isac
  1275 & enth\"alt alle Theorien von\isac{}\\
  1276 \end{tabular}\end{center}\end{table}}
  1277 
  1278 
  1279 \section{Daten in {\tt *.thy} und {\tt *.ML}}
  1280 Wie schon zuvor angesprochen, haben die Arbeiten die theories von *.thy und *.ML zusammen und haben deswegen den selben Dateiname. Wie diese Daten zwischen den zwei Dateien verteilt werden wird in der
  1281 Tab.\ref{thy-ML} auf Seite \pageref{thy-ML} gezeigt. Die Ordnung von den Datenteilchen in den theories sollte an der Ordnung von der Liste festhalten.
  1282 
  1283 {\begin{table}[h]
  1284 \caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML}
  1285 \tabcolsep=2.0mm
  1286 \begin{center}
  1287 \def\arraystretch{1.0}
  1288 \begin{tabular}{llp{7.7cm}}
  1289 Datei & Daten & Beschreibung \\
  1290 \hline
  1291 & &\\
  1292 {\tt *.thy}
  1293 & consts
  1294 & Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}')
  1295 \\
  1296 & rules
  1297 & theorems: \isac{} verwendet theorems von Isabelle, wenn m\"oglich; zus\"atzliche theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt
  1298 \\& &\\
  1299 {\tt *.ML}
  1300 & {\tt theory' :=}
  1301 & Die theory, die 
  1302 abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht
  1303 \\
  1304 & {\tt eval\_fn}
  1305 & 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
  1306 \\
  1307 & {\tt *\_simplify}
  1308 & 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}
  1309 \\
  1310 & {\tt norm\_rls :=}
  1311 & der automatisierte Vereinfacher {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac{}  zug\"anglich ist
  1312 \\
  1313 & {\tt rew\_ord' :=}
  1314 & das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird
  1315 \\
  1316 & {\tt ruleset' :=}
  1317 & dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls})
  1318 \\
  1319 & {\tt calc\_list :=}
  1320 & 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 tactic {\tt Calculate} in einem Skript)
  1321 \\
  1322 & {\tt store\_pbl}
  1323 & Problems, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}
  1324 \\
  1325 & {\tt methods :=}
  1326 & methods, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}
  1327 \\
  1328 \end{tabular}\end{center}\end{table}}
  1329 
  1330 \section{Formale Beschreibung der Hierarchie von Problemen}
  1331 
  1332 \section{Skripttaktiken}
  1333 Tats\"achlich sind es die tactics, die die Berechnungen vorantreiben: im Hintergrund bauen sie den proof tree 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 tactics; die Semantik ist beschrieben etwas weiter unten im Kontext mit tactics, die die Benutzer/Innen dieses Programmes verwenden: Es gibt einen Schriftverkehr zwischen den user-tactics und den script tactics.
  1334 
  1335 
  1336 
  1337 \part{Authoring on the knowledge}
  1338 
  1339 
  1340 \section{Add a theorem}
  1341 \section{Define and add a problem}
  1342 \section{Define and add a predicate}
  1343 \section{Define and add a method}
  1344 \section{}
  1345 \section{}
  1346 \section{}
  1347 \section{}
  1348 
  1349 
  1350 
  1351 \newpage
  1352 \bibliography{bib/isac,bib/from-theses}
  1353 
  1354 \end{document}