Department Mathematik
print


Navigationspfad


Inhaltsbereich

Seminar: Rechnerischer Gehalt von Beweisen

Zeit und Ort

Mi 14-16, B041; Beginn 19. Oktober 2011

Inhalt

Es sollen Theorie und Praxis der Extraktion von Programmen aus Beweisen erarbeitet werden. Vorausgesetzt werden Kenntnisse in Mathematischer Logik (eine einführende Vorlesung, insbesondere Vertrautheit mit Gentzens System des natürlichen Schließens). Ferner wird vorausgesetzt, daß die Teilnehmer das Tutorium des Beweisassistenten Minlog durchgearbeitet haben.

Vorträge

Die Vorträge wurden in der ersten Seminarsitzung am 19. Oktober verteilt (Daten sind vorläufig):
  • Einführung. Helmut Schwichtenberg, 26.10., 2. und 16.11.
  • Konstruktive Analysis. Matthias Benkard, 23. und 30.11.
  • Stetigkeit in der konstruktiven Analysis. Lucas Hoffmann, 7. und 14.12., 11.1.
  • Stream computation of the average. Kenji Miyamoto, 18.1.
  • Higman's lemma. Iosif Petrakis, 25.1. und 1.2.

Materialien

Skript Konstruktive Analysis (Überarbeitung des gleichnamigen Skripts vom SS 2005); es soll im Verlauf des Seminars vervollständigt werden. Hilfreich sind die Arbeiten Ferner sollte man changes.scm zu Minlog hinzuladen. Die Dateien real11.scm, cont11.scm und extraction11.scm sollen im Verlauf des Seminars weiterentwickelt werden.

Sprechstunde

Helmut Schwichtenberg , Mi 13-14, B421

Letzte Änderung

1. Februar 2011