Theoretical Computer Science

Logik 2014

News

Neuigkeiten

• Am Mittwoch, dem 12.11.2014, um 12:00 Uhr bieten wir eine weitere Einsichtnahme in die Nachklausur an. Im Gegensatz zur ersten Einsichtnahme findet diese allerdings in 34-423 statt.
• Die Einsichtnahme zur Nachschreibeklausur findet am 22.10.2014 um 14.00 Uhr im Raum 34-420 statt.
• Die Ergebnisse der Nachschreibeklausur sind im STATS veröffentlicht.
• Die Nachschreibeklausur wird am 17.10.2014 von 8.00 bis 11.00 Uhr in der Mensa geschrieben. Als Hilfsmittel in der Klausur ist, wie in der Zwischenklausur, ein beidseitig handbeschriebenes DIN A4-Blatt erlaubt. Melden Sie sich bitte im STATS zu der Klausur an.
Das Aufgabenblatt 7 wird zum Zusatztermin der Logik-Übung zurückgegeben und besprochen. Dieser findet am 31.7.2014 von 15:00 bis 16:30 Uhr in 52-207 statt.
• Am 20.8.2014 von 15:00 bis 17:00 Uhr wird es in 52-207 eine Fragestunde geben. Hier können Sie den TutorInnen Ihre Fragen zu den Inhalten der Logik-Vorlesung stellen.
• Es gibt einen Davis-Putnam-Solver zur eigenen Weiterentwicklung zum Download.

Vorlesung

• Vorlesung: Mi 11:45 - 13:15 in 52-207
• Vorlesung im KIS und im Modulhandbuch.

Übungen

• Die Organisation der Übungen erfolgt über STATS. Ab Mittwoch, 23.4.2014, 14.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: Martin Köhler.
  • Donnerstags 10.00 - 11.30 Uhr in 32-439. Tutor: Jonathan Kolberg.
  • Donnerstags 13.45 - 15.15 Uhr in 46-280. Tutorin: Elisabeth Neumann.
  • Donnerstags 17.15 - 18.45 Uhr in 48-379. Tutorin: Elisabeth Neumann.
  • Freitags 8.15 - 9.45 Uhr in 48-379. Tutor: Albert Schimpf.
  • Freitags 10.00 - 11.30 Uhr in 11-262. Tutor: Jonathan Kolberg.
  • Freitags 11.45 - 13.15 Uhr in 11-260. Tutor: Albert Schimpf.
  • Freitags 13.45 - 15.15 Uhr in 32-439. Tutor: Martin Köhler.
  (Die Angaben im KIS sind nicht aktuell.)
• 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 mittwochsabends 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.
• Bitte geben Sie zu zweit oder zu dritt ab.
• Bitte beachten Sie, dass die Übungen verpflichtend sind.
• Bei Fragen zu oder Problemen mit den Übungen wenden Sie sich bitte an Georg Zetzsche. — Kommen Sie einfach vorbei oder schreiben Sie eine Mail.

Übungsblätter:

• Blatt 1.
• Präsenzblatt 1.
• Blatt 2. Achtung, in Aufgabe 2.4d müssen Konstanten (⊥ und T) als atomare Formeln zugelassen werden.
• Präsenzblatt 2.
• Blatt 3.
• Präsenzblatt 3.
• Blatt 4.
• Präsenzblatt 4.
• Blatt 5.
• Präsenzblatt 5.
• Blatt 6.
• Präsenzblatt 6.
• Blatt 7.
• Präsenzblatt 7.

Prüfungsmodalitäten:

• Zwischenklausur: 10. Juni 2014, 17.00 - 20.00 Uhr in 46-220.
• Abschlussklausur: 22. August 2014, 16:30 - 18:30 in 28-111 (Sporthalle)
• Zweite Abschlussklausur: 17. Oktober 2014, 8:00 - 11:00 in der Mensa

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

Vorlesungsaufzeichnungen

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

Information in English

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

Schöning: Logik für Informatiker.

Nissanke: Introductory Logic and Sets for Computer Scientists.

Kreuzer, Kühling: Logik für Informatiker.

Enderton: A Mathematical Introduction to Logic.

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.