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