Seminar: Konstruktive Analysis
Zeit und Ort
Mo 14-16, B252; Beginn Montag, 15. Oktober 2018Inhalt
Es sollen die Grundlagen der konstruktiven Analysis erarbeitet werden. Die Beweise sollen auch in formalisierter Form geführt werden, um die Extraktion von Programmen zu ermöglichen. Vorausgesetzt werden Grundkenntnisse in Mathematischer Logik (mindestens der gleichzeitige Besuch der einführenden Vorlesung "Logik" von Prof. Merkl). Ferner wird vorausgesetzt, daß die Teilnehmer das Tutorium des Beweisassistenten Minlog durchgearbeitet haben.Nach erfolgreichem Besuch des Seminars ist es möglich, eine Bachelorarbeit zu einem Thema aus diesem Umkreis zu schreiben.
Vorträge
- Einführung in die konstruktive Logik. 22. Oktober 2018, Helmut Schwichtenberg (introlog.scm),
- Natürliche, positive, ganze und rationale Zahlen. Division mit Rest. 29. Oktober 2018, Helmut Schwichtenberg (intronum.scm),
- Reelle Zahlen: Gleichheit, Archimedische Eigenschaft. 5. November 2018, Sebastian Kleiner
- Nicht-negative und positive reelle Zahlen. 12. November 2018, Max Zeuner
- Arithmetische Funktionen. 19. November 2018, Florian Griesser (multiplication.scm),
- Vergleich reeller Zahlen. 26. November 2018, Sebastian Kleiner
- Überabzählbarkeit, Vollständigkeit. 3. Dezember 2018, Max Zeuner
- Nachtrag: Formale Beweise. 10. Dezember 2018, Max Zeuner (completeness.scm)
- Nachtrag: Formale Beweise. 17. Dezember 2018, Sebastian Kleiner (PlusPos.scm)
- Stetige Funktionen. 7. Januar 2019, Franziskus Wiesnet
- Zwischenwertsatz. 14. Januar 2019, Nils Köpp. Wegen Krankheit verschoben auf den 21. Januar.
Minlog
Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert (Aufruf: minlog). Falls git auf Ihrem Rechner installiert ist, können Sie die jeweils aktuelle Version von Minlog erhalten durch Ausführen vongit clone http://www.math.lmu.de/~minlogit/git/minlog.git
Bitte verwenden Sie (via git checkout dev) den dev-Zweig
Literatur
Allgemein
- Bishop/Bridges, Constructive Analysis. Springer 1985.
- Bridges/Vita, Techniques of Constructive Analysis. Springer 2006.
- A. Bauer, Five stages of accepting constructive mathematics (Bull AMS, 2016)
Speziell
- H. Ishihara, The constructive Hahn-Banach theorem, revisited
- N. Köpp, Automatically verified program extraction from proofs with applications to constructive analysis
- Skript Constructive analysis with witnesses
Sprechstunde
- Helmut Schwichtenberg, Mi 13-14, B421.