Sommersemester 2001

Logik

Prof. Tobias Nipkow


 Inhalt  Übung  Literatur

Bereich: III, Wahlpflichtvorlesung: 4 Std. (+2Ü)
Zeit und Ort: Mo, 11:15-12:45, 0360
Do, 11:15-12:45, 0360
Beginn: Mo, 23.04.2001
Zentralübung: Di, 14:15-15:45, 0360
Übungsleitung: Gerwin Klein

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

Voraussetzungen: Vordiplom

Empfehlenswert für:
jegliche Fragestellungen und Anwendungen von Logik-basierten Formalismen (ein Pleonasmus!), von der Softwarespezifikation bis zur Künstlichen Intelligenz.

Inhalt:
Die Vorlesung orientiert sich stark an:

Uwe Schöning: Logik für Informatiker. Spektrum Akademischer Verlag, 2000. (5. Auflage).

Der Inhalt im Überblick (wird im Laufe der Vorlesung ergänzt):

  1. Einführung: Geschichte, Einordnung, Ziele
  2. Aussagenlogik
    1. Syntax
    2. Semantik
    3. Normalformen (KNF & DNF)
    4. Hornformeln und effizienter Erfüllbarkeitstest
    5. Kompaktheitssatz ("Endlichkeitssatz")
    6. Resolution (Korrektheit und Vollständigkeit)
    7. Hilbert-Kalkül (H) (Ded.thm und Korrektheit) [Troelstra]
    8. Natürliches Schließen (N) [Troelstra]
      1. Transformation von H-Beweisen in N-Beweise
      2. Transformation von N-Beweisen in H-Beweise
      3. Simulation von Resolution durch N-Beweise
    9. Sequenzen-Kalkül [Troelstra]
      1. Korrektheit, Vollständigkeit, Gegenmodell-Generierung
      2. Signierter Tableau-Kalkül [Fitting]
  3. Prädikatenlogik erster Stufe
    1. Syntax und Semantik
    2. Unentscheidbarkeit (via PCP)
    3. Äquivalenzen und Normalformen, (Pränex-, Skolem-)
    4. Herbrand-Theorie (Herbrand-Struktur; Sätze von Löwenheim-Skolem, Gödel-Herbrand-Skolem, und Herbrand; Algorithmus von Gilmore)
    5. Resolution (Grundresolution, Unifikation, Prädikatenlogische Resolution, Korrektheit und Vollständigkeit)
    6. Verfeinerungen der Resolution (P-Resolution, N-Resolution, Lineare Resolution, Input-Resolution, Unit-Resolution, Paramodulation - keine Beweise über die Kalküle)
    7. Hilbert-Kalkül (Ded.thm und Korrektheit) [Troelstra]
    8. Natürliches Schließen (Äquivalenz von H und N) [Troelstra]
    9. Sequenzen-Kalkül [Troelstra]
      1. Korrektheit, Gegenmodell-Generierung, Vollständigkeit
      2. Signierter Tableau-Kalkül [Fitting]
  4. HOL: Prädikatenlogik höherer Stufe [Gordon]
    1. Typen und lambda-Terme
    2. Die Basis-Logik
    3. Definition von Aussagen- und Prädikatenlogik
    4. Typdefinitionen
    5. Definition der natürlichen Zahlen
Literatur:
  1. Uwe Schöning: Logik für Informatiker. Spektrum Akademischer Verlag, 2000. (5. Auflage).
  2. A.S. Troelstra und H. Schwichtenberg: Basic proof Theory. Cambridge University Press, 1996.
  3. Melvin Fitting: First-Order Logic and Automated Theorem Proving. Springer Verlag, 1996. (2nd edition).
  4. Mike Gordon: HOL - A Machine Oriented Formulation of Higher-order Logic. University of Cambridge, Computer Laboratory, Report 68, 1985.
 

Gerwin Klein Last modified: Mon Jul 23 08:02:30 MET DST 2001