Projektseminar: Rechnergestuetztes Beweisen
|
|
|
|
|
Veranstaltungsnummer: 18.376
Titel: Projektseminar: Rechnergestütztes Beweisen
Veranstalter: Mark-Oliver Stehr, Manfred Kudlek
Zeit und Ort: Fr. 14-16 C221
Inhalt: Logik höherer Ordnung und Typtheorie bilden die theoretische Basis für viele moderne, universelle Beweisassistenten. Je nach Interesse der Teilnehmer sollen verschiedene Systeme wie ISABELLE, LEGO und COQ sowie ihre zugrundeliegenden Theorien behandelt werden. Zur praktischen Einführung in die Systeme sind zunächst einige einfache Übungen aus den Bereichen Mathematik und Informatik geplant. Angestrebt wird schließlich der Entwurf einer größeren Theorie im Bereich Spezifikation und Verifikation von nebenläufigen Programmen oder Systemen. Als Spezifikationssprache bietet sich die Verwendung einer temporalen Logik an. Zur Modellierung der Systeme könnten Petrinetze eingesetzt werden. Aber auch die Möglichkeiten der Verwendung anderer Ansätze (wie z.B. Prozeßalgebren) sollen diskutiert werden.
Lernziel: Geübt werden soll der theoretische und praktische Umgang mit formalen Methoden. In Seminarvorträgen und praktischen Übungen sollen sich die Teilnehmer Kenntnisse erarbeiten, die notwendig sind, Beweisassistenten effizient einzusetzen. Die Teilnehmer sollen lernen, den Aufwand und den Nutzen von Formalisierungen abzuschätzen. Es soll ferner eine systematische Vorgehensweise beim Theorieentwurf bzw. der Theorieentwicklung vermittelt werden, die analog zur Vorgehensweise beim Softwareentwurf bzw. bei der Programierung ist.
Stellung im Studienplan: Hauptstudium, Vertiefungsgebiete:Th1, Th2, Th4
Voraussetzungen: Interesse an formalen Methoden
Vorgehen: Projektseminar
Literatur:
L.C.Paulson:
The next 700 theorem provers, In: Logic and Computer Science,
Academic Press, 1990
L.C.Paulson:
Isabelle: a generic theorem prover, LNCS 828,
Springer-Verlag, 1994
M.O.Stehr:
Skript zur Vorlesung Typtheorie im SS 97, 1997
K. M. Chandy, J. Misra:
Parallel Program Design. A Foundation,
Addison-Wesley, 1988
Z. Manna, A. Pnueli:
The Temporal Logic of Reactive and Concurrent Systems,
Springer-Verlag, 1992
Periodizität: unregelmäßig
Eignung: Für Lehrer und Nebenfächler nicht geeignet.
Stichworte: Logik höherer Ordnung, Typtheorie, Verifikation, Spezifikation
Last Change: 17:40 05/19/2011 Imprint/Disclaimer