Logik II: Beweise und Programme

Zeit und Ort

Vorlesung: Mo, Mi 8:30-10, A027. Beginn: Montag 13. April 2026.

Übung: Fr 8:30-10, A027. Beginn: Freitag 17. April.

Inhalt

Minimallogik und Einbettung der klassischen und intuitionistischen Logik, Curry-Howard Korrespondenz. Stetige Funktionale: Semantik und axiomatische Behandlung. Induktiv und coinduktiv definierte Prädikate. Realisierbarkeit und rechnerischer Gehalt von Beweisen. Korrektheitssatz mit Anwendungen. Die Vorlesung ist auch für interessierte Studenten geeignet, die keine einführende Logik-Vorlesung gehört haben. Die notwendigen Kenntnisse (natürliches Schliessen, Curry-Howard Korrespondenz) werden am Anfang der Vorlesung vermittelt.

Skriptum

Das vollständige Skript mit Inhaltsverzeichnis, Bibliographie und Index finden Sie hier.

Übungen

ueb01, sowie peirce.scm, disj.scm, refl.scm (Lösungshilfen für Minlog-Aufgaben).

ueb02, sowie mints.scm, natpluscomm.scm, natplus.scm (Lösungshilfen für Minlog-Aufgaben).

ueb03, sowie quotremuniq.scm (Lösungshilfe für die Minlog-Aufgabe).

ueb04, sowie np.scm (Lösungshilfe für die Minlog-Aufgaben),

ueb05, sowie natpluscomm.scm (Lösungshilfe für die Minlog-Aufgabe),

ueb06, sowie sqrttwo.scm (Lösungshilfe für die Minlog-Aufgabe),

ueb07, sowie fib.scm (Lösungshilfe für die Minlog-Aufgabe),

ueb08, sowie heron.scm (Lösungshilfe für die Minlog-Aufgabe),

ueb09, sowie dy.scm (Lösungshilfe für die Minlog-Aufgabe),

ueb10, sowie heronb.scm (Lösungshilfe für die Minlog-Aufgabe),

ueb11, sowie ratsqrt.scm (Lösungshilfe für die Minlog-Aufgaben).

Sprechstunden

• Noah Wedlich. Bitte anmelden, wedlichn[at]gmail.com
• Katharina Wendler. Bitte anmelden, Wendler.Katharina[at]campus.lmu.de
• Helmut Schwichtenberg, Mi 13-14, B434.

Literatur

• Schwichtenberg/Wainer, Proofs and Computations. Cambridge 2012
• Troelstra/Schwichtenberg, Basic Proof Theory. Cambridge 2000
• van Dalen, Logic and Structure. Berlin 1980
• Skript Constructive analysis with witnesses
• Daniel Diessner, Die Vollständigkeit der reellen Zahlen

Minlog

Die Verwendung von Minlog ist ein wesentlicher Bestandteil der Vorlesung (also auch Gegenstand der Prüfung). Über Minlog kann man sich in den mitgelieferten Dateien tutor.pdf und ref.pdf informieren. Eine ausführliche Einführung (von Franziskus Wiesnet) ist hier. Sehr hilfreich ist auch eine Serie von Videos, die auch von Franziskus Wiesnet angefertigt wurden.

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). Eine konkrete Einführung (von Nils Köpp und Valentin Herrmann) ist ueb00.scm.

Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert. Wenn man "minlog-dev" in der Konsole eines CIP-Rechners eingibt wird der dev-Zweig aufgerufen. Minlog Web (von Valentin Herrmann) erlaubt das Arbeiten mit Minlog ohne das System zu installieren.

Prüfungsform

Mündliche Prüfung, mit Benotung. Voraussetzung für die Zulassung zur Prüfung ist das Erreichen von 30 Prozent der Punkte in den Übungen. Prüfungstermin: Montag 27. Juli im B414.
Der Nachhol-Prüfungstermin ist Freitag 9. Oktober auch im B414.
Bitte melden Sie sich per email bei Herrn Wedlich an.

Studienordnungen

Die Vorlesung (mit Übung) kann mit 9 ECTS-Punkten als Modul WP33 (Fortgeschrittene Themen aus der Logik) in der Masterstudienordnung Mathematik (2021) eingebracht werden. Für Bachelorstudenten kann sie bei einem späteren Masterstudium angerechnet werden.

Letzte Änderung

12. August 2026