Ausgewählte Kapitel aus der Beweistheorie
Zeit und Ort
Vorlesung: Mi 10-12, A027; Beginn 17. April 2013. Am 26. Juni fällt die Vorlesung aus.Übung: Fr 10-12, A027. Beginn 19. April 2013. Die Übung am 28. Juni findet statt.
Inhalt
Anfangsfälle der transfiniten Induktion. Berechenbare Funktionale. Induktiv definierte Prädikate. Realisierbarkeit und rechnerischer Gehalt von Beweisen.Skriptum
Wird hier veröffentlicht. Kapitel 1: Proof theory of arithmetic, Stand 24. April,Kapitel 2: Computablity in higher types, Stand 12. Juni,
Kapitel 3: Extracting computational content from proofs, Stand 17. Juli.
Es gibt auch ein Gesamtskript, mit Index und Literaturangaben.
Übungen
Bitte melden Sie sich hier an.Übungsblätter werden an dieser Stelle veröffentlicht: Übung 1, 2, 3, 4, 5, 6, 7, 8, 9, 10.
Die Lösungen werden in der Übungsstunde präsentiert. Dort werden auch die korrigierten Übungsblätter verteilt, danach im Rückgabekasten im 1. Stock. Abgabe bitte in der Vorlesung.
Tutorium
Es wird ein Tutorium angeboten. Tutor: Anton Freund. Zeit: Mi 16-18, B252.Sprechstunden
- Anton Freund [anton.freund[at]campus.lmu.de]. Nach Vereinbarung.
- Lucas Hoffmann [Lucas.Hoffmann[at]campus.lmu.de]. Zeit 14-15, Gumbel.
- Kenji Miyamoto, Di 13-14, B420.
- Helmut Schwichtenberg , Mi 13-14, B421.
Literatur
- Troelstra/Schwichtenberg, Basic Proof Theory. Cambridge 2000
- Schwichtenberg/Wainer, Proofs and Computations. Cambridge 2012
Minlog
Zum interaktiven Erzeugen von Beweisen kann man sich in dem Tutorium für den Beweisassistenten Minlog informieren. Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert. Eine Datei ind.scm mit einfachen Beispielen zu Induktionsbeweisen finden Sie hier. Hinweise zu Aufgabe 11 finden Sie hier. Hinweise zu Blatt 7 finden Sie in ueb07.scm. Hinweise zu Blatt 8 finden Sie in ueb08.scm. Hinweise zu Blatt 9 finden Sie in ueb09.scm. Hinweise zu Blatt 10 finden Sie in ueb10.scm.Klausuren
Es wird eine Klausur geschrieben, und zwar am Freitag, 19. Juli 2013, 10:00-12:00, im A027. Hilfsmittel (Bücher, Skripten etc.) sind in der Klausur nicht zugelassen; Schreibpapier wird gestellt. Bitte einen Lichtbildausweis mitbringen.Die Ergebnisse der Klausur können per email erfragt werden, und zwar bis Mittwoch, 14. August bei Helmut Schwichtenberg unter schwicht at math dot lmu dot de und danach bei Maria Ketnath unter sekrsch2 at math dot lmu dot de. Eine Klausureinsicht ist möglich am Freitag, dem 9. August, 12:30 - 13:30 im Raum B421.