Navigation Forschung Lehre Personen Publikationen Kontakt   Logik und Semantik (LOS) Veranstalter Zeit/Ort Inhalt Literatur Links Wir freuen uns über Kommentare und Hinweise zu diesen Seiten. Letzte Änderung: 17.01.2013

18.113 Vorlesung: Logik und Semantik (LOS) Veranstalter Christopher Habel Rüdiger Valk Zeit/Ort Mo 14-16, Do 14-16 B-201 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) Christopher Habel 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. Springer: New York Carpenter, Bob (1997). Type-logical semantics. Cambridge, MA: MIT-Press 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) Links Die Seite der Vorlesung im Sommer 03 mit Links zu den Folien Übungsblätter Blatt 1 Blatt 2 Blatt 3 (korrigierte Fassung)