Department Mathematik
print


Navigationspfad


Inhaltsbereich

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.

Letzte Änderung

5. August 2013