Vorlesung: Einführung in die Logik
Sommersemester 2024
Neuigkeiten
- 25. März
-
Die erste Vorlesung findet am Mittwoch, den 10. April statt.
- 04. April
-
Die erste große Übung findet am Montag, den 08. April statt.
- 15. April
-
Anmeldung zu den kleinen Übungen ab heute um 13:10 möglich auf StudIP.
- 16. April
-
Die Termin-Informationen zu den kleinen Übungen auf StudIP sind falsch.
Richten Sie sich bitte nach den Informationen weiter unten auf dieser Seite.
- 22. April
-
Neue Abgabegruppen für die kleinen Übungen sind verfügbar.
- 26. April
-
Videos und Notizen zur Vorlesung aus vergangenen Semestern als Material hinzugefügt.
Vorlesung
-
Der Prüfer und Modulverantwortliche ist Prof. Dr. Roland Meyer.
-
Die Vorlesungen werden von Jens Gutsfeld gehalten, die großen Übungen werden von Sören van der Wall gehalten.
-
Eintrag im Vorlesungsverzeichnis,
-
Vorlesungstermin:
Mittwoch, 09:45 - 11:15 in PK 11.1
Übungsbetrieb
-
Große Übung: Montags, 11:30 - 13:00 in PK 11.1,
-
Kleine Übungen, alle zwei Wochen (KW 18, 20, 22, 24, 26, 28), in IZ 358:
Übungsblätter
Die Übungsblätter werden hier hochgeladen und online im StudIP abgegeben.
Um die Übungsblätter abzugeben, müssen Sie in einer Dreiergruppe im StudIP eingetragen sein !
Schreiben Sie auf Ihre Abgaben unbedingt:
den Namen, die Matrikelnummer,
den Studiengang und eine E-Mail
Adresse aller Gruppenmitglieder!
Kontaktieren Sie bei Fragen zu den Präsenzblättern Ihren Tutor.
Modul
Um das Modul erfolgreich abzuschließen, sind zwei Leistungen zu erbringen:
- Prüfungsleistung: Sie bestehen die schriftliche Abschlussklausur.
- Studienleistung: Sie erreichen mindestens 50% der Punkte in den Übungsaufgaben.
Material
Der Foliensatz, der in den Vorlesungen präsentiert wird.
Videos zur Vorlesung aus vergangenen Semestern.
- Einführung und Kompaktheit:
Folien,
Beispiel zur Semantik,
Beweis des Lemmas zur Fortsetzung von Belegungen,
Beweis der aufbauenden Folgerung,
Beweis des Deduktionstheorems (semantische Version),
Beweis des Kompaktheitssatzes.
- Deduktive Systeme:
Folien,
Beispielbeweis zur Vollständigkeit einer Operatorenmenge,
Beweis des Deduktionstheorems (syntaktische Version).
- F0:
Beweise in F0,
Beweis mittels Inkonsistenz,
Vollständigkeit von F0.
- Sequenzen, Typsysteme und Tableaus:
Folien zum Sequenzenkalkül,
Beispielbeweis im Sequenzenkalkül,
Typsysteme,
Beispiele zu Tableaus.
Folien zu Tableaus.
- Normalformen, Davis-Putnam:
Folien zu Normalformen,
Beispiel zu Tseitin mit Syntaxbaum,
Beispiele zu Davis-Putnam,
Folien zu Davis-Putnam.
- Resolution, BMC:
Beispiel zur Resolution,
Folien zur Resolution,
Widerlegungsvollständigkeit der Resolution,
Bounded-Model-Checking.
- Syntax und Semantik der Prädikatenlogik:
Folien,
Lassie und Nemo.
- Substitution und Normalformen:
Folien,
Beispiel zur Substitution,
Anwendung des Substitutionslemmas,
Pränexnormalform,
Beispiel zur Skolemisierung,
Beweis des Satzes von Skolem.
- Herbrand-Theorie:
Folien,
Beispiel zu Herbrand-Strukturen,
Beweis des Satzes von Herbrand.
- Algorithmus von Gilmore und Kompaktheit:
Folien,
Beispiel zur Herbrand-Expansion,
Diskussion zur Auffassung von E(A) als Menge aussagenlogischer Formeln,
Beweis des Satzes von Gödel, Herbrand und Skolem,
Beweis des Kompaktheitssatzes,
Existenz von Nicht-Standardmodellen der Arithmetik.
- System F:
Folien.
Handschriftliche Notizen zur Vorlesung.
Literatur
-
Enderton: A Mathematical Introduction to Logic, Academic Press.
-
Schöning: Logik für Informatiker, Spektrum Akademischer Verlag.
-
Ebbinghaus et. al.: Einführung in die mathematische Logik, Spektrum Akademischer Verlag.
-
Huth and Ryan: Logic in Computer Science, Cambridge University Press.
-
Ben-Ari: Mathematical Logic for Computer Science, Springer-Verlag.
-
Nissanke: Introductory Logic and Sets for Computer Scientists, Pearson.
-
S. Hedman: A First Course In Logic, Oxford University Press.
-
Yosuhara: Recursive Function Theory and Logic, Academic Press.
-
Mancosu, Galvan Zach: An Introduction To Proof Theory, Oxford University Press.
-
Papadimitriou and Doxiadis: Logicomix: An Epic Search For Truth, Bloomsbury, deutsche Ausgabe bei Atrium.
