Modulcode:	infLICS2-01a
Englische Bezeichnung:	Logic in Computer Science - Advanced
Modulverantwortliche(r):	Prof. Dr. Thomas Wilke
Turnus:	unregelmäßig (SS18 WS19/20)
Präsenzzeiten:	4V 2Ü
ECTS:	8
Workload:	60 h lectures, 30 h exercises, 150 h self studies
Dauer:	ein Semester
Modulkategorien:	BSc-Inf-WP (BSc Inf (21)) MSc-Inf-Theo (MSc Inf (21)) MSc-Inf-WP (MSc Inf (21)) 2F-MEd-Inf-WP (MEd-Hdl Inf (21)) 2F-MA-Inf-WP (2F-MA Inf (21)) MSc-WInf-WP-Inf (MSc WInf (21)) TI (MSc Inf (15)) WI (MSc Inf (15))
Lehrsprache:	Englisch
Voraussetzungen:	Inf-Math-B infBL-01a

Kurzfassung:

There are various ways in which computer science and mathematical logic are intertwined. Some of the more advanced are explored in this course, which addresses mathematically/logically inclined CS students.

Lernziele:

Students

• explain deep results connecting CS and mathematical logic and from mathematical logic relevant to CS,
• explain the theories behind these results and how they relate to questions in CS,
• solve problems in mathematical logic and CS by applying methods from mathematical logic and computer science going along with these theories.

Lehrinhalte:

1. Natural Deduction in Propositional and Predicate Logic [1]
2. Program Verification (Hoare Logic) [1]
3. Complexity of Arithmetic (Post's Theorem) [2]
4. Decidability of Presburger and Skolem Arithmetic [3] [4]
5. Decidability of the Reals (Tarski's Theorem) [5]
6. Modal Logic and Logic of Knowledge [1]
7. LTL and LTL Model Checking [1]

Optional

1. Modal Fixed-Point Logic & MSOL
2. LTL Model Checking on Infinite Structures

Weitere Voraussetzungen:

Required are the competencies aquired in the above-mentioned modules.

Prüfungsleistung:

When there are only a few students: portfolio, including problems worked on, summaries of scientific papers, documentation of a presentation. Other material can be added.

Otherwise: oral exam, based on written pre-exam (small assignment), approx. 60 min. overall.

Lehr- und Lernmethoden:

Presentations by lecturer, problem-solving sessions, reading sessions, discussions in class, self- and group-study components: reading, writing, problem solving.

Verwendbarkeit:

Only one of the following modules can be credited to the same degree programme: infFLog-01a: Fortgeschrittene Logik in der Informatik, infLICS2-01a: Logic in Computer Science - Advanced oder infAutLog-01a: Automata and Logics.

Literatur:

1. Michael Huth, Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, Cambridge, 2004.
2. Piergiorgio Odifreddi, Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers, Elsevier, Amsterdam, 1992.
3. Achim Blumensath and Erich Grädel, Automatic structures, Proc. 15th Ann. IEEE Symposium on Logic in Computer Science, Santa Barbara, CA, 2000, pp. 51-62.
4. Achim Blumensath, Automatic Structures, Diploma Thesis, RWTH Aachen, 1999.
5. Jacek Bochnak, Michel Coste, Marie-Francoise Roy, Real Algebraic Geometry, Springer, New York, 1998.

Verweise:

Kommentar: