\chapter{Kurzfassung}

\begin{german}

Multicore-Prozessoren sind im Personal Computing Bereich mittlerweile ein etablierter Standard. Ähnlich der {\em Softwarekrise} um 1970 ist aber die Entwicklung von Software, die diese Hardware effizient nutzen kann, immer noch ein schwieriger, fehleranfälliger Prozess.

Funktionale Programmiersprachen basieren auf einem Programmierstil ohne Nebeneffekten und sollen daher für diese Art von Aufgaben besonders geeignet sein. Eine Anwendung solcher Sprachen sind computerbasierte Theorembeweiser. Wegen ihrer Begründung in Mathematik und Logik liegt funktionale Programmierung als Paradigma besonders nahe. {\em Isabelle} ist ein Framework für interaktives Beweisen von Theoremen, dessen Backend in {\em Standard ML} entwickelt wurde. Die Implementierungsarbeiten der letzten Jahre haben dazu geführt, dass das System nun die Ressourcen moderner Multicore-Prozessorarchitekturen besonders wirkungsvoll einsetzen kann. Das Mathematiklernsystem \isac{} baut auf {\em Isabelle} auf und war damit bis vor Kurzem das einzige seiner Art, welches auf Theorembeweisertechnologien basiert.

Diese Arbeit dokumentiert die Einführung von {\em Isabelle}s Parallelitätskonzepten in \isac{} und gibt einen Überblick über dafür relevante Technologien wie Grundlagen der Parallelität, unterschiedliche Ansätze zu Parallelität in funktionaler Programmierung und maschinengestützes Beweisen. Außerdem werden die Architekturen {\em Isabelle}s und \isac{}s vorgestellt, die beide Mechanismen zur Kommunikation mit der {\em Java Virtual Machine} für ihre Frontends beinhalten. Damit werden die Stärken funktionaler und imperativer Programmierung kombiniert und beide Paradigmen jeweils zur Lösung jener Probleme eingesetzt, für die sie besonders angemessen sind. Die Ergebnisse der Parallelisierung sind vielversprechend und werden es ermöglichen, dass eine große Anzahl von Schülern und Studenten gleichzeitig einen schnell reagierenden \isac{} Server für Berechnungen beanspruchen kann.

\end{german}