Automatisierte Logik und Programmierung
Zweisemestrige Vorlesung, Technische Universität Darmstadt, 1994/95


Übersicht

Die Vorlesung Automatisierte Logik und Programmierung richtet sich an Studenten des Hauptstudiums Informatik mit einem Interesse für den Einsatz formal-logischer Methoden in der Programmierung. Aufgrund der Vielzahl aufeinander aufbauender Themen erstreckt sich die Veranstaltung über zwei Semester.
Der erste Teil befasst sich mit der Formalisierung von Logik, Berechenbarkeit und Datentypen sowie den zugehörigen Kalkülen, während im zweiten Teil die Implementierung von Beweissystemen, die Automatisierung logischer Schlüsse und die Synthese von Algorithmen aus formalen Spezifikationen im Vordergrund steht. Dabei wird ein besonderer Schwerpunkt auf die intutionistische Typentheorie und das interaktive Beweissystem NuPRL gelegt.
Thematisch ist die Veranstaltung sowohl in der Theoretischen als auch in der Angewandten Informatik angesiedelt, wobei der erste Teil die Theorie etwas stärker betont und der zweite Teil die Anwendung von Theorie bei der Entwicklung zuverlässiger Software.


Vorlesungsfolien

Vollständiges Skriptum (350 Seiten)


Kapitel 1: Einführung
PS PS (2:1) PDF
Kapitel 2: Formalisierung von Logik, Berechenbarkeit und Typdisziplin
PS PS (2:1) PDF
Kapitel 3: Die Intuitionistische Typentheorie
PS PS (2:1) PDF
Kapitel 4: Automatisierung des formalen Schliessens
PS PS (2:1) PDF
Kapitel 5: Automatisierte Softwareentwicklung
PS PS (2:1) PDF
Anhang A: Typentheorie: Syntax, Semantik, Inferenzregeln
PS PS (2:1) PDF
Anhang B: Konservative Erweiterungen der Typentheorie und ihre Gesetze
PS PS (2:1) PDF
Literaturverzeichnis
PS PS (2:1) PDF

BACK
Back to overview of courses