Uni des Saarlandes
Informatik
Programmiersysteme
Vorlesungen
LSV SS-02


Hauptseite
Termine
Literatur
Übungen
Klausuren
Mailingliste
Software
Skript

Logik, Semantik und Verifikation

Vorlesung im Sommersemester 2002.

Prof. Gert Smolka, Tim Priesnitz.
Fachrichtung Informatik, Universität des Saarlandes.

Termine und Ort

Montags 9-11 Uhr und Mittwochs 11-13 Uhr, Gebäude 45, Hörsaal 002

Beginn am Mittwoch, 10. April 2001, 11 Uhr c.t.

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: nach Vereinbarung.
• Tim Priesnitz: nach Vereinbarung.