Formale Grundlagen der Informatik III (FGI-3), Teil 1: Logik
(Wintersemester 2015/16)

Veranstalter: Frank Heitmann
Zeit und Ort: Montag, 14-16 in B-201 (erste Vorlesung am Montag, 12. Oktober)

Aktuelles:

Aktuell noch nichts.

Folien:

Errata:
- In Kapitel 2 (Aussagenlogik. Resolution) muss es beim Resolutionsalgorithmus auf Folie 26 von fgi3_v2.pdf nicht eine do-while Schleife sein, sondern eine repeat-until.
Foliensatz 1 (VL 12.10). Kapitel 1. Aussagenlogik. Syntax & Semantik
Foliensatz 2 (VL 19.10). Kapitel 2. Aussagenlogik. Resolution
Foliensatz 3 (VL 26.10). Kapitel 3. Aussagenlogik. Natürliche Deduktion
- Dieser Foliensatz wird bei der nächsten Vorlesung noch erweitert.
- PDF wie beim Vortrag
- Handout Version (1 Folie pro Seite)
- Handout Version (4 Folien pro Seite)
Einschub für die VL am 02.11. Prädikatenlogik. Synatx & Semantik
Foliensatz 3 (VL 09.11). Kapitel 3. Aussagenlogik. Natürliche Deduktion
- Vervollständigung des Foliensatzes vom 26.10
- PDF wie beim Vortrag
- Handout Version (1 Folie pro Seite)
- Handout Version (4 Folien pro Seite)
Foliensatz 4 (VL 16.11). Kapitel 3. Aussagenlogik. Natürliche Deduktion. Korrektheit und Vollständigkeit
- PDF wie beim Vortrag (auch Handout mit 1 Folie pro Seite)
- Handout Version (4 Folien pro Seite)
Einschub für die VL am 23.11. Prädikatenlogische Normalformen
Foliensatz 5 (VL 30.11). Kapitel 4. Prädikatenlogik. Resolution
Foliensatz 5 (VL 07.12). Kapitel 4. Prädikatenlogik. Resolution
Foliensatz 5 (VL 16.12). Kapitel 4. Prädikatenlogik. Resolution
- Fortsetzung der Vorlesung vom letzten Mal. Wir beweisen die fünf Sätze, die in dem obigen Foliensatz im Ausblick stehen. Siehe Kapitel 2.4 und 2.5 im Buch von Schöning.
Foliensatz 6 (VL 04.01). Kapitel 5. Verification by Model Checking
Foliensatz 7 (VL 11.01). Kapitel 6. Automatenbasiertes LTL Model Checking
Foliensatz 8 (VL 25.01). Kapitel 6. Automatenbasiertes LTL Model Checking (Teil 2)

Kommentare/Inhalte:

In der Vorlesung werden verschiedene Logiken behandelt. Dies sind insb. die Aussagenlogik, die Prädikatenlogik, die Modallogik sowie die Temporallogiken CTL und LTL. Im Zentrum stehen nach Einführung von Syntax und Semantik Ableitungsverfahren wie das Resolutionskalkül und die Tableau-Methode sowie weitere (Semi-)Entscheidungsverfahren, um bspw. das zentrale (Un-)Erfüllbarkeitsproblem zu lösen. Als wichtiger Anwendungsfall dient uns in der Vorlesung der Bereich der (Software-)Spezifikation und der (Software-)Verifikation.

Lernziel:

Vertiefte Kenntnisse grundlegender Modelle, Begriffe, Methoden und Ergebnisse der Logik mit Anwendungen in der Verifikation.

Vorgehen:

Vorlesung. Material für selbstständige Übungen wird zur Verfügung gestellt. Zum zeitnahen Verständnis des Stoffes wird die regelmässige Bearbeitung der Übungen empfohlen.

Literatur:

Den Stoff der Vorlesung findet man insbesonder in

Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Michael Ryan, Cambridge University Press, 2nd edition, 2004.
Mathematical Logic for Computer Science, Mordechai Ben-Ari, Springer, 3rd edition, 2012
evtl. First-order logic and automated theorem proving. Melvin Fitting, Melvin, Springer, 2nd edition 1996.

Für Grundlagen (Aussagenlogik, Prädikatenlogik) empfehle ich

Schöning, Uwe (2000). Logik für Informatiker. Spektrum, Akademischer Verlag

sowie

Hopcroft, John E., Motwani, Rajeev und Ullman, Jeffrey D. (2007) Introduction to Automata Theory, Languages, and Computation, 3ed, Pearson/Addison-Wesley (auch auf Deutsch erhältlich).

für NP-Vollständigkeit und SAT.

Imprint/Disclaimer

Last Change: 14:44 02/03/2016

Formale Grundlagen der Informatik III (FGI-3), Teil 1: Logik (Wintersemester 2015/16)