Logik 2012
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 Ergebnisse der zweiten Logik-Abschluss-Klausur hängen neben Raum 34/422 aus. Am Dienstag, den 6.11.2012 um 14.00 Uhr wird es eine Klausureinsicht in Raum 34/420 geben.
- The results of the second final exam are posted next to room 34/422. On Tuesday, November 6th, at 2pm, there will be a post-exam review in room 34/420.
- There are more references in English, please check the literature section below.
- Ein interaktives Tutorial zum Sequenzenkalkül findet sich unter dieser Adresse. Vielen Dank an Raphael Reitzig für den Hinweis.
- There are new pointers (below) to literature in English that can be found on the web.
- Die Übungsorganisation wird von Reiner Hüchting und Georg Zetzsche übernommen. Als Termine für Übungsgruppen stehen zur Auswahl:
- Donnerstags 10.00 - 11.30 Uhr in 32-439. Tutor: Reiner Hüchting.
- Donnerstags 11.45 - 13.15 Uhr in 48-379. Tutor: Reiner Hüchting.
- Donnerstags 13.45 - 15.15 Uhr in 46-280. Tutor: Reiner Hüchting.
- Donnerstags 15.30 - 17.00 Uhr in 11-241. Tutor: Georg Zetzsche.
- Freitags 10.00 - 11.30 Uhr in 11-262. Tutor: David Deininger.
- Freitags 11.45 - 13.15 Uhr in 11-260. Tutor: David Deininger.
- Die Vorlesung findet mittwochs von 11.45 - 13.15 Uhr in 52-207 statt.
- 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.
Vorlesungsaufzeichnungen
Zu der Vorlesung gibt es ein Skript (2002) sowie Folien (2011).Übungsaufgaben
Die Übungszettel werden mittwochsabends ausgegeben und sind zwei Wochen später am Dienstagmittag 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.
- Aufgabenblatt 1 (english).
- Präsenzaufgabenblatt 1 (english).
- Aufgabenblatt 2 (english).
- Präsenzaufgabenblatt 2 (english).
- Aufgabenblatt 3 (english).
- Präsenzaufgabenblatt 3 (english).
- Aufgabenblatt 4 (english).
- Präsenzaufgabenblatt 4 (english).
- Aufgabenblatt 5 (english).
- Präsenzaufgabenblatt 5 (english).
- Aufgabenblatt 6 (english).
- Präsenzaufgabenblatt 6 (english).
- Aufgabenblatt 7 (english). Hinweis: Blatt 7 ist freiwillig, d.h. es können Punkte damit erzielt werden, die aber nicht zu den 100% zählen, von denen 60% erreicht werden müssen. Note: Sheet 7 is not mandatory, i.e. you can gain points with it, but the reachable points do not count towards the 100% of which you need 60%.
- Präsenzaufgabenblatt 7 (english).
Inhalt
Aussagenlogik: Syntax und Semantik, Kalküle, deduktiver Aufbau der Aussagenlogik, natürliche Kalküle, algorithmischer Aufbau: Tableau-Methode, Davis-Putman-Algorithmen, Resolutionsverfahren.Prädikatenlogik: Syntax, Beziehungen zwischen Eigenschaften von Elementen, Semantik: Interpretationen, Belegungen, Bewertungen, Erfüllbarkeit, Transformationen von Termen und Formeln, Unentscheidbarkeit der Allgemeingültigkeit, deduktiver Aufbau der Prädikatenlogik, Hauptsätze von PL1, Theorien erster Stufe, Modelle, Aufzählungsverfahren für PL1, Tableau- und Resolutionsverfahren, Logisches Programmieren und Prolog.
Literatur
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.