Theoretical Computer Science

Logik 2015

Neuigkeiten

• Die Korrektur der zweiten Abschlussklausur ist fertig!
  • Sie können die Ergebnisse im STATS einsehen.
  • Ergebnisse ab der Note 4.0 bzw. ab 40 Punkten zählen als bestanden.
  • Die Klausureinsicht findet am Mittwoch, dem 28.10 von 15:30 bis 16:00 in 34-420 statt.
• Der zweite Abschlussklausur / Nachklausur, findet am Freitag, dem 16.10.15 ab 8:15 in der Mensa statt.
• Die Korrektur der ersten Abschluss- bzw. zweiten Zwischenklausur ist fertig!
  • Sie können die Ergebnisse im STATS einsehen.
  • Ergebnisse ab der Note 4.0 bzw. ab 37 Punkten zählen als bestanden.
  • Die Teilnehmer, die nicht mitgeschrieben oder nicht bestanden haben, können (sofern sie die Klausurzulassung erhalten haben) am 16.10 an der Nachklausur teilnehmen. Melden Sie sich gegebenenfals rechtzeitig beim Prüfungsamt an!
  • Die Klausureinsicht findet am Montag, dem 07.09 von 13:30 - 14:30 in Raum 34-420 statt!
• Alle Studierende, die sowohl beim Prüfungsamt für die Klausur angemeldet waren, als auch eine Zulassung haben, sollten nun im STATS für die Klausur angemeldet sein. Falls Sie im STATS nicht als für die Klausur angemeldet angezeigt werden, aber angemeldet sein sollten, melden Sie sich bitte unverzüglich bei uns (muskalla@cs.uni-kl.de, Raum 34-426).
• Wir bieten in Kooperation mit den Tutoren am Donnerstag, dem 13.08 ab 14:00 in Raum 48-208 eine Fragestunde als freiwillige Zusatzveranstaltung an, auf der das (freiwillige) 7. Einreichblatt zurückgegeben und besprochen wird und wir ausserdem Ihre Fragen zum Vorlesungsstoff - insbesondere im Hinblick auf die Abschlussklausur - beantworten.
• Der Raum, in dem die Abschlussklausur stattfindet hat sich zu Raum 01-106 geändert.
• Das diese Woche veröffentlichte 7. Einreichblatt ist im folgenden Sinne freiwillig und gibt Bonuspunkte:
  • Der entsprechende Vorlesungsstoff ist klausurrelevant.
  • Die 9 Punkte, die Sie durch dieses Blatt erhalten können, werden nicht zur maximalen Punktzahl hinzugerechnet. Das heisst, Sie benötigen 60% der Punkte der ersten sechs Einreichblätter (25 = 0.6 * 42 Punkte) , um zur Klausur zugelassen zu werden.
  • Die Punkte, die Sie für die Bearbeitung dieses Blattes erhalten, werden trotzdem als Bonuspunkte auf ihr Punktekonto addiert. (Es ist also insgesamt möglich, bis zu 51 Punkte zu erhalten.)
  • Die Rückgabe des Blattes erfolgt ab dem 06.08 zu üblichen Bürozeiten in Raum 34-426 oder in der Fragestunde (siehe oben).
• Die Anmeldung zur zweiten Zwischenklausur ist jetzt im STATS möglich. Weitere Informationen zu Zwischen- und Abschlussklausur finden Sie weiter unten.
• Die Einführungsveranstaltung zum Logik-Seminar findet am Montag, dem 29.06 ab 17:15 in Raum 34-420 statt.
• Wenn Sie Interesse an der Teilnahme an einem Logik-Seminar zum Bauen eines SAT-Solvers in der vorlesungsfreien Zeit nach diesem Semester haben, melden Sie sich bis zum 23.06 bei Sebastian Muskalla (muskalla@cs.uni-kl.de, Raum 34-426) für die Einführungsveranstaltung an, auf der wir weitere Details zum Seminar bekanntgeben werden. Eine verbindliche Anmeldung zum Seminar findet erst im Anschluss an die Einführungsveranstaltung statt.
• Die Zwischenklausur ist fertig korrigiert!
  • Sie können die Ergebnisse im STATS einsehen.
  • Ergebnisse ab der Note 4.0 bzw. ab 40 Punkten zählen als bestanden.
  • Die Teilnehmer, die nicht mitgeschrieben oder nicht bestanden haben, können den ersten Termin der Abschlussklausur als zweiten Versuch für die Zwischenklausur verwenden . (Dann allerdings über den kompletten Stoff der Vorlesung.) Wenn sie diesen Versuch bestehen, können sie dann entsprechend den Nachtermin der Abschlussklausur als Erstversuch wahrnehmen.
  • Die Klausureinsicht findet am Freitag, dem 12.06 von 13:00 - 13:45 in Raum 34-420 statt!
• Am Donnerstag, dem 04. Juni finden aufgrund Fronleichnam keine Übungen statt. Desweiteren findet die Übung von Jonathan Kolberg am Freitag, dem 05. Juni um 11:45 - 13:15 nicht statt. Falls Sie hiervon betroffen sind, gehen Sie bitte in einen der folgenden Ersatztermine:
  • Freitag, 05. Juni, 11:45 - 13:15 Uhr in 11-260. Tutor: Albert Schimpf (Regulärer Termin)
  • Montag, 08. Juni, 08:15 - 09:45 Uhr in 11-260. Tutor: Jonathan Kolberg
  • Montag, 08. Juni, 13:45 - 15:15 Uhr in 34-420. Tutor: Martin Köhler
  • Montag, 08. Juni, 15:30 - 17:00 Uhr in 44-482. Tutor: Jakob Wenzel
• Der Tutor Jonathan Kolberg hat ein Dokument zu struktureller Induktion erstellt, in dem er diese Technik unter anderem anhand eines Beispiels erklärt: strukturelleinduktion.pdf (Update 09.06.2015: Einige Fehler im PDF wurden korrigiert.)
• Melden Sie sich bitte bis zum 02. Juni im STATS für die Zwischenklausur am 08. Juni an. Weitere Informationen zur Zwischenklausur finden Sie weiter unten.
• Für die Termine, die am 14. Mai wegen Christi Himmelfahrt ausfallen bieten wir Ersatztermine an. Die TeilnehmerInnen der Donnerstagsgruppen können sich aussuchen, welchen der Ersatztermine sie wahrnehmen:
  • Montag, 18. Mai, 08:15 - 9:45 Uhr in 11-260. Tutor: Martin Köhler.
  • Montag, 18. Mai, 13:45 - 15:15 Uhr in 48-379. Tutor: Jakob Wenzel.
  • Dienstag, 19. Mai, 11:45 - 13:15 Uhr in 11-205. Tutor: Jonathan Kolberg.
• Da sich die Gruppen-Anmeldungen auf wenige Termine konzentrierten, bieten wir neue Gruppen zu den beliebten Terminen an (unten in grün). Achtung: Gehen Sie bitte trotzdem zu dem Termin, für den Sie momentan im STATS angemeldet sind. Die Aufteilung auf die beiden parallelen Termine findet dann dort statt. Sollten Sie für eine Freitagsgruppe angemeldet sein, gehen Sie zu einem beliebigen Ersatztermin (am 4. oder 5. Mai) und gehen dann am 8. Mai in Ihre momentan gewählte Gruppe.
• Da am 1. Mai keine Lehrveranstaltungen stattfinden, wird es in der Woche darauf Ersatztermine für die Übungen geben. Die TeilnehmerInnen der Freitagsgruppen können sich aussuchen, welchen der Ersatztermine sie wahrnehmen:
  • Montag, 04. Mai, 08.15 - 9.45 Uhr in 11-260. Tutor: Martin Köhler.
  • Montag, 04. Mai, 13.45 - 15.15 Uhr in 48-379. Tutor: Jakob Wenzel.
  • Dienstag, 05. Mai, 13.45 - 15.15 Uhr in 57-165. Tutor: Albert Schimpf.
  • Dienstag, 05. Mai, 17.00 - 18.30 Uhr in 11-243. Tutor: Jonathan Kolberg.
• Die Logik Tools sind jetzt online. Die Seite ist nur per https erreichbar.

Vorlesung

• Vorlesung: Mi 11:45 - 13:15 in 52-207
• Achtung: Am 22.04.2015 findet die Vorlesung im Hörsaal 13-222 statt.
• Vorlesung im KIS und im Modulhandbuch.

Übungen

• Die Organisation der Übungen erfolgt über STATS. Ab Mittwoch, 22.04.2015, 15.00 Uhr können Sie sich im STATS zu den Übungsgruppen anmelden. Bitte legen Sie sich dafür im STATS einen Account an.
• Es werden die folgenden Übungstermine angeboten:
  • Donnerstags 8.15 - 9.45 Uhr in 48-379. Tutor: Jonathan Kolberg
  • Donnerstags 10.00 - 11.30 Uhr in 32-439. Tutor: Jakob Wenzel
  • Donnerstags 10.00 - 11.30 Uhr in 34-420. Tutor: Martin Köhler
  • Donnerstags 13.45 - 15.15 Uhr in 46-280. Tutor: Jakob Wenzel
  • Donnerstags 13.45 - 15.15 Uhr in 34-420. Tutor: Martin Köhler
  • Freitags 10.00 - 11.30 Uhr in 11-262. Tutor: Albert Schimpf
  • Freitags 11.45 - 13.15 Uhr in 11-260. Tutor: Albert Schimpf
  • Freitags 11.45 - 13.15 Uhr in 34-420. Tutor: Jonathan Kolberg.
• 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 in Gebäude 34, 4. Stock, nahe Raum 401 und der AG Softwaretechnik. verpflichtend sind.
• Bitte geben Sie zu zweit oder zu dritt ab.
• Bitte beachten Sie, dass die Übungen verpflichtend sind.

Übungsblätter:

• Blatt 1
• Präsenzblatt 1
• Blatt 2
• Präsenzblatt 2
• Blatt 3
• Präsenzblatt 3.
• Blatt 4
• Präsenzblatt 4
• Blatt 5 (Update 18.06 10:25: Fehler in Aufgabe 5.1 korrigiert)
• Präsenzblatt 5
• Blatt 6
• Präsenzblatt 6
• Blatt 7 (freiwillig, siehe oben)
• Präsenzblatt 7

Prüfungsmodalitäten:

1. Die Zwischenklausur ist zu bestehen
2. Es sind 60% der Übungsaufgaben mit einem Plus zu lösen (sinnvoll bearbeitet). Sie benötigen also mindestens 25 Punkte.
3. Es ist eine Aufgabe an der Tafel vorzustellen.

Abschlussklausur & 2. Zwischenklausur

• Die Abschlussklausur / zweite Zwischenklausur findet am Freitag, dem 21. August 2015 ab 16:30 in Raum 01-106 statt.
• Die Anmeldung zur Abschlussklausur erfolgt(e) über das Prüfungsamt. Die Anmeldung zur zweiten Zwischenklausur ist bis zum 9. August über das STATS möglich.
• Der Stoff der zweiten Zwischenklausur umfasst (genau wie der Stoff der Abschlussklausur) den kompletten Vorlesungszeitraum.
• Als Hilfsmittel zugelassen sind Sprachewörterbücher sowie ein beidseitig von Hand beschriebenes DIN A4 Blatt.

1. Zwischenklausur

• Die Ergebnisse der ersten Zwischenklausur sind im STATS einsehbar!
• Die Klausureinsicht findet am Freitag, dem 12.06 von 13:00 - 13:45 in Raum 34-420 statt!
• 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!
• Die (erste) Zwischenklausur findet am Montag, dem 08. Juni 2015 ab 17:15 in Hörsaal 46-110 statt.
• Die Zwischenklausur muss bestanden werden, um an der Abschlussklausur teilnehmen zu dürfen.
• Als Hilfsmittel zugelassen sind Sprachewörterbücher sowie ein beidseitig von Hand beschriebenes DIN A4 Blatt.

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)

Software

Literatur:

Information in English

If you want additional information or a different presentation of the contents of the lecture, you may find these links useful:

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