Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

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

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.

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.