Logik II: Beweise und Programme

Zeit und Ort

Vorlesung: Mo, Mi 8:15-10, A027. Beginn: Montag 15. April 2024.
Übung: Fr 8:30-10, A027. Beginn: Freitag 19. April.

Inhalt

Minimallogik und Einbettung der klassischen und intuitionistischen Logik, Curry-Howard Korrespondenz. Berechenbare 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

Introduction. vii-viii
1. Logic. 01-11
2. Computable functionals. 13-20 (Stand 29. April 2024).

Übungen

Bitte melden Sie sich hier an.
ueb01, ueb01.scm (Lösungshilfe für Minlog-Aufgaben),
ueb02,
ueb03, ueb03.scm (Lösungshilfe für Minlog-Aufgaben). Gebraucht wird natplus.scm.

Sprechstunden

• Valentin Herrmann [valentin.herrmann[at]math.lmu.de]. Bitte anmelden.
• 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

Minlog

Viele Teile der in der Vorlesung entwickelten Theorie sind in dem Beweisassistenten Minlog implementiert. 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 den mitgelieferten Dateien tutor.pdf und ref.pdf informieren. Eine ausführliche Einführung (von Franziskus Wiesnet) ist hier. 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. Minlogpad (von Valentin Herrmann) erlaubt das Arbeiten mit Minlog ohne das System zu installieren.

Prüfungsform

Mündliche Prüfung, mit Benotung.

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

30. April 2024