Department Mathematik
print


Navigationspfad


Inhaltsbereich

Logik II

Zeit und Ort

Vorlesung: Mo 8-10 und Mi 8-10, A027.
Übung: Fr 8-10, A027.
Praktikum: Mo 10-12, B134.

Inhalt

Gentzens Kalkül des natürlichen Schliessens. Minimallogik und Einbettung der klassischen und intuitionistischen Logik. Curry-Howard Korrespondenz. Normalisierung. Berechenbare Funktionale. Induktiv und koinduktiv definierte Prädikate. Realisierbarkeit und rechnerischer Gehalt von (dekorierten) Beweisen. Korrektheitssatz mit Anwendungen.

Skriptum

1. Logic (Stand 10. Mai), 2. Computability (Stand 7. Juni), 3. A theory of computable functionals (Stand 26. Juni), 4. Computational content of proofs (Stand 19. Juli).
Appendix A. Denotational semantics: proofs

Ü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, 11.
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.

Sprechstunden

  • Christian Ittner [mail[at]christian-ittner.de], nach Vereinbarung
  • Iosif Petrakis [petrakis[at]math.lmu.de], Mi 13:00-14:00, B418.
  • Helmut Schwichtenberg, Mi 13:00-14:00, B421.
  • Franziskus Wiesnet [Franziskus.Wiesnet[at]gmx.de], Mo 15:00-18:00, B420.
  • Chuangjie Xu [xu[at]math.lmu.de], Mi 14:00-15:00, B420.

Literatur

  • Schwichtenberg/Wainer, Proofs and Computations. Cambridge 2012
  • Troelstra/Schwichtenberg, Basic Proof Theory. Cambridge 2000
  • van Dalen, Logic and Structure. Berlin 1980

Minlog

Zum interaktiven Erzeugen von Beweisen kann man sich in dem Tutorium für den Beweisassistenten Minlog informieren. Eine ausführliche Einführung (von Franziskus Wiesnet) ist hier.
Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert. Falls git auf Ihrem Rechner installiert ist, können Sie die jeweils aktuelle Version von Minlog erhalten durch Ausführen von
git clone http://www.math.lmu.de/~minlogit/git/minlog.git.
Bitte arbeiten Sie mit dem dev-Zweig (durch Ausführen von git checkout dev).

Praktikum

Viele Teile der in der Vorlesung entwickelten Theorie können in einem Beweisassistenten implementiert werden. In dem Praktikum wird die Möglichkeit geboten, eine vereinfachte Version von Minlog im Einzelnen kennenzulernen, und auch eigene Ideen zu implementieren. Das Praktikum ist ein Zusatzangebot (der Inhalt also kein Gegenstand der Prüfung); betreut wird es von Christian Ittner und Chuangjie Xu. Zeit und Ort: Montag 10-12, B134.
Skript zum Praktikum: Scheme (Stand 19. Mai).
Übungen zum Praktikum (Stand 19. Juni).

Prüfungsform

Mündliche Prüfung, mit Benotung. Prüfungstermine: Montag 31. Juli und Freitag 4. August.

Studienordnungen

Die Vorlesung (mit Übung) ist unter WP 29 (bzw. WP35) in der Masterstudienordnung Mathematik (bzw. Wirtschaftsmathematik) mit 9 ECTS Punkten aufgelistet. Für Bachelorstudenten kann sie als ausgewähltes Thema der Mathematik unter WP 20 nach PO 2015 oder bei einem späteren Masterstudium angerechnet werden.

Letzte Änderung

19. Juli 2017