Logik, Semantik und Verifikation

Hauptseite
Literatur
Übungen
Klausuren
Mailingliste
Software
Material

Vorlesung im Sommersemester 2000.

Prof. Gert Smolka, Christian Schulte.
Fachrichtung Informatik, Universität des Saarlandes.

Termine und Ort

Montags und Donnerstags, 9-11 Uhr, Hörsaal 002

Beginn am Donnerstag 13. April 2000

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.
• Christian Schulte: nach Vereinbarung.