336 {\footnotesize\begin{verbatim} |
336 {\footnotesize\begin{verbatim} |
337 > rewrite; |
337 > rewrite; |
338 val it = fn |
338 val it = fn |
339 : |
339 : |
340 theory' -> |
340 theory' -> |
341 rew_ord' -> |
341 rew_ord -> |
342 rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option |
342 rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option |
343 \end{verbatim}} |
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. |
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} |
345 {\footnotesize\begin{verbatim} |
346 > rewrite_inst; |
346 > rewrite_inst; |
347 val it = fn |
347 val it = fn |
348 : |
348 : |
349 theory' -> |
349 theory' -> |
350 rew_ord' -> |
350 rew_ord -> |
351 rls' ->bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option |
351 rls' ->bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option |
352 \end{verbatim}} |
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. |
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. |
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)}. |
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)}. |
434 val it = "?s = ?t ==> ?t = ?s" : Thm.thm |
434 val it = "?s = ?t ==> ?t = ?s" : Thm.thm |
435 > rearrange_assoc; |
435 > rearrange_assoc; |
436 val it = |
436 val it = |
437 Rls |
437 Rls |
438 {id = "rearrange_assoc", |
438 {id = "rearrange_assoc", |
439 scr = Script (Free ("empty_script", "RealDef.real")), |
439 program = Script (Free ("empty_script", "RealDef.real")), |
440 calc = [], |
440 calc = [], |
441 erls = |
441 asm_rls = |
442 Rls |
442 Rls |
443 {id = "e_rls", |
443 {id = "e_rls", |
444 scr = EmptyScr, |
444 program = EmptyScr, |
445 calc = [], |
445 calc = [], |
446 erls = Erls, |
446 asm_rls = Erls, |
447 srls = Erls, |
447 prog_rls = Erls, |
448 rules = [], |
448 rules = [], |
449 rew_ord = ("dummy_ord", fn), |
449 rew_ord = ("dummy_ord", fn), |
450 preconds = []}, |
450 preconds = []}, |
451 srls = |
451 prog_rls = |
452 Rls |
452 Rls |
453 {id = "e_rls", |
453 {id = "e_rls", |
454 scr = EmptyScr, |
454 program = EmptyScr, |
455 calc = [], |
455 calc = [], |
456 erls = Erls, |
456 asm_rls = Erls, |
457 srls = Erls, |
457 prog_rls = Erls, |
458 rules = [], |
458 rules = [], |
459 rew_ord = ("dummy_ord", fn), |
459 rew_ord = ("dummy_ord", fn), |
460 preconds = []}, |
460 preconds = []}, |
461 rules = |
461 rules = |
462 [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), |
462 [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), |
1110 {\it eval\_rls } |
1110 {\it eval\_rls } |
1111 & rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\ |
1111 & rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\ |
1112 {\it fmz} |
1112 {\it fmz} |
1113 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\ |
1113 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\ |
1114 {\it met} |
1114 {\it met} |
1115 & eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\ |
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} |
1116 {\it metID} |
1117 & bezieht sich auf {\it met}\\ |
1117 & bezieht sich auf {\it met}\\ |
1118 {\it op} |
1118 {\it op} |
1119 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\ |
1119 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\ |
1120 {\it pbl} |
1120 {\it pbl} |
1125 & Anordnung beim Rewriting\\ |
1125 & Anordnung beim Rewriting\\ |
1126 {\it rls} |
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 \\ |
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} |
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)\\ |
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 scr} |
1130 {\it program} |
1131 & script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\ |
1131 & script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\ |
1132 {\it norm\_rls} |
1132 {\it norm\_rls} |
1133 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\ |
1133 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\ |
1134 {\it spec} |
1134 {\it spec} |
1135 & Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\ |
1135 & Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\ |
1152 \caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb} |
1152 \caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb} |
1153 \tabcolsep=0.3mm |
1153 \tabcolsep=0.3mm |
1154 \begin{center} |
1154 \begin{center} |
1155 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline |
1155 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline |
1156 tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\ |
1156 tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\ |
1157 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\ |
1157 & &thy &program &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\ |
1158 \hline\hline |
1158 \hline\hline |
1159 Init\_Proof |
1159 Init\_Proof |
1160 &fmz & x & & & x & & & & & & & x \\ |
1160 &fmz & x & & & x & & & & & & & x \\ |
1161 &spec & & & & & & & & & & & \\ |
1161 &spec & & & & & & & & & & & \\ |
1162 \hline |
1162 \hline |