Logik

Prof. Tobias Nipkow

Bereich: III, Wahlpflichtvorlesung: 3 Std.

Zeit: Montag, 8.30-10.00 Uhr (S1128) und Dienstag, 10.15-11.00 Uhr (S0320)

Beginn: 5.5.1997

Übung: Montag, 13.30-15.45 Uhr, S1128 (3stündig); Beginn: 5.5.1997
Übungsleitung: Wolfgang Naraschewski und Dr. Birgit Schieder
Übungsschein: Einen Schein erhält, wer mindestens 40 Prozent der Punkte aus den Hausaufgaben und Programmieraufgaben erreicht und erfolgreich an der Semestralklausur teilnimmt.

Die Aufgabenblätter für die Zentralübung werden regelmäßig in der Vorlesung verteilt. Für alle Aufgaben werden Lösungsvorschläge bereitgestellt. Bei Bedarf werden in der Vorlesung auch Merkblätter ausgeteilt.

Inhalt: Ziel der Vorlesung ist es, eine Einführung in Mathematische Logik zu geben, die stark algorithmischer Natur ist. Zusätzlich zu der rein mathematischen Frage, ob eine gewisse Menge von Schlussregeln vollständig ist, d.h. ob man alle wahren Aussagen damit ableiten kann, wird auch immer die Implementierung einer dazugehörigen Beweisprozedur behandelt, die Beweise automatisch zu finden versucht. Als Programmiersprache dient hierbei Prolog.
Der Inhalt im Überblick:

1. Einführung: Geschichte, Einordnung, Ziele
2. Aussagenlogik
   1. Syntax
   2. Semantik
   3. Uniforme Notation
   4. Disjunktive Normalform
3. Tableaux Kalkül für Aussagenlogik
   1. Hintikkas Lemma
   2. Der Modellexistenzsatz
   3. Vollständigkeit des Tableaux Kalküls
   4. Semantische Konsequenz (|=) und der Kompaktheitssatz
4. Weitere aussagenlogische Beweissysteme
   1. Hilbert Kalkül
   2. Natürliches Schließen
   3. Sequenzenkalkül
5. Prädikatenlogik erster Stufe
   1. Syntax
   2. Substitutionen
   3. Semantik
   4. Herbrand-Strukturen
   5. Uniforme Notation für Quantoren
   6. Hintikkas Lemma
   7. Der Modellexistenzsatz
   8. Das Theorem von Löwenheim und Skolem
6. Beweiskalküle für Prädikatenlogik erster Stufe
   1. Tableaux Kalkül mit Korrektheit und Vollständigkeit
   2. Kompaktheitssatz, Nichtcharakterisierbarkeit von Endlichkeit
   3. Natürliches Schließen
   4. Sequenzenkalkül
7. Implementierung von Tableaux mit Unifikation
8. Weitergehende Eigenschaften der Prädikatenlogik

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 Software Spezifikation bis zur Künstlichen Intelligenz.

Übungsschein: nach Bestehen einer Semestralklausur

Skript: keines

Literatur: Die Vorlesung orientiert sich sehr stark an

Melvin Fitting: First-Order Logic and Automated Theorem Proving.
Springer Verlag, 1996. (2nd edition)

Hinweis: wer nicht nur die Theorie der Logik kennenlernen sondern auch deren praktische Anwendung erkunden möchte, dem sei das Praktikum Spezifikation und Verifikation empfohlen.

Sprechstunde: S2233, nach Vereinbarung.

Semestralklausur: Die Scheine können ab Montag, den 4. August 1997 bei Frau Metz abgeholt werden.