Zur Hauptnavigation Zum Inhaltsbereich Zur Suche Zum Seitenfu├č


Projektseminar: Rechnergestuetztes Beweisen

Deutsche Version. This page is available in German only. Cette page n'existe qu'en Allemand. Ésta página sólo existe en Alemán.


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

Letzte Änderung: 17:40 19.05.2011
Impressum