|
neuper@42070
|
1 |
\chapter{Einf\"{u}hrung}
|
|
neuper@42072
|
2 |
Europa ist bei Computer Theorem Provern (CTP) weltweit f\"uhrend, die zwei prominenten Prover sind Coq \cite{coq1999} und Isabelle \cite{Paulson:Isa94}.
|
|
neuper@42072
|
3 |
Im Zuge der Weiterentwicklung der Informatik als Ingenieurs-Disziplin werden auch Anwendungsgebiete zunehmend mathematisiert \cite{db:dom-eng}, was wiederum CTP vermehrt auf den Plan ruft.
|
|
neuper@42072
|
4 |
CTP sind bis dato in H\"anden eines relativ kleinen Kreises von Experten, von denen der Gro{\ss}teil wiederum im akademischen Bereich arbeitet und nur ein kleiner Teil in der Industrie. Diese Experten bevorzugen Keyboard-Shortcuts (vor Men\"us), reine Texte (ohne mathematische Sonderzeichen) und benutzen auch mit gro{\ss}em Aufwand hergestellte CTP-Entwicklungs-Umgebungen nicht, zum Beispiel die CoqIDE.
|
|
neuper@42070
|
5 |
|
|
neuper@42072
|
6 |
Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software- Ingenieuren vorzudringen beginnen (siehe zum Beispiel \cite{aichernig:uni-iist-02,aichernig:mut-test}),% \cite{wolff10-boogie},
|
|
neuper@42072
|
7 |
stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen. Einer der Vorschl\"age, wie Theorem Prover mit Front-ends zu verbinden w\"are, findet sich in \cite{Aspinall:2007:FIP:1420412.1420429}. Isabelle geht einen anderen Weg, indem es sich aktuellen technischen Herausforderungen stellt \cite{makarius:isa-scala-jedit}: Multicore-Maschinen versprechen erh\"ohten Durchsatz, falls Teile von Beweisen parallel abgearbeitet werden k\"onnen. Isabelles Entwurf sieht vor, die Programmsprache Scala (insbesonders seine Actor-Library) als Bindeglied zwischen der Mathematik-Sprache SML und der g\"angisten Plattform f\"ur GUIs vor, der Java-Virtual-Maschine.
|
|
neuper@42070
|
8 |
|
|
neuper@42072
|
9 |
Die Bachelorarbeit l\"auft im Rahmen des ISAC-Projektes. ISACs experimenteller Mathematik-Assistant baut auf dem SML-Teil von Isabelle auf und es ist geplant, auch sein Frontend in entsprechend geplanten Schritten an die aktuelle Entwicklung von Isabelle anzuschlie{\ss}en. Der erste Schritt geht einen Umweg, um die Technologie kennen zu lernen: Nicht ISACs Rechnungen (mit aufw\"andigen Interaktionen), sondern Backs 'structured derivations' (SD) \cite{back-grundy-wright-98} sollen auf jEdit und Isabelle aufgesetzt werden. Die Bachelorarbeit liefert die Machbarkeits-Studie f\"ur diesen Schritt.
|