 |
| Wir freuen uns über zu diesen Seiten. |
|
| Letzte Änderung:
17.01.2013 |
|
|
|
18.113 Vorlesung: Logik und Semantik (LOS)
Sommersemester 2007 |
| Veranstalter |
| Carola Eschenbach,
Matthias Jantzen
|
| Zeit/Ort |
| Mo 14-16, Do 12:30-14 B-201 |
| Aktuelles |
| Diese Seite deckt nur den ersten Teil der Vorlesung ab. Informationen zum zweiten Teil
sind hier zu finden |
| 9.5.07 CE: Prüfungstermine in der ersten Woche der vorlesungsfreien Zeit können über das Prüfungsamt vereinbart werden.
Weitere Termine im September/Oktober werde ich später bekanntgeben. |
| 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)
- 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)
- 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:
- 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]
- Weitere Informationen:
LOS-Seiten zum Semantik-Teil
|
|
| 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 klappt
es aber.
Gesamter Foliensatz (.pdf 21.5.2007)
|
| Links |
|
|
|
