 |
| Wir freuen uns über zu diesen Seiten. |
|
| Letzte Änderung:
17.01.2013 |
|
|
|
| 18.113 Vorlesung: Logik und Semantik (LOS) |
| Veranstalter |
| Carola Eschenbach |
| Rüdiger Valk |
| Zeit/Ort |
| Mo 14-16, Do 14-16 B-201 |
| Aktuelles |
| Die Vorlesungsunterlagen werden auch gedruckt zur Verfügung gestellt. Diese Seite deckt
nur den ersten Teil der Vorlesung ab. Zweiter Teil
der Vorlesung
|
| Inhalt |
| Die Vorlesung LOS behandelt die für viele Bereiche der Informatik grundlegenden Konzepte
der Logik und Semantik. Beide Gebiete basieren auf einer gemeinsamen Konzeption
syntaktischer Strukturen, deren Bedeutungen durch Interpretation in passenden Modellen
mathematisch präzise erfasst werden. Als Modelle treten nicht nur mathematische Strukturen
wie Algebren oder Relationengebilde auf, sondern auch Funktionen oder Rechenabläufe einer
(abstrakten) Maschine. Neben den Prinzipien syntaktischer Spezifikationen werden Verfahren
zur Strukturierung, Transformation und Abbildung der syntaktischen Objekte behandelt. Die
Notwendigkeit, die Semantik von Programmier- und Repräsentationssprachen formal und exakt zu
beschreiben, ergibt sich u.a. aus der Forderung nach sicherer Software. Nur so kann geprüft
werden, ob Informatiksysteme das leisten, was in der Spezifikation gefordert wurde.
Teil I (Logik und Semantik) Carola Eschenbach
- Konsolidierung der im Grundstudium vermittelten Kenntnisse über Aussagen- und
Prädikatenlogik, Beweistheorie - Modelltheorie
- Vertiefung des Verständnisses an Hand von weiteren Kalkülen (Tableaukalkül)
- Modale Aussagen- und Prädikatenlogik, Zeitlogik auf der Basis von Modallogik,
Sortenlogik, Typenlogik, Logik höherer Stufen
- Lambda-Kalkül
|
Teil II (Semantik und Programmiersprachen) Rüdiger Valk
- Denotationale Semantik, Domains und stetige Funktionen, Fixpunktsatz
- Formale Spezifikation, Programmverifikation, axiomatische Semantik, Hoare-Tripel,
Beweis-Kalküle
- Illustration der denotationalen Semantik bei zusammengesetzten Datenstrukturen,
Fehlerbehandlung, Ein-/Ausgabe
- Operationale Semantik und Nichtdeterminismus, Semantik von nebenläufigen
Programmen
- Auswertestrategie funktionaler Sprachen: normal-order evaluation, eager
evaluation, lazy evaluation
- Fortführung der Typ-Theorie und der Typ-Kalküle
|
|
| Literatur |
| Es gibt sehr viele Lehrbücher zur Logik, allerdings keines, das exakt den in der
Vorlesung vorgestellten Stoff umfasst. Gute Begleitbücher sind:
- Ben-Ari, Mordechai (2001). Mathematical Logic for Computer Science. Springer:
London.
- Fitting, Melvin (1996; 2nd.). First-Order Logic and Automated Theorem Proving.
Springer: New York.
- Nerode, Anil & Richarf A. Shore (1997). Logic for Application. Springer:
New York.
|
Außerdem gibt es sehr gute Handbücher zur Logik.
Zur Semantik:
- zum Einstieg: Pepper: Grundlagen der Informatik, (Oldenburg, 1992) und Wätjen:
Theoretische Informatik, Kapitel 6 (Oldenburg, 1994).
- Im Wesentlichen: J.C. Reynolds: Theories of Programming Languages (Cambridge
University Press, 1998)
- Als weitere Quellen: J.C. Mitchell: Foundations for Programming Languages (The MIT
Press, 1996)
- D. Gries: The Science of Programming (Springer, 1981)
- A.R. Hoare: Unifying Theories of Programming (Prentice Hall, 1998)
- B. Meyer: Introduction to the Theory of Programming Languages (Prentice Hall, 1990)
|
|
| Folien |
| Die Foliensätze, die hier zu Beginn des Semesters zu finden sind, entsprechen zum Teil
dem Stand der Vorlesung des letzten Jahres. Im Laufe des Semesters, füge ich aktualisierte
Fassungen und auch Übungsunterlagen hier ein.
Wenn man die pdf-Dateien unter Unix mit einer alten Version von Acrobat ausdruckt,
kann es passieren, dass die
Symbole nicht korrekt gedruckt werden. Mit der Version 7, die nun auch fuer Unix verfügbar ist,
klappt es aber. Gesamter Foliensatz, der der gedruckten Fassung
zugrunde liegt. |
| Links |
|
|
|
