2st. Do 14 - 16 C-221
(Hauptstudiumsschwerpunktvorlesung im WiSe 2005/2006)
Berndt Farwer
Lernziel:
Kennenlernen verschiedener substruktureller Logiken und deren Anwendung auf informatikspezifische Fragestellungen; Formulierung präziser Semantiken für unterschiedliche Konzepte der Programmierung und Modellierung.
Inhalt:
Substrukturelle Logiken sind nichtklassische Logiken, die insbesondere im Zusammenhang mit Problemen der formalen Grundlagen der Mathematik, der mathematischen Linguistik, der Logik und der theoretischen Informatik entwickelt wurden. In den vergangenen Jahren sind auf diesem Gebiet viele spannende und für die Informatik bedeutsame Ergebnisse erzielt worden, die tiefe Einblicke in die formalen Strukturen von Informatiksystemen erlauben. Während in allen substrukturellen Logiken die Regeln (in einem Gentzenschen Sequenzenkalkül) für die logischen Konnektoren unverändert bestehen bleiben, unterscheiden sich diese Logiken durch den Satz vorhandener Strukturregeln, die zum Beispiel für die Kommutativität der Konjunktion oder für die Ableitbarkeit des Satzes vom ausgeschlossenen Dritten (tertium non datur) verantwortlich sind. Es werden verschiedene Logiken und Kalküle behandelt.
Zu den behandelten Themenbereichen gehören:
• Grundlagen der Beweistheorie
1. Hilbert-Systeme
2. Gentzen-Systeme
3. Paradigmen: Formeln als Typen, Formeln als Beweise und Formeln als Terme
• Propositionale und prädikatenlogische Kalküle
1. intuitionistische Logik
2. Relevanz-Logik
3. Lineare Logik
• Spieltheorie
• Kategorientheorie
• Anwendungen substruktureller Logiken
Es wird in der Vorlesung besonderer Wert auf aktuelle Ergebnisse gelegt, die einen direkten Zusammenhang zur Informatik haben (z.B. zu eager vs. lazy evaluation, garbage collection, Ressourcenkonzepte, Petrinetze).
Stellung im Studienplan:
Hauptstudium, Vertiefungsgebiete A1, P1, P10, P2, P3, P4, P5, P6, P8, Th1, Th2, Th3, Th4; Schwerpunkte SEM, SV, VIS, WV
Voraussetzungen:
Grundstudium
Vorgehen:
Vorlesung mit integrierten Übungen
Literatur:
Greg Restall, An Introduction to Substructural Locics, Routledge, 2000;
Weitere aktuelle Literatur wird in der Veranstaltung bekanntgegeben.
Periodizität:
letztmalig
Sprache:
Deutsch
Eignung:
Geeignet für Nebenfachstudierende. Bedingt geeignet für Lehramtsstudierende, Bioinformatikstudierende. Nicht geeignet für Wirtschaftsinformatikstudierende.
Stichwörter:
lineare Logik, Ressourcenkonzepte, Beweistheorie, Semantik funktionaler Programmiersprachen, Erweiterungen von Prolog, Logik, automatisches Beweisen
