DIESE SEITE BETRIFFT NUR DEN SEMANTIK-ANTEIL DER VORLESUNG!

4st. Mo 14 - 16, Do 14 - 16 in B-201

Lernziel:
	Kennenlernen grundlegender theoretischer Modelle, Begriffe, Methoden und Ergebnisse der Logik und Semantik, sowie der Beziehungen zwischen diesen. Einführung in die theoretischen Grundlagen und den praktischen Einsatz der verschiedenen Arten von Semantiken (operationale, denotationale und axiomatische) wie auch der Typtheorie in Hinblick auf Anwendungen in modernen Programmierkonzepten, formalen Beweisen sowie der Daten- und Wissensmodellierung. Aneignung von wichtigen Techniken für die Analyse und das Verständnis der Spezifikation von Informatiksystemen.
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
Stell. im Studienplan:
	Hauptstudium, Vertiefungsgebiete P1, P10, P2, P3, P4, P5, P6, P7, P8, P9, Th1, Th2, Th3, Th4, T2; Schwerpunkte BV, OSE, RNT, SEM, SV, VIS, WV
Voraussetzungen:
	Vordiplom (bestandener F- und P-Zyklus unabdingbar)
Vorgehen:
	Vorlesung mit integrierten Übungen. Zur Vorlesung wird die Vor- und Nachbereitung an Hand der angegebenen Literatur erwartet. Die beiden Abschnitte der Vorlesung umfassen jeweils 13 Sitzungen (Teil I: Ch. Habel / Teil II: R. Valk). Einleitung und Abschlusssitzung werden von beiden Veranstaltern gemeinsam durchgeführt.
Literatur:
	Zur Logik: Fitting, Melvin (1996; 2nd). First-order logic and automated theorem proving. New York: Springer-Verlag. 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) [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) [T GRI], 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]
Periodizität:
	jährlich zum SS
Eignung:
	Geeignet für Lehramtsstudierende, Nebenfachstudierende. Nicht geeignet für Bioinformatikstudierende, Wirtschaftsinformatikstudierende.
Stichwörter:
	Kalkül, Sortenlogik, Typenlogik, denotationale, axiomatische und operationale Semantik, Domains, Fixpunktsatz, Typ-Theorie, Modell, Spezifikation, Resolution, Syntax, Deduktion, Modallogik, Zeitlogik
Materialien:
	Skript (Kapitel 1 - 3) Skript (Kapitel 5-7) Folien (Kapitel 1, Teil 1) Folien (Kapitel 1, Teil 2) Folien (Kapitel 1, Teil 3) Folien (Kapitel 2, Teil 1) Folien (Kapitel 2, Teil 2) Folien (Kapitel 2, Teil 3) Folien (Kapitel 3, Teil 1) Folien (Kapitel 3, Teil 2) Folien (Kapitel 5, Teil 1) Folien (Kapitel 5, Teil 2) Folien (Kapitel 6, Teil 1) Folien (Kapitel 6, Teil 2) Folien (Kapitel 7) Auswerten von Lambda-Ausdrücken aus Kapitel 5

Benutzernamen und Passwort finden sich auf der Titelrückseite des verteilten Skriptes oder sind über valk AT informatik PUNKT uni-hamburg PUNKT de zu erfahren.