Logik II
Zeit und Ort
Vorlesung: Mo, Mi 8-10, A027. Beginn: Montag 25. April 2022.
Übung: Fr 8-10, A027. Beginn: Freitag 29. 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
1. Logic. 01-12,
2. Computable functionals. 13-43,
3. A theory TCF of computable functionals. 45-61,
4. Computational content of proofs. 63-74.
5. Applications. 75-90.
Das vollständige Skriptum mit Inhalts- und Literaturverzeichnis sowie
einem Index finden Sie hier. Zum Anwendungskapitel gehört die
Datei
sdindav.scm.
Übungen
ueb01,
ueb01.scm (Lösungshilfe für Minlog-Aufgaben),
ueb02,
ueb02.scm (Lösungshilfe für Minlog-Aufgaben),
ueb03,
ueb03.scm (Lösungshilfe für Minlog-Aufgaben),
ueb04,
ueb04.scm (Lösungshilfe für Minlog-Aufgaben),
ueb05,
ueb05.scm (Lösungshilfe für Minlog-Aufgaben),
ueb06,
ueb06.scm (Lösungshilfe für Minlog-Aufgaben),
ueb07,
ueb07.scm (Lösungshilfe für Minlog-Aufgaben),
ueb08,
ueb08.scm (Lösungshilfe für Minlog-Aufgaben),
ueb09,
ueb09.scm (Lösungshilfe für Minlog-Aufgaben),
ueb10,
ueb10.scm (Lösungshilfe für Minlog-Aufgaben),
ueb11,
ueb11.scm (Lösungshilfe für Minlog-Aufgaben).
Die Lösungen werden in der Übungsstunde präsentiert.
Dort werden auch die korrigierten Übungsblätter verteilt;
danach können sie im B414 abgeholt werden. Abgabe wahlweise
elektronisch
oder physisch (in der Vorlesung). Gemeinsame Lösungen sind
zugelassen.
Sprechstunden
- Nils Köpp [koepp[at]math.lmu.de], Mi 11-12, B414.
- Philippe Vollmuth [ph.vollmuth[at]campus.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 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. Um die CIP-Pools benutzen zu können brauchen die
Studierenden eine entsprechende Kennung. Um eine Kennung zu erhalten
ist die vollständige Teilnahme an einem ca. einstündigen
Einführungskurs zwingende Voraussetzung. Sie können sich
hier
für einen Kurs eintragen. Die limitierten Plätze werden dann
in Reihenfolge der Eintragung zugeteilt. Im Anmeldungsformular stehen
auch alle bisher angesetzten Termine für
Einführungsveranstaltungen.
Prüfungsform
Mündliche Prüfung, mit Benotung.
Prüfungstermin: Mittwoch 17. August im B252.
Der Nachhol-Prüfungstermin ist am Freitag 23. September (vormittags,
auch 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
29. Juli 2022