Logik, Semantik und Verifikation

Hauptseite
Literatur
Übungen
Klausuren
Mailingliste
Software
Skript

Vorlesung im Sommersemester 2001.

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

Termine und Ort

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

Beginn am Donnerstag, 5. April 2001

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



Christian Schulte, Letzte Änderung: Sat Oct 28 17:12:37 2017.