Theoretical Computer Science

Logik 2016

Neuigkeiten

• Die Ergebnisse der Nachklausur stehen fest.
  • Die Ergebnisse können im STATS eingesehen werden.
  • Ab 40 Punkten bzw. Note 4.0 zählt die Klausur als bestanden.
  • Die Klausureinsicht findet am Donnerstag, dem 03. November, von 15:00 bis 16:00 Uhr in Raum 34-420 statt.
• Wir bieten am Dienstag, dem 11. Oktober, ab 14:00 in Raum 32-439 eine Fragestunde an.
• Alle Studierende, die über das Prüfungsamt für die Nachklausur angemeldet sind, sollten nun im STATS für die zweite Modulprüfung eintragen sein.
• Sie dürfen auch dann an der Nachklausur teilnehmen, wenn Sie die Zwischenklausur(en) nicht bestanden haben.
• Die Ergebnisse der Abschlussklausur stehen fest.
  • Die Ergebnisse können im STATS eingesehen werden.
  • Ab 37 Punkten bzw. Note 4.0 zählt die Klausur als bestanden.
  • Die Klausureinsicht findet am Donnerstag, dem 01. September, von 15:00 bis 16:00 Uhr in Raum 34-420 statt.
• Alle Studierende, die sowohl eine Klausurzulassung haben, als auch über das Prüfungsamt für die Abschlussklausur angemeldet sind, sollten nun im STATS für die Modulprüfung eintragen sein. Alle Studierende, die über das Prüfungsamt angemeldet waren, allerdings keine Zulassung haben, haben wir über die im STATS angegebene E-Mail-Adresse kontaktiert.
  Falls Sie dann im STATS nicht eingetragen sind, obwohl Sie teilnehmen möchten, kontaktieren Sie mich bitte umgehend.
• Wir weisen darauf hin, dass es im KAI-System viele Logik-Altklausuren online stehen. (Nur aus dem Uninetz bzw. per VPN erreichbar.)
• Wir bieten in Kooperation mit den Tutoren am Montag, dem 15. August ab 14:00 in Raum 48-208 eine freiwillige Zusatzveranstaltung an. Auf dieser wird
  • Übungsblatt 13 besprochen und gegebenenfalls zurückgegeben und
  • Ihre Fragen zum Vorlesungsstuff - insbesondere im Hinblick auf die Klausur - beantwortet.
• Wenn Sie an der 2. Zwischenklausur teilnehmen möchten, melden Sie sich bitte bis zum 08. August im STATS zur Klausur an.
• Zusätzliche Notizen zu Nichtstandardmodellen wurden hochgeladen und den Materialien hinzugefügt.

Vorlesung

• Die Vorlesung wird von Prof. Roland Meyer gehalten.
• Vorlesungstermin:
  • Mittwochs, 11:45 - 13:15 in 52-207

Übungen

• Die Organisation der Übungen erfolgt über STATS.
• Die Übungen werden von Sebastian Muskalla organisiert.
• Übungstermine:
  • Gruppe 1: Donnerstag, 8:15 - 9:45 in Raum 48-379 (Kathrin Thomas)
  • Gruppe 2: Donnerstag, 11:45 - 13:15 in Raum 34-420 (Kathrin Thomas)
  • Gruppe 3: Donnerstag, 13:45 - 15:15 in Raum 48-379 (Lea Plückebaum)
  • Gruppe 4: Freitag, 8:15 - 9:45 in Raum 44-465 (Jakob Wenzel)
  • Gruppe 5: Freitag, 13:45 - 15:15 in Raum 32-439 (Lea Plückebaum)
  • Gruppe 6: Freitag, 15:30 - 17:00 in Raum 13-370 (Jakob Wenzel)
• Es gibt wöchentlich abwechselnd ein Abgabe-Übungsblatt oder ein Präsenz-Übungsblatt. Zu ersteren geben Sie Lösungen ab und letztere bearbeiten Sie gemeinsam in der Übung.
• Die Übungsblätter werden mittwochabends hier veröffentlicht.
• Die Lösungen zu den Abgabe-Blättern sind bis 1,5 Wochen später freitags 12.00 Uhr abzugeben. Die entsprechenden Kästen finden sich im Treppenhaus von Gebäude 34, 4. Stock, nahe Raum 401 und der AG Softwaretechnik.
• Bitte geben Sie zu dritt ab.
• Bitte beachten Sie, dass die Übungen verpflichtend sind.

Übungsblätter

• Blatt 1 (Präsenz)
• Blatt 2 (Abgabe)
• Blatt 3 (Abgabe)
• Blatt 4 (Präsenz)
• Blatt 5 (Abgabe)
• Blatt 6 (Präsenz)
• Blatt 7 (Abgabe & Zusatzaufgaben)
• Blatt 8 (Präsenz)
• Blatt 9 (Abgabe)
• Blatt 10 (Präsenz)
• Blatt 11 (Abgabe)
• Blatt 12 (Präsenz)
• Blatt 13 (Abgabe)
• Blatt 14 (Präsenz)

Material

1. Iteratives Bounded-Model-Checking. (Woche 1)
2. Syntax und Semantik der Aussagenlogik, Kompaktheitssatz. (Woche 2, 3)
3. Deduktionstheorem, Beweise. (Woche 4)
4. Vollständigkeit, Sequenzen, Tableaus. (Woche 5)
5. Beispiele Davis-Putnam und Resolution, Widerlegungsvollständigkeit der Resolution. (Woche 6)
6. Syntax und Semantik der Prädikatenlogik erster Stufe. (Woche 7)
7. Substitution und Normalformen. (Woche 8)
8. Herbrand-Theorie. (Woche 9)
9. Allgemeingültigkeit. (Woche 10)
10. Kompaktheitssatz. (Woche 11)
11. Theorien. (Woche 12)
12. Tableaus und Unifikation. (Woche 13)
13. Prädikatenlogische Resolution. (Woche 14)
14. Zusätzliche Notizen zu Nichtstandardmodellen.

Prüfungsmodalitäten

• Die Zwischenklausur ist zu bestehen
• Es sind 60% der Übungsaufgaben mit einem Plus ("sinnvoll bearbeitet") zu lösen.
• Es ist eine Aufgabe an der Tafel vorzustellen.

1. Zwischenklausur

• Die (erste) Zwischenklausur findet am Montag, dem 13. Juni 2016, um 19:00 in Hörsaal 46-220 statt.
• Melden Sie sich bis zum Dienstag, dem 07. Juni im STATS für die Zwischenklausur an, um teilzunehmen.
• Die Zwischenklausur muss bestanden werden, um an der Abschlussklausur teilnehmen zu dürfen.
• Als Hilfsmittel zugelassen ist ein beidseitig von Hand beschriebenes DIN A4 Blatt sowie Sprachwörterbücher.
• Falls Sie die erste Zwischenklausur nicht mitschreiben oder nicht bestehen, kann auch der erste Termin der Abschlussklausur im August als Zwischenklausur geschrieben werden, dann allerdings über den kompletten Stoff der Vorlesung!

1. Abschlussklausur & 2. Zwischenklausur

• Die Abschlussklausur wird am Freitag, dem 19. August 2016, ab 16:30 in Raum 28-111 (Sporthalle) stattfinden.
• Die Anmeldung zur Abschlussklausur erfolgt über das Prüfungsamt. Um die Abschlussklausur als Modulprüfung mitschreiben zu dürfen, ist eine Klausurzulassung nötig. Wir werden voraussichtlich am 08. August alle Studierende, die sowohl eine Klausurzulassung haben, als auch über das Prüfungsamt für die Klausur angemeldet sind, im STATS für die Klausur eintragen. Falls Sie dann im STATS nicht eingetragen sind, obwohl Sie teilnehmen möchten, kontaktieren Sie mich bitte umgehend.
• Die Anmeldung zur 2. Zwischenklausur erfolgt über STATS. Wenn Sie an der 2. Zwischenklausur teilnehmen möchten, melden Sie sich bitte bis zum 08. August im STATS zur Klausur an.
• Als Hilfsmittel zugelassen ist ein beidseitig von Hand beschriebenes DIN A4 Blatt sowie Sprachwörterbücher.

2. Abschlussklausur / Nachklausur

• Die Nachklausur wird am Freitag, dem 14. Oktober 2016, ab 8:00 in der Mensa stattfinden.
• Die Anmeldung zur Nachklausur erfolgt über das Prüfungsamt. Um die Abschlussklausur mitschreiben zu dürfen, ist eine Klausurzulassung nötig, wobei Sie die Zwischenklausur(en) nicht bestanden haben müssen.
• Als Hilfsmittel zugelassen sind ein beidseitig von Hand beschriebenes DIN A4 Blatt sowie Sprachwörterbücher.

Software

• Logik-Tools.

Literatur

• Schöning: Logik für Informatiker.
• Kreuzer, Kühling: Logik für Informatiker.
• Enderton: A Mathematical Introduction to Logic.
• Nissanke: Introductory Logic and Sets for Computer Scientists.

Information in English

• An English translation of the slides is available. Thanks to Erik Steiner for the translation!
• Exercise sheets in English are available.
• You have to register for the final exam at the Prüfungsamt (examination office) at least 2 weeks before the date of the exam.
• You can find the syllabus of the "Theoretic Computer Science Amendment"-version of Logic in the Modulhandbuch, Module 89-5021. Note that Gentzen sequent calculus for propositional logic and the Tableaux method in predicate method are not included in the syllabus. (The Tableaux method for propositional logic is included!)

• The Davis-Putnam algorithm is described here (Slides 1 to 8) and here. Note that we use the rules pure, unit, subsumption reduce, and splitting. You have to use them in this order, as is defined in pseudo code on our Slide 120. The examples on Slides 117 and 118 of our lecture will be helpful. There is quite some material on the web, search for Davis-Putnam or DPLL algorithm.
• Resolution is explained here (Slides 1 to 6 on Page 1) and here. Please also check the examples on our Slides 125 to 127. Alternatively, you can google for resolution rule and propositional logic.
• The tableau method is described here and here (we decompose conjunctions). Also check the examples on our Slides 77, 87 to 90. Again, Google may provide more information.
• Our system F0 is precisely what is described in Gaifman's notes. Up to the third axiom, it coincides with system H2 that Anita Wasilewska discusses in Chapter 8 (starting from Page 10) and Chapter 9 of her book.
• The sequent calculus is introduced (in slightly different notation) under the name Gentzen Style Proof System in Anita Wasilewska's Chapter 11.
• A good overview of topics on predicate logics can be found here.
• An introduction to predicate logic together with a description of Herbrand theory, unification, and resolution can be found in this course on artificial intelligence. Concerning the syntax of predicate logic, you may prefer to use our notation on Slides 144 to 147 (syntax) and 155 to 158 (semantics).
• The tableaux method for predicate logic is explained in these notes.
• A proof of undecidability of validity via a reduction of PCP can be found here. You may compare the development with Slides 190 to 194.
• Quantifier elimination in QBF is described here (cf. Slides 171 and 172).
• Gödel's System F is explained in Enderton's book as well as Slides 199 to 212.
• First-order theories are introduced here, the relationship between axiomatizability and decidability is discussed here. More information is given on Slides 213 to 225.
• Lecture notes in English by Haim Gaifman can be found here.
• This course by Anita Wasilewska comes with slides as well as lecture notes in English.