Theoretical Computer Science

Vorlesung: Einführung in die Logik

Sommersemester 2021

Neuigkeiten

12. April

Die Vorlesung beginnt in der Woche zum 19. 04.

12. April

Bitte tragen Sie sich bis zum 23.04 zur Abgabe des ersten Blattes zu viert im StudIP als Abgabegruppe ein.

20. April

Anzahl der Gruppen im StudIP erhöht.

26. April

Gruppen auf Abgabgegruppen zugeteilt. Bitte geben Sie die Hausaufgabenblätter im StudIP ab. Ihren Abgabeordner können Sie aus der folgenden Liste ablesen:

• Abgabeordner 1: Gruppe 1 / 6 / 11 / ... (Kongruent 1 modulo 5)
• Abgabeordner 2: Gruppe 2 / 7 / 12 / ... (Kongruent 2 modulo 5)
• Abgabeordner 3: Gruppe 3 / 8 / 13 / ... (Kongruent 3 modulo 5)
• Abgabeordner 4: Gruppe 4 / 9 / 14 / ... (Kongruent 4 modulo 5)
• Abgabeordner 5: Gruppe 5 / 10 / 15 / ... (Kongruent 0 modulo 5)

24.-28. Mai

Exkursionswoche - keine VL.

02. Juni

Link zum Evaluationsbogen im StudIP

07. Juli

Die Klausur wird am 03.08.2021 online stattfinden. Weitere Informationen zum Ablauf folgen später.

21. Juli

Das Übungsblatt 7 wird nicht bewertet. Zur Klausurvorbereitung ist empfohlen, die Aufgaben zu bearbeiten. Die Lösungen werden am 27. Juli hochgeladen.

28. Juli

Der genaue Klausurtermin ist der 03.08.2021 10:00 - 13:00. Die Klausur findet online als Hausarbeit statt. Die Klausur wird für den Klausurzeitraum im StudIP in einem separaten Ordner verfügbar sein. Außerdem wird es dort auch einen Abgabeordner für die Klausur geben. Alle Informationen zur Klausur finden Sie auf dem Klausurdeckblatt. Lesen Sie sich das Blatt sorgfältig durch! Sie müssen eine Eigenständigkeitserklärung ausfüllen, drucken, unterschreiben und dann eingescannt/fotografiert in den Abgabeordner hochladen, damit ihre Klausur gewertet werden kann. Sollten Sie nicht in der Lage sein zu drucken, können Sie in den Information zu Onlineprüfungen eine Alternative wählen. Bei technischen Problemen während der Klausur machen Sie bitte Beweisfotos und melden sich bitte umgehend unter +49 (0)531 391 9532.

27. August

Die Klausurergebnisse finden Sie im StudIP. Zur Klausureinsicht können Sie Termine bis zum 30.09. mit Andrea Soleinsky ausmachen.

Organisation

Vorlesung

• Der Dozenten der Vorlesung ist Prof. Dr. Roland Meyer und Sören van der Wall.
• Prüfer der Vorlesung ist Prof. Dr. Roland Meyer.
• Eintrag im Vorlesungsverzeichnis: Vorlesung.
• Vorlesungstermine: Die Vorlesungen werden im Videoformat mittwochabends hochgeladen.

Modul

Um das Modul erfolgreich abzuschließen, sind zwei Leistungen zu erbringen:

• Prüfungsleistung: Zu erbringen durch Bestehen einer schriftliche Abschlussklausur zu Beginn des vorlesungsfreien Zeitraums.
• Studienleistung: Zu erbringen durch das erfolgreiche Bearbeiten von mindestens 50% der Übungsaufgaben.

Vorlesungsmaterialien

• Woche 1: 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.

• Woche 2: Deduktive Systeme

  Folien, Beispielbeweis zur Vollständigkeit einer Operatorenmenge, Beweis des Deduktionstheorems (syntaktische Version).

• Woche 3: F0

  Beweise in F0, Beweis mittels Inkonsistenz, Vollständigkeit von F0.

• Woche 4: Sequenzen, Typsysteme und Tableaus

  Folien zum Sequenzenkalkül, Beispielbeweis im Sequenzenkalkül, Typsysteme, Beispiele zu Tableaus. Folien zu Tableaus.

• Woche 5: Normalformen, Davis-Putnam

  Folien zu Normalformen, Beispiel zu Tseitin mit Syntaxbaum, Beispiele zu Davis-Putnam, Folien zu Davis-Putnam.

• Woche 6: Resolution, BMC

  Beispiel zur Resolution, Folien zur Resolution, Widerlegungsvollständigkeit der Resolution, Bounded-Model-Checking.

• Woche 7: Syntax und Semantik der Prädikatenlogik

  Folien, Lassie und Nemo.

• Woche 8: Substitution und Normalformen

  Folien, Beispiel zur Substitution, Anwendung des Substitutionslemmas, Pränexnormalform, Beispiel zur Skolemisierung, Beweis des Satzes von Skolem.

• Woche 9: Herbrand-Theorie

  Folien, Beispiel zu Herbrand-Strukturen, Beweis des Satzes von Herbrand.

• Woche 10: 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.

• Woche 11: System F

  Folien.

Die Präsentation ist hier in Form von Videos zu finden. Ausführlichere Darstellungen des Inhalts finden Sie in den folgenden handschriftliche Notizen:

• Einführung in das Beweisen
• Syntax und Semantik der Aussagenlogik, Kompaktheitssatz
• Deduktionstheorem, Beweise
• Vollständigkeit, Sequenzen, Tableaus
• Beispiel zur Tseitin-Transformation
• Beispiele Davis-Putnam und Resolution, Widerlegungsvollständigkeit der Resolution
• Syntax und Semantik der Prädikatenlogik erster Stufe
• Substitution und Normalformen
• Herbrand-Theorie
• Allgemeingültigkeit
• Kompaktheitssatz der Prädikatenlogik
• Theorien
• Tableaus und Unifikation
• Prädikatenlogische Resolution
• Zusätzliche Notizen zu Nichtstandardmodellen.

• ausführliche Folien (mit allen Zwischenschritten) von 2019
• kompakte Folien (ohne Zwischenschritte) von 2019
• Folien von 2018
• Skript von 2017
• sehr lückenhaftes Skript von 2019

Übungsbetrieb

• Große Übungen werden in Form von Videos hochgeladen.
• Die kleinen Übungen werden von Tutoren gehalten. Die Tutoren werden abwechselnd ein Tutorium aufnehmen und auf dieser Seite zugänglich machen.
• Tragen Sie sich bitte bis zum 23.04 zur Abgabe des ersten Blattes zu viert im StudIP als Abgabegruppe ein.

• Woche 1: Einführung in das Beweisen
• Woche 2/3: Deduktives Beweisen in F0 und Anwenden des Kompaktheitssatzes
• Woche 4/5: Satisfiability Checking - Algorithmen
• Woche 6/7: Prädikatenlogik - Syntax, Semantik und Bedeutsamkeit
• Woche 8/9/10: Herbrand-Theorie: Elimination der Gleichheit - Anwendung des Kompaktheitssatzes für Prädikatenlogik

Übungsblätter

• Abgabeordner 1: Gruppe 1 / 6 / 11 / ... (Kongruent 1 modulo 5)
• Abgabeordner 2: Gruppe 2 / 7 / 12 / ... (Kongruent 2 modulo 5)
• Abgabeordner 3: Gruppe 3 / 8 / 13 / ... (Kongruent 3 modulo 5)
• Abgabeordner 4: Gruppe 4 / 9 / 14 / ... (Kongruent 4 modulo 5)
• Abgabeordner 5: Gruppe 5 / 10 / 15 / ... (Kongruent 0 modulo 5)

• Übungsblatt 1 - Bis Fr, 30.04.2021 23:59
• Übungsblatt 2 - Bis Fr, 1314.05.2021 23:59
• Übungsblatt 3 - Bis Fr, 04.06.2021 23:59
• Übungsblatt 4 - Bis Fr, 18.06.2021 23:59
• Übungsblatt 5 - Bis Fr, 02.07.2021 23:59
• Übungsblatt 6 - Bis Fr, 16.07.2021 23:59
• Übungsblatt 7 - Unbewertet

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.
• Kreuzer, Kühling: Logik für Informatiker, Pearson.
• Nissanke: Introductory Logic and Sets for Computer Scientists, Pearson.
• Yosuhara: Recursive Function Theory and Logic, Academic Press.