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

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