 |
| Wir freuen uns über zu diesen Seiten. |
|
| Letzte Änderung:
17.01.2013 |
|
|
|
18.113 Vorlesung: Logik und Semantik (LOS)
Sommersemester 2006 |
| Veranstalter |
| Carola Eschenbach |
| Rüdiger Valk |
| Zeit/Ort |
| Mo 14-16, Do 14-16 B-201 |
| Aktuelles |
| Ein Projekt, das Themen des Logik-Teils dieser Vorlesung wieder aufgreift und in der praktischen Umsetzung vertieft, finden Sie hier |
| Die gedruckten Prüfungsunterlagen sind leider vergriffen. Nutzen Sie die (aktuelleren)
elektronischen Unterlagen. |
| Diese Seite deckt nur den ersten Teil der Vorlesung ab. Informationen zu zweiten Teil sind
hier zu finden |
| KVV-Eintrag |
| 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 |
| Zur Logik:
- Fitting, Melvin (1996; 2nd). First-Order Logic and Automated Theorem Proving. New
York: Springer.
- Ben-Ari, Mordechai (2001). Mathematical Logic for Computer Science. London:
Springer.
- Nerode, Anil & Richard A. Shore (1997). Logic for Application. New York:
Springer
|
Zur Semantik:
-
LOS-Seiten zum Semantik-Teil
- 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) [T REY]
- Als weitere Quellen: J.C. Mitchell: Foundations for Programming Languages (The MIT
Press, 1996) [T MIT]
- D. Gries: The Science of Programming (Springer, 1981) [ TGRI]
- A.R. Hoare: Unifying Theories of Programming (Prentice Hall, 1998) [T HOA]
- B. Meyer: Introduction to the Theory of Programming Languages (Prentice Hall,
1990) [T MEY]
|
|
| 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 (.pdf
22.5.2006)
|
| Links |
|
|
|
