Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

Logik 2015

For information in English, see below.

Neuigkeiten

Vorlesung

Übungen

Übungsblätter:

Prüfungsmodalitäten:

Es werden eine Zwischenklausur sowie eine Abschlussklausur geschrieben. Um zur Prüfung zugelassen zu werden sind die folgenden Voraussetzungen zu erfüllen:
  1. Die Zwischenklausur ist zu bestehen
  2. Es sind 60% der Übungsaufgaben mit einem Plus zu lösen (sinnvoll bearbeitet). Sie benötigen also mindestens 25 Punkte.
  3. Es ist eine Aufgabe an der Tafel vorzustellen.
Beachten Sie: Sollten Sie in einem vergangenen Semester nur einen Teil der obigen Bedingungen erfüllt haben, so müssen Sie in diesem Semester alle Bedingungen erneut erfüllen, um die Klausurzulassung zu erwerben.

Abschlussklausur & 2. Zwischenklausur

1. Zwischenklausur

Material

Zu der Vorlesung gibt es Folien (Stand 21.04.2015). Ein älteres Skript sowie ältere Folien sind ebenfalls verfügbar. Ferner wird es Notizen zu einzelnen Themen der Vorlesung geben.
  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

Es gibt eine Implementierung des Davis-Putnam-Verfahrens in Java. Der Algorithmus lässt sich mit Heuristiken weiterentwickeln. Vielen Dank an Albert Schimpf! Ein umfassendes Logikpackage ist derzeit in der Entwicklung. Vielen Dank an Sebastian Henningsen und Manuel Hoffmann!

Literatur:

  • Schöning: Logik für Informatiker.
  • Kreuzer, Kühling: Logik für Informatiker.
  • Enderton: A Mathematical Introduction to Logic.
  • Nissanke: Introductory Logic and Sets for Computer Scientists.
  • Information in English

    An English translation of the slides is available. Thanks to Erik Steiner for the translation!

    If you want additional information or a different presentation of the contents of the lecture, you may find these links useful: