Logik

Peter Rossmanith

Bereich: III, Wahlpflichtvorlesung: 4 Std.

Zeit: Montag 11-13 Uhr Hörsaal 0360, Freitag 10-12 Uhr Hörsaal 1100

Beginn: Montag, 15. April

Übungsseite

Folien: 15. April, 19. April, 22. April, 26. April, 29. April, 3. Mai, 6. Mai, 10. Mai, 13. Mai, 17. Mai Alle zusammen

Inhalt:

Logik spielt in vielen Bereichen der Informatik eine zentrale Rolle; bei der Spezifikation und Verifikation von Programmen, in der künstlichen Intelligenz, sie ist Grundlage deskriptiver Programmiersprachen wie Prolog. Inhalt der Vorlesung ist die Einführung in die mathematische Logik, wobei das möglichst effiziente Finden von Beweisen einem Schwerpunkt bildet. Für die Aussagenlogik und die Prädikatenlogik erster Stufe werden verschiedene Kalküle vorgestellt und deren Korrektheit und Vollständigkeit, d.h. die Ableitbarkeit aller wahren Aussagen, gezeigt. Die Algorithmen zum Finden von Beweisen beruhen im wesentlichen auf Refutation, Resolutions- und Unifikationstechniken.

Der Inhalt im Überblick:

  1. Einführung: Geschichte, Einordnung, Ziele
  2. Aussagenlogik
    1. Syntax
    2. Semantik
    3. Normalformen
    4. Endlichkeitssatz
  3. Beweiskalküle für Aussagenlogik
    1. Davis-Putnam
    2. Resolution
    3. Hilbert-Kalküle
  4. Prädikatenlogik erster Stufe
    1. Syntax
    2. Semantik
    3. Normalformen
    4. Unentscheidbarkeit
    5. Herbrand-Theorie
  5. Beweiskalküle für Prädikatenlogik erster Stufe
    1. Resolution
    2. Tableaux Kalkül
    3. Hilbert-Kalküle
  6. Implementierung von Tableaux und Resolution mit Unifikation
  7. Varianten und Teillogiken
    1. Hornformeln
    2. Prädikatenlogik mit Gleichheit

Literatur: Die Vorlesung orientiert sich stark an

[Sch] Uwe Schöning: Logik für Informatiker. Reihe Informatik, Band 56, Wissenschaftsverlag, 1992. (4. Auflage).

mit Ergänzungen aus

[Fit] Melvin Fitting: First-Order Logic and Automated Theorem Proving. Springer Verlag, 1996. (2nd edition)
[Kle] Hans Kleine Büning, Theodor Lettmann. Aussagenlogik: Deduktion und Algorithmen. Teubner, 1994.

Weitere Literaturhinweise

Hörerkreis: Studenten/-innen der Informatik und Mathematik

Voraussetzungen: Vordiplom

Empfehlenswert für: jegliche Fragestellungen und Anwendungen von Logik-basierten Formalismen.

Übungsschein: nach Bestehen einer Semestralklausur

Sprechstunde: Zimmer 2209, nach Vereinbarung, und nach den Vorlesungsstunden.

Peter Rossmanith