Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

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

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.

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.