Logik 2013
Angeboten wird die 2+2 Pflichtveranstaltung im Grundstudium Bachelor Informatik, Diplom Informatik, Diplom Technoinformatik, WI Richtung Informatik. Vorlesung und begleitende Übungen finden auf Deutsch statt. Weitere Informationen zu den Übungen finden sich unter Neuigkeiten.Neuigkeiten
- Die Klausurergebnisse sind im STATS verfügbar. die Einsichtnahme in die Nachschreibeklausur wird am 25. Oktober von 14.00 bis 14.30 Uhr in 34-420 stattfinden.
- Die Nachschreibeklausur findet am 11. Oktober von 8.00 Uhr bis 11.00 Uhr in der Mensa statt und wird unter den gleichen Bedingungen wie die (erste) Abschlussklausur geschrieben.
- The retry exam will be written on October 11 from 8am to 11am in the Mensa. The same conditions as for the first exam will apply.
- Am Montag, den 23. September, 11.00 bis 12.00 Uhr in Raum 34-420 besteht noch einmal die Möglichkeit einer Einsichtnahme in die Klausur.
- On monday, September 23, 11-12am in room 34-420, there will be another exam review.
- Die Klausureinsicht findet am Donnerstag, den 22. August von 16.00 bis 17.00 Uhr im Raum 34-420 statt.
- The exam review will take place on Thursday, August 22 between 4 and 5pm in room 34-420.
- Die Klausurergebnisse der Abschlussklausur und der zweiten Zwischenklausur sind nun auch im STATS verfügbar. The results of the exam and the second mid-term exam are now also available in the STATS system.
- Die Klausurergebnisse werden am Dienstag, den 20. August um 14.00 Uhr im Flur der Concurrency Theory AG ausgehängt.
- The list of exam results will be published on Tuesday, August 20 at 2pm in the Concurrency Theory Group.
- Im Flur der Concurrency Theory AG, zwischen Raum 34-426 und 34-428 hängt eine Liste mit Matrikelnummern der Studenten, die im QIS zur Klausur angemeldet sind und die Zulassung erworben haben. Ebenso enthalten ist eine Liste der Studenten, die genügend Punkte auf den Abgabeblättern haben, aber die (erste) Zwischenklausur nicht bestanden haben, die also die zweite Zwischenklausur mitschreiben können.
- Beachte: In Satz 6.10 muss Formel A als geschlossen vorausgesetzt werden.
- Bitte melden Sie sich im QIS (oder Prüfungsamt) und im STATS-System für die Abschlussklausur an. Wenn Sie am Freitag die Klausur als zweiten Versuch für die Zwischenklausur mitschreiben möchten, melden Sie sich bitte im STATS-System unter "Zwischenklausur (2. Versuch)" an.
- Please register in QIS (or the Prüfungsamt) and in the STATS system for the exam. If you would like to use the exam on Friday as a second chance to pass the mid-term exam, then please register in the STATS system under "Zwischenklausur (2. Versuch)".
- Übungsaufgaben (inkl. Lösungen) der Logik-Vorlesung von 2011 finden Sie hier.
- Problem sets (and solutions) of the Logics lecture in 2011 can be found here.
- Am 8. August um 11.30 Uhr wird in 48-208 von den Tutoren eine Fragestunde angeboten.
- On August 8 at 11.30am in 48-208, there will be a question and answer session held by the tutors.
- Zur Klausurvorbereitung wird am 05. August um 10 Uhr in 48-210 eine zusätzliche Veranstaltung stattfinden.
- On the 05th of August at 10am in 48-210, there will be a meeting that helps you prepare for the exam.
- Aufgabenblatt 7 ist freiwillig, zählt also nicht zu den erreichbaren Punkten. Sie können das Blatt aber nutzen, um die 60% Hürde zur Zulassung zu erreichen. Der Stoff ist natürlich klausurrelevant.
- Exercise Sheet 7 is optional in the sense that it does not count towards the overall reachable points. You may use the exercise sheet to reach the 60% required for admission to the exam. The material is of course relevant for the exam.
- The Turing award 2012 goes to Shafi Goldwasser and Silvio Micali. An overview of their contributions can be found in this article (accessible from within the university network).
- Shafi Goldwasser und Silvio Micali erhalten den Turing-Award 2012. Ein Überblick ihrer Beiträge findet sich in diesem Artikel (zugreifbar aus dem Universitätsnetz).
- The exam review will take place next Monday, the 10th of June 2013 from 15.30 to 16.30 Uhr in 34/420.
- Die Klausureinsicht findet am Montag, den 10.06.2013 von 15.30 Uhr bis 16.30 Uhr in 34/420 statt.
- The results of the mid-term exam are available in the STATS system. To see your result, you have to sign up for the exam in the system. You can do this by clicking on "Anmelden" next to "Zwischenklausur - Logik - SS13". You can then see your results by clicking on the link labeled "verfügbar".
- Die Ergebnisse der Zwischenklausur sind im STATS-System verfügbar. Um Ihr Ergebnis abzurufen, müssen Sie sich im System einmal für die Klausur anmelden.
- Since May 30th is a holiday, the English-speaking students will be contacted by their tutor about an alternative date.
- Da am 30. Mai ein Feiertag ist, weichen Sie bitte auf einen der folgenden Termine aus, falls Sie eine Übung am Donnerstag haben:
- Freitag 08.15 - 09.45 Uhr in 48-379. Tutor: Thomas Eickhoff.
- Freitag 10.00 - 11.30 Uhr in 11-262. Tutor: Martin Köhler.
- Freitag 13.45 - 15.15 Uhr in 11-243. Tutor: Thomas Eickhoff (Zusatztermin!).
- Für die Zwischenklausur dürfen Sie ein beidseitig handbeschriebenes DIN-A4-Blatt mit Notizen mitbringen.
- For the mid-term exam, you are allowed to bring one double-sided handwritten DIN-A4 sheet with notes.
- Unser Tutor Martin Köhler hat auf seiner Homepage Artikel zu Logik-Themen geschrieben. Zum Beispiel über strukturelle Induktion und das deduktive System F0. Vielen Dank an Herrn Köhler.
- The mid-term exam will take place on June 3rd 2013 from 5pm to 7pm in the Mensa.
- Die Zwischenklausur wird am 3. Juni 2013 von 17 bis 19 Uhr in der Mensa stattfinden. Eine Woche vorher, am 27. Mai, wird 13.45 - 15.15 Uhr von Elisabeth Neumann und Martin Köhler in 46-280 eine Fragestunde angeboten.
- Die Zuordnung von Tutoren hat sich leicht geändert (siehe Liste).
- There will be an English-speaking group on Thursdays, 3.30pm-5pm in 34-420 (see below).
- Die Vorlesung findet mittwochs von 11.45 - 13.15 Uhr in 52-207 statt.
- Die Übungsorganisation wird von Georg Zetzsche übernommen. Als Termine für Übungsgruppen stehen zur Auswahl:
- Donnerstags 10.00 - 11.30 Uhr in 32-439. Tutor: Elisabeth Neumann.
- Donnerstags 13.45 - 15.15 Uhr in 46-280. Tutor: David Deininger.
- Donnerstags 15.30 - 17.00 Uhr in 11-241. Tutor: Martin Köhler.
- Donnerstags 15.30 - 17.00 Uhr in 34-420. Tutor: Thomas Eickhoff (in English).
- Donnerstags 17.15 - 18.45 Uhr in 48-462. Tutor: Elisabeth Neumann.
- Freitags 08.15 - 09.45 Uhr in 48-379. Tutor: Thomas Eickhoff.
- Freitags 10.00 - 11.30 Uhr in 11-262. Tutor: Martin Köhler.
- Freitags 11.45 - 13.15 Uhr in 11-260. Tutor: David Deininger.
- Die Anmeldung zu den Übungsgruppen wird über das STATS-System der AG Softwaretechnik erfolgen.
- Um zur Klausur zugelassen zu werden, (i) sind 60% der Übungsaufgaben mit einem Plus zu lösen, (ii) ist eine Aufgabe an der Tafel vorzustellen, (iii) muss die Zwischenklausur bestanden werden, (iv) ist an den Übungen teilzunehmen.
- Ein interaktives Tutorial zum Sequenzenkalkül findet sich unter dieser Adresse. Vielen Dank an Raphael Reitzig für den Hinweis.
Vorlesungsaufzeichnungen
Zu der Vorlesung gibt es ein Skript (24.04.2013) sowie Folien (05.08.2013, vollständig). Beachte: In Satz 6.10 muss Formel A als geschlossen vorausgesetzt werden. Ein älteres Skript sowie Folien finden sich hier (Skript) und hier (Folien). Leider sind die alten gedruckten Logik-Skripte bereits vergriffen. In Raum 34-424 liegen jedoch noch Skripte zu den Vorlesungen "Reduktionssysteme 1", "Grundlagen der Programmierung" und "Einführung in die Theoretische Informatik", die Sie sich gerne abholen können.Übungsaufgaben/Exercise Sheets
Die Übungszettel werden mittwochsabends ausgegeben und 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 SoftTech AG.Die Besprechung der Aufgaben findet in den am Donnerstag und Freitag folgenden Übungen statt. In den Wochen, in denen kein Aufgabenzettel abzugeben ist, werden Präsenzaufgaben in den Übungen gelöst.
Bitte beachten Sie, dass die Übungen verpflichtend sind.
Sollten Sie Fragen zu oder Probleme mit den Übungen haben, melden Sie sich bitte — kommen Sie einfach vorbei oder schreiben Sie uns eine Mail.
The exercise sheets will be published Wednesday evenings and are due 1,5 weeks later on Friday at 12.00pm (noon). The box for your solutions are in building 34, 4th floor, next to room 401 and the SoftTech AG.
The solutions are discussed on the following Thursday or Friday. In weeks without a turn-in exercise sheet, you will solve in-class exercise sheets.
Note that attendance at the tutorials is mandatory.
If you have problems or questions concerning the tutorials, please come to us or write us an email.
- Aufgabenblatt 1 / Exercise Sheet 1.
- Präsenzaufgabenblatt 1 / In-Class Sheet 1.
- Aufgabenblatt 2 / Exercise Sheet 2.
- Präsenzaufgabenblatt 2 / In-Class Sheet 2.
- Aufgabenblatt 3 / Exercise Sheet 3. Achtung, in der ersten Version des Blatts gab es einen Fehler in Aufgabe 3.1b. Please note: In the first version of this sheet, there was a mistake in Exercise 3.1b.
- Präsenzaufgabenblatt 3 / In-Class Sheet 3.
- Aufgabenblatt 4 / Exercise Sheet 4.
- Präsenzaufgabenblatt 4 / In-Class Sheet 4.
- Aufgabenblatt 5 / Exercise Sheet 5.
- Präsenzaufgabenblatt 5 / In-Class Sheet 5.
- Aufgabenblatt 6 / Exercise Sheet 6.
Hinweise:
- In Aufgabe 6.1 brauchen Sie keine Theorien.
- In Aufgabe 6.2a gab es einen Fehler. Statt "erfüllbar" meinten wir "unerfüllbar". Aufgabe 6.2a wird nun nicht gezählt.
- In Exercise 6.1, you do not need theories.
- In Exercise 6.2a, there is a mistake. Instead of "satisfiable", we meant "unsatisfiable". Exercise 6.2a will not be counted.
- Präsenzaufgabenblatt 6 / In-Class Sheet 6.
- Aufgabenblatt 7 / Exercise Sheet 7.
- Präsenzaufgabenblatt 7 / In-Class Sheet 7.
Literatur / Information in English
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 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.