wneuper/isa: comparison doc-src/isac/mlehnfeld/projektbericht.tex

equal deleted inserted replaced

-:ee2c2928150e
+:59b7fd45b037
 \item \textbf{Den Benutzer anleiten}: Wei\3 der Lernende nicht mehr weiter, so kann das System den n\"achsten Schritt vorschlagen und den Benutzer so Schritt f\"ur Schritt zum Ergebnis f\"uhren. Ein \sisac{}-Programm wird so interpretiert, wie es bei einem Debugger passiert; die Breakpoints (i.e. Schritte) sind als bestimmte Statements im Programm definiert, die notwendigerweise zum Verlauf der Rechnung bzw. deren Aufbau geh\"oren. An den Breakpoints kann der Benutzer frei entscheiden, ob er den n\"achsten Schritt generieren lassen m\"ochte oder ob er versucht, selbst weiter zu rechnen. Die Herausforderung f\"ur den \textit{Lucas-Interpreter} ist, mit beliebigen Benutzereingaben umgehen zu k\"onnen.
 \item \textbf{Schritte erkl\"aren}: Bei Interesse hat der Lernende Zugang zu dem Wissen, das f\"ur einen mechanisierten \textit{math assistant} zur L\"osung mathematischer Probleme von N\"oten ist: Definitionen, Axiome und Theoreme (erfasst in ``theories''\footnote{siehe http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index\_thy.html}), Spezifikationen von Problemklassen\footnote{siehe z.B. http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html} und Programme, um die Probleme zu l\"osen\footnote{siehe http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html}. Theoretisch ist dieses Wissen ausreichend, automatisch Erkl\"arungen f\"ur die einzelnen Schritte zu generieren. Das Hintergrundwissen liegt zwar in mathematischer Formulierung vor, es ist jedoch fraglich, wie dies in eine Form gebracht werden kann, die den Lernenden nicht \"uberfordert.
 \end{enumerate}
 \subsection{Isabelles Konzept von ``contexts''}
-Die Beschreibung dieses bew\"ahrten Konzeptes findet sich in einem internen Papier zur Implementatierung von Isabelles Beweissprache Isar \cite{isar-impl}. Isabelle stellt einen sehr generellen Funktor zur Verf\"ugung:
+Die Beschreibung dieses bew\"ahrten Konzeptes findet sich in einem internen Papier zur Implementierung von Isabelles Beweissprache Isar \cite{isar-impl}. Isabelle stellt einen sehr generellen Funktor zur Verf\"ugung:
 {\tt
 \begin{tabbing}
 xx\=xx\=in\=\kill
 structure ContextData =  {Proof\_Data}\\
 \>$[{x = 0}, x = \frac{6}{5}]$ \\
 \`{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
 \>$[x = \frac{6}{5}]$ \\
 $[x = \frac{6}{5}]$
 \end{tabbing}
-Aufgrund von Punkt \ref{conflict}. oben wird es m\"oglich, aus dem Programm, das obige Rechnung erzeugt, das Statement \textit{Chec\_Elementwise Assumptions} zu streichen:
+Aufgrund von Punkt \ref{conflict}. oben wird es m\"oglich, aus dem Programm, das obige Rechnung erzeugt, das Statement \textit{Check\_Elementwise Assumptions} zu streichen:
 {\tt
 \begin{tabbing}
 xx\=xx\=xx\=xx\=xx\=xx\=\kill
 Script Solve\_root\_equation (e\_e::bool) (v\_v::real) =      \\
 \> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@   \\
 \subsection{L\"osungsphase mit {\it context}s}
 Die Integration von {\it context}s in die Lösungsphase zur Ersetzung der ursprünglichen behandlung von Assertions konnte in enger Zusammenarbeit mit Herrn Neuper fertiggestellt werden, persönliche Termine auf beiden Seiten verlängerten aber den zeitlichen Verlauf. Der Code des Lucas-Interpreters ist jetzt sauberer und die Logik vereinfacht.
 \section{Abschließende Bemerkungen}
-Rückblickend betrachte ich das Projektpraktikum als sehr positive Erfahrung, da ich das Gefühl habe, etwas nicht Unwesentliches  zur Erweiterung von \sisac{} beigetragen zu haben. Die persönliche Zusammenarbeit mit Akademikern und auch die Verrichtung einer Arbeit, die nach Abschluss gebraucht und verwendet wird, ist eine Erfahrung, die ich im Verlauf meines Studiums leider erst einmal davor machen durfte.\\
+Rückblickend betrachte ich das Projektpraktikum als sehr positive Erfahrung, da ich das Gefühl habe, etwas nicht Unwesentliches  zur Erweiterung von \sisac{} beigetragen zu haben. Die persönliche Zusammenarbeit mit Akademikern und auch die Verrichtung einer Arbeit, die nach Abschluss gebraucht und verwendet wird, ist eine Erfahrung, die in meinem Studium nicht selbstverständlich ist und um die ich mich sehr bemüht habe.\\
 Der nicht zuletzt durch das überraschend notwendig gewordene Update bedingte zähe Verlauf bis ich endlich wirklich an der eigentlichen Aufgabenstellung arbeiten konnte war etwas ernüchternd, da ich gehofft hatte, das Praktikum bis spätestens Ende März abschließen zu können.\\
 Die Zusammenarbeit mit Herrn Neuper hat jedenfalls sehr gut funktioniert und aus meiner Sicht haben wir uns sehr gut verstanden. Das hat ein entspanntes Arbeitsklima ermöglicht.\\
-Da mir bis zum Abschluss meiner Arbeit nicht bewusst war, dass eine Präsentation zu halten und ein umfangreicher Projektbericht abzufassen sind, musste ich den für eine Lehrveranstaltung von 6 ECTS vorgesehenen Arbeitsaufwand deutlich überschreiten. Das und die zeitliche Verzögerung des Projektes geben der Freude über den erfolgreichen Abschluss der geplanten Aufgaben und deren interessanten Charakter einen bitteren Beigeschmack.
+Abgesehen von der zeitlichen Verzögerung des Projektes freue ich mich über den erfolgreichen Abschluss der geplanten Aufgaben und deren interessanten Charakter.
 \clearpage
 \bibliography{bib}

branch	decompose-isar
changeset 42038	59b7fd45b037
parent 42037	ee2c2928150e
child 42039	9b04517e3f28