Einführung in die Logik SS25

News

• 29. April: Die Übung von Gruppe 4 am 01. Mai fällt aus. Sie findet stattdessen am 08. Mai statt.

• 29. April: Es gibt dieses Semester den Lerntreff Theorie, in dem Sie Fragen rund um die theoretischen Fächer des Bachelors Informatik stellen können.

• 22. April: Am 23. April findet anstelle der großen Übung eine Vorlesung statt. Raum bleibt PK 11.1.

• 15. April: Ab dem 16. April um 15:00 Uhr können Sie sich im StudIP in die Übungsgruppen eintragen.

• 20. Februar: Die Informationen auf dieser Seite sind vorläufig.

Organisation

• Die Vorlesung wird von Prof. Dr. Roland Meyer gehalten. 
• Turnus: nur im Sommersemester
• Arbeitsaufwand: 42 h Präsenzstudium + 108 h Selbststudium
• Vorlesungstermin: Montag, 11:30 - 13:00 in PK 11.2
• Große Übung/Vorlesung: Mittwoch, 09:45 - 11:15 in PK 11.1
• Kleine Übungen: Anmeldung im StudIP (sobald freigeschaltet).
• Prüfungstermin: 29. Juli 2025, 16:00-18:00.
• Die Vorlesung beginnt am 14.04.

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

Folien

• Lemma 1-7 für das Beweisen in F0

Videos 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.

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.