Logik II

Zeit und Ort

Vorlesung: Mo, Mi 8:25-10, A027. Beginn: Montag 17. April 2023.

Übung: Fr 8:30-10, A027. Beginn: Freitag 21. 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.

Skriptum

Introduction. vii-viii

1. Logic. 1-12

2. Computable functionals. 13-34

3. A theory TCF of computable functionals. 35-53

4. Computational content of proofs. 55-62

5. Applications. 63-76

Das vollständige Skriptum mit Inhalts- und Literaturverzeichnis sowie einem Index finden Sie hier. Zum Anwendungskapitel gehört die Datei sdindav.scm.
Anhang A: Atomic coherent information systems

Anhang B: Unification

Anhang C: Denotational semantics

Anhang D: Realizers for axioms

Anhang E: Extensionality of extracted terms

Minlog-Dateien: 20230426.scm, 20230524.scm, 20230621.scm, 20230703.scm, 20230705.scm, 20230719.scm.

Übungen

Bitte melden Sie sich hier an.

ueb01, ueb01.scm (Lösungshilfe für Minlog-Aufgaben),

ueb02, ueb02.scm (Lösungshilfe für Minlog-Aufgaben),

ueb03,

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

Sprechstunden

Nils Köpp [koepp[at]math.lmu.de], Mi 11-12, B414.
Philippe Vollmuth [ph.vollmuth[at]gmail.com]. 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 dem mitgelieferten Tutorium 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) ist ueb00.scm.

Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert.

Prüfungsform

Mündliche Prüfung, mit Benotung. Prüfungstermin: Montag 31. Juli im B251.
Der Nachhol-Prüfungstermin ist am Montag 25. September im B252.
Bitte melden Sie sich per email bei Herrn Köpp 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

19. Juli 2023