Theoretische Informatik II

Inhalt:

Ein zentrales Problem der Informatik ist sicherlich die "Korrektheit von Programmen": Wie kann man sicherstellen, dass ein Programm tatsächlich das verlangte (Ein-/Ausgabe-) Verhalten hat? Verschiedenste Ansätze sind hier verfolgt worden, beispielsweise ausführliches Testen, Software-Review, oder Verifikation. Idealerweise liefert ein formales Verifikationsverfahren einen mathematischen Beweis für die Korrektheit eines Programms. Die mathematischen Grundlagen der Verifikationsmethoden liefert die mathematische Logik. Auch durch die Entwicklung neuerer Anwendungen wie "Automatisches Beweisen" und "Logik-Programmierung" hat die mathematische Logik einen wichtigen Stellenwert in der Informatik erhalten.

In dieser Veranstaltung soll eine Einführung in die mathematische Logik und in einige der Teilgebiete der Logik gegeben werden, die für die Informatik von besonderer Bedeutung sind. Im Einzelnen sollen folgende Themen behandelt werden:

  1. Aussagenlogik: Grundbegriffe, Äquivalenz und Normalformen, Hornformeln, der Endlichkeitssatz und die Resolution.
  2. Prädikatenlogik: Grundbegriffe, Normalformen, Unentscheidbarkeit, Herbrand-Theorie, Resolution.
  3. Programm-Verifikation: Grundbegriffe, Vor- und Nachbedingungen, Inferenzregeln, Schleifeninvarianten.
  4. Logik-Programmierung: Erzeugen von Antworten, Hornklauselprogramme und ihre Semantik, Auswertungsstrategien, PROLOG.

Literatur:

Uwe Schoening:
Logik für Informatiker, 5. Auflage, Spektrum Akademischer Verlag, Heidelberg, Berlin, 2000, ISBN 3-8274-1005-3 (Euro 17.95)

Ergänzende Literatur:

H. Hamburger, D. Richards:
Logic and Language Models for Computer Science, Prentice Hall, Upper Saddle River, N.J., 2002, ISBN 0-13-065487-6 (Euro 87.57)

Angesprochener Hörerkreis:

Studenten und Studentinnen der Informatik im 4. Fachsemester.

Voraussetzungen:

Theoretische Informatik I und Diskrete Strukturen I

Leistungsnachweis:

Klausur am Ende des Semesters. Aktive Teilnahme an den Übungen sowie gründliche Beschäftigung mit den wöchentlichen Übungsaufgaben wird als Vorbereitung auf die Klausur dringend (!) empfohlen!