Department Mathematik
print


Navigationspfad


Inhaltsbereich

Logik II

Zeit und Ort

Vorlesung: Mo, Mi 8-10, A027. Beginn: Montag 12. April 2021. Ende 14.Juli 2021. Wegen der aktuellen Situation wird die Vorlesung bis auf Weiteres in digitaler Form stattfinden. Zu jedem Vorlesungstermin finden Sie auf dieser Seite (1) eine pdf-Datei mit dem Vorlesungsstoff und (2) eine oder mehrere mp3-Dateien mit Kommentaren. Bitte drucken Sie die pdf-Datei aus und arbeiten Sie sie durch, wobei die Kommentare helfen sollten.

Übung und Tutorium: Beides wird von Herrn Nils Köpp [koepp[at]math.lmu.de] organisiert. Wenn Sie an der Vorlesung teilnehmen, schreiben Sie ihm bitte eine email.

Inhalt

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

Skriptum

Der jeweils aktuelle Stand wird hier veröffentlicht.
1. Logic. Kommentare. intro, 03-04, 04-05, 05-06, 07-08, 09-10, 11-12, 13-14, 15-16, 16-18.
2. Computability. Kommentare. 19-20, 20-22, 22-24, 24-27, 27-28, 29-30, 30-33, 33-35, 35-38, 38-40, 40-42, 42-43.
3. A theory TCF of computable functionals. Kommentare. 45-47, 47-50, 50-54, 54-57. 57-60, 60-64.
4. Computational content of proofs. Kommentare. 65-68, 68-70, 71-74, 75-77, 77-81.
5. Applications. Kommentare. 83-86, 86-88, 89-92, 92-95, 95-98.
Das vollständige Skriptum (mit Index und Referenzen) finden Sie hier.

Übungen

Der Übungsbetrieb, insbesondere die Abgabe und Korrektur der Übungsblätter, wird hauptsächlich über Uni2Work ablaufen. Die Übungsblätter werden online veröffentlicht und können digital als .pdf (oder .scm) in Uni2Work hochgeladen werden. Die korrigierte Abgabe sowie die Lösung des Übungsblattes finden Sie ebenfalls dort. Wegen verschiedener Korrektoren bitte pro Woche zwei getrennte Abgaben, für normale und für Minlog Aufgaben.

ueb00.scm (Vorbereitende Übungen mit Minlog),
ueb01, minlog01, ueb01.scm (Lösungshilfe für Aufgabe 4).
ueb02, minlog02, ueb02.scm (Lösungshilfe für Aufgabe 8).
ueb03, minlog03, ueb03.scm (Lösungshilfe für Aufgabe 12).
ueb04, minlog04, ueb04.scm (Lösungshilfe für Aufgabe 16).
ueb05, minlog05, ueb05.scm (Lösungshilfe für Aufgabe 20).
ueb06, minlog06, ueb06.scm (Lösungshilfe für Aufgabe 24), Abgabetermin verschoben auf den 9. Juni.
ueb07, minlog07, ueb07.scm (Lösungshilfe für Aufgabe 28).
ueb08, minlog08, ueb08.scm (Lösungshilfe für Aufgabe 32).
ueb09, minlog09, ueb09.scm (Lösungshilfe für Aufgabe 36).
ueb10, minlog10, ueb10.scm (Lösungshilfe für Aufgabe 40).

Sprechstunden

  • Nils Köpp [koepp[at]math.lmu.de]. Bitte anmelden.
  • Helmut Schwichtenberg, Mi 13-14, B434.
  • Philippe Vollmuth [ph.vollmuth[at]gmail.com]. Bitte anmelden.

Literatur

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

Minlog

Viele Teile der in der Vorlesung entwickelten Theorie können in einem Beweisassistenten wie Minlog implementiert werden. In einigen Übungsaufgaben wird die Möglichkeit geboten, dies in einfachen Fällen auszuprobieren. Die Verwendung von Minlog ist ein Zusatzangebot (also kein Gegenstand der Prüfung). Über Minlog kann man sich in dem mitgelieferten Tutorium 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.

Prüfungsform

Mündliche Prüfung, mit Benotung. Prüfungstermine: Donnerstag 29. Juli und Freitag 30. Juli.
Der Nachhol-Prüfungstermin ist am Montag 20. September (vormittags).
Bitte melden Sie sich per email bei Herrn Köpp an.

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 bei einem späteren Masterstudium angerechnet werden.

Letzte Änderung

14. Juli 2021