Universität des Saarlandes
FR Informatik
Programmiersysteme
Vorlesungen
Comp. Logik SS 03


Hauptseite
Termine
Literatur
Übungen
Prüfungen
Mailingliste
Software
Material

Einführung in die Computationale Logik

Einführung in die Computionale Logik
(Logik, Semantik und Verifikation)

Grundvorlesung im Diplomstudiengang Informatik
Stammvorlesung in den Bachelor/Master-Studiengängen

Prof. Gert Smolka, Marco Kuhlmann
Fachrichtung Informatik, Universität des Saarlandes

Termine

Dienstag, 9.15–11.00 Uhr, Gebäude 45, HS 002
Donnerstag, 11.15–13.00 Uhr, Gebäude 45, HS 002

Erste Vorlesung am Donnerstag, den 24.4.2003
Letzte Vorlesung am Donnerstag, den 24.7.2003

Keine Vorlesungen am 1.5. (Maifeiertag), 29.5. (Christi Himmelfahrt) und 19.6. (Frohnleichnam)

Inhalt

Logische Methoden spielen in der Informatik eine wichtige Rolle. Anwendungsbereiche sind die Künstliche Intelligenz, Programmiersprachen sowie die Spezifikation und Verifikation von Hardware und Software.

Die Vorlesung behandelt Aussagenlogik, Hoare-Logik und Prädikatenlogik erster Stufe. Dabei werden grundlegende Konzepte wie Rekursion (Fixpunktoperatoren), Induktion, logische Sprachen, Syntax (abstrakte), Semantik (denotationale und operationale), Berechenbarkeit, Verifikation, Reduktionssysteme, Beweissysteme (Resolution) und Expressivität behandelt.

Methodisch gehört die Vorlesung zur Theoretischen Informatik, arbeitet also mit mathematischen Definitionen und Beweisen (insbesondere durch Induktion). Gelegentlich werden wir auch kleine Programme in SML schreiben, um das Verständnis von Definitionen zu vertiefen.

Sprechzeiten

Prof. Gert Smolka: Mittwoch, 14–15 Uhr
Marco Kuhlmann: Mittwoch, 14–15 Uhr