Schedule

Type	Date				Location		Organizer
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

Coursework

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

Supplements

• Das klassische Entscheidungsproblem [ps]

Content

Many problems in mathematics or computer science can be viewed or reformulated as either model checking problems or satisfiability problems in suitable logical theories. This is true on the one hand for many unsolved problems in mathematics (including, say, the Riemann hypothesis), on the other hand also for numerous modern applications in various areas of computer science, including

• automatic verification of parallel processes (model checking for modal and temporal logics)
• the evaluation of database queries (model checking for first-order logic and Datalog)
• consistency and subsumption problems in knowledge representation (satisfiability tests for suitable logical formalisms, such as modal logics, description logics, or fragments of first-order logic)

In this course we will, on the basis of numerous examples, present methods and techniques that permit us

1. to understand whether such problems are algorithmically decidable,
2. to determine their complexity, and
3. to develop good algorithms for such problems.

An interesting approach to solve algorithmic problems in logical theories relies on strategy constructions in finite and infinite games. One of the subjects of this course will therefore be the algorithmic theory of games and their applications in logic.

Prerequisites

• Mathematische Logik

Classification

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