Theoretische Grundlagen der Informatik
Formale Grundlagen der Informatik III (FGI-3), Teil 1: Logik
(Wintersemester 2015/16)
Veranstalter:
Frank HeitmannZeit und Ort: Montag, 14-16 in B-201 (erste Vorlesung am Montag, 12. Oktober)
Aktuelles:
- Aktuell noch nichts.
Links
- Link zum zweiten Teil (Semantik von Programmen): http://www2.informatik.uni-hamburg.de/tgi/lehre/vl/WS1516/FGI3/
- Link zu den Seminaren: http://www2.informatik.uni-hamburg.de/tgi/lehre/vl/WS1516/FGI3-Seminar/
- Folien (siehe unten)
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
- 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.
- Schöning, Uwe (2000). Logik für Informatiker. Spektrum, Akademischer Verlag
- 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).
Letzte Änderung: 14:44 03.02.2016
