Hauptseite
Literatur
Übungen
Klausuren
Mailingliste
Software
Skript
Vorlesung im Sommersemester 2001.
Prof. Gert Smolka,
Christian Schulte.
Fachrichtung Informatik,
Universität des Saarlandes.
Montags und Donnerstags, 9-11 Uhr, Gebäude 45, Hörsaal 002
Beginn am Donnerstag, 5. April 2001
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.