Termine

Art	Termin				Ort		Veranstalter
V4	Mo 8:15 – 9:45				AH I	Beginn 19. April	E. Grädel
	Do 10:00 – 11:30				AH V	Beginn 19. April	E. Grädel
Ü2	Do 12:30 – 14:00				Seminarraum I7		E. Grädel

Übungen

• Übung 1 [ps]
• Übung 2 [ps]
• Übung 3 [ps]
• Übung 4 [ps]
• Übung 5 [ps]
• Übung 6 [ps]
• Übung 7 [ps]
• Übung 8 [ps]

Materialien

• Das klassische Entscheidungsproblem [ps]

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)