Seminar: Rechnerischer Gehalt von Beweisen
Zeit und Ort
Mi 14-16, B252; Beginn 4. Mai 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 4. Mai verteilt.
- Injektive Funktionen auf endlichen Mengen
(AutoMath). Stephan Kulla 18.5.
- Theoretische Grundlagen, induktiv definierte Prädikate.
Davide Rinaldi, 25.5. und 1.6.
- Zulässige Substitutionen.
Folien und Tafelanschrieb.
Anton Freund 15.6.
- Der Mengenbegriff in der konstruktiven Analysis.
Christian Neukirchen 22.6.
- Verwendung klassischer Schlußweisen in der konstruktiven Analysis.
Thilo Weghorn 6.7.
- Der Fächersatz.
Sifis Petrakis 13.7.
- Lambda-Terme als Datentyp (?)
- Das Dicksonsche Lemma (?)
Sprechstunde
Helmut Schwichtenberg ,
Mi 13-14, B415
Letzte Änderung
17. Juni 2011
