Termine

Art	Termin				Ort		Veranstalter
V2	Di 8:15 – 9:45				AH II	Beginn 15. Oktober	E. Grädel

Skript

• Kapitel 1: Der Satz von Trakhtenbrot [ps]
• Kapitel 2: Präfixklassen der Logik erster Stufe [ps]
• Kapitel 3: Model-Checking-Spiele [pdf]

Inhalt

Viele Probleme aus Mathematik und Informatik lassen sich als Auswertungs- oder Erfüllbarkeitsprobleme in logischen Theorien formulieren. Dies gilt sowohl für klassische mathematische Fragestellungen wie auch für zahlreiche moderne Informatik-Anwendungen ganz unterschiedlicher Natur, beispielsweise

• die automatische Verifikation paralleler Prozesse (Model-Checking für modale und temporale Logiken)
• das Auswerten von Datenbank-Anfragen (Model-Checking für die Logik erster Stufe und Datalog)
• Konsistenz- und Subsumtionsprobleme in der Wissenrepräsentation (Erfüllbarkeit in geeigneten logischen Formalismen, z.B. Modallogiken oder Fragmenten der Logik erster Stufe)

In der Vorlesung werden wichtige Methoden und Techniken vorgestellt, um

• zu beurteilen, ob solche Problem überhaupt algorithmisch entscheidbar sind,
• ihre Komplexität zu bestimmen,
• möglichst effiziente Algorithmen dafür zu entwickeln.

Ein interessanter Ansatz um algorithmische Probleme in logischen Theorien zu lösen beruht auf Strategiekonstruktionen in endlichen und unendlichen Spielen. Ein Schwerpunkt der Vorlesung liegt daher auf der algorithmischen Spieltheorie und ihren Anwendungen in der Logik.

Voraussetzungen

• Mathematische Logik

Zuordnung

• Informatiker: Theoretische Informatik, Vertiefungsfach, Anwendungsfach Mathematik
• Mathematiker: Reine Mathematik, Angewandte Mathematik
• Lehramtskandidaten: Algebra und Grundlagen der Mathematik (B), Angewandte Mathematik (D)