Formale Systeme
Vorlesung im Wintersemester 2015/2016
Prof. Dr. Bernhard Beckert (BB)
Dr. Thorsten Bormer (TB),
Dr. Vladimir Klebanov (VK),
Dr. Mattias Ulbrich (MU)
| Zielgruppe: | Diplom Informatik, Bachelor Informatik, Master Informatik |
| Umfang: | 4 SWS / 6 Leistungspunkte |
| Ort: | Gaede-Hörsaal (Geb. 30.22) |
| Zeit: | Donnerstag, 14:00-15:30 und Freitag, 11:30-13:00 |
Aktuelles
- 29.08.16: Die vorläufigen Klausurergebnisse zur Nachklausur sind online.
- 24.08.16: Die Klausureinsicht zur Nachklausur findet am 01.09. von 14:00-15:00 Uhr in Raum 201 (Geb. 50.34) statt.
- 03.08.16: Änderungen in der Anmeldeliste: Durch einen Fehler war die bisher veröffentlichte Anmeldeliste zur Nachklausur fehlerhaft. Dieser Fehler ist mittlerweile in der aktuellen Liste korrigiert.
- 02.08.16: Die Klausur am 05.08. um 11 Uhr findet im Gaede-Hörsaal statt. Anmeldeliste und weitere Informationen zur Klausur sind online.
-
04.05.16: Bei der Berechnung der Gesamtpunktzahl zur Klausur wurden nicht in allen Fällen die Bonuspunkte des ersten Zwischentests berücksichtigt.
Die korrigierten Klausurergebnisse sind nun online. Durch die Änderung hat sich die Note der Klausuren mit dem Code 110, 165, 169, 192 und 203 um 0,3 bzw. 0,4 verbessert.
- 14.04.16: Die Klausureinsicht zur Hauptklausur findet am 29.04. von 13:30-16:00 Uhr in Raum 201 (Geb. 50.34) statt.
- 04.04.16: Die vorläufigen Klausurergebnisse zur Hauptklausur sind online. Der Termin der Klausureinsicht wird noch bekannt gegeben.
Materialien
Skriptum
skriptum.pdfForum und Einreichung von Lösungen: ilias@kit
Bitte beachten Sie die Regeln. Insbesondere dürfen keine Lösungen gepostet werden.
- Direktlink zum Ilias-Server am KIT
- Wegweiser im Ilias-System: Magazin -> Organisationseinheiten -> Fakultät für Informatik -> WS 15/16 -> Formale Systeme
Folien
Vorlesung am 22.10.15
Organisatorisches: bildschirm - druck
Syntax und Semantik der Aussagenlogik: bildschirm - druck
Vorlesung am 23.10.15
Syntax und Semantik der Aussagenlogik (Fortsetzung und Ende)
Craigsches Interpolationslemma: bildschirm - druck
Vorlesung am 29.10.15
Kurze Konjunktive Normalform: bildschirm - druck
Shannon-Graphen, OBBDs: bildschirm - druck
Vorlesung am 05.11.15
Shannon-Graphen, OBBDs (Fortsetzung und Ende)
Das Erfüllbarkeitsproblem der Aussagenlogik, DPLL-Verfahren: bildschirm - druck
Vorlesung am 06.11.15
Das Erfüllbarkeitsproblem der Aussagenlogik, DPLL-Verfahren (Fortsetzung und Ende)
Einführung in die Prädikatenlogik: bildschirm - druck
Vorlesung am 12.11.15
Einführung in die Prädikatenlogik (Fortsetzung und Ende)
Vorlesung am 19.11.15
Semantik der Prädikatenlogik: bildschirm - druck
Vorlesung am 20.11.15
Semantik der Prädikatenlogik (Fortsetzung und Ende)
Normalformen für Formeln der Prädikatenlogik: bildschirm - druck
Vorlesung am 26.11.15
Normalformen für Formeln der Prädikatenlogik (Fortsetzung und Ende)
Vorlesung am 03.12.15
Beweistheorie - Einführendes Beispiel: bildschirm - druck
Hilbertkalkül: bildschirm - druck
Vorlesung am 04.12.15
Resolutionskalkül für die Aussagenlogik: bildschirm - druck
Resolutionskalkül für die Prädikatenlogik (bis Folie 5): bildschirm - druck
Vorlesung am 10.12.15
Resolutionskalkül für die Aussagenlogik (Fortsetzung und Ende)
Tableaukalkül (bis Folie 13): bildschirm - druck
Vorlesung am 17.12.15
Tableaukalkül (Fortsetzung und Ende)
Vorlesung am 18.12.15
Sequenzenkalkül: bildschirm - druck
Vorlesung am 07.01.16
Peano-Arithmetik: bildschirm - druck
Java Modeling Language (bis Folie 9): bildschirm
(JML Homepage, JML Reference Manual,
Theorembeweiser KeY)
Vorlesung am 14.01.16
Java Modeling Language (Fortsetzung und Ende)
Vorlesung am 21.01.16
Reduktionssysteme: bildschirm - druck
Termersetzungssysteme (bis Folie 4): bildschirm - druck
Vorlesung am 28.01.16
Termersetzungssysteme (Fortsetzung und Ende)
Modallogik (bis Folie 14): bildschirm - druck
Vorlesung am 29.01.16
Modallogik (Fortsetzung und Ende)
Vorlesung am 04.02.16
Modallogischer Hilbertkalkül, Beispielbeweis zur Logelei mit den drei Weisen: bildschirm
Endliche Automaten - kurze Wiederholung: bildschirm - druck
Büchi-Automaten (bis Folie 8): bildschirm - druck
Vorlesung am 11.02.16
Büchi-Automaten (Fortsetzung und Ende)
Lineare Temporale Logik (LTL): bildschirm - druck
LTL und Büchi-Automaten (bis Folie 8): bildschirm - druck
Vorlesung am 12.02.16
LTL und Büchi-Automaten (Fortsetzung und Ende)
LTL und Model Checking: bildschirm - druck
Wiederholung: bildschirm - druck
Übungsblätter
Jeden Montag wird hier ein neues Übungsblatt bereitgestellt. Die Lösungen von jeweils zwei Blättern werden dann in den 14-tägig stattfinden Übungen am Freitag besprochen.
| Ausgabe am |
Besprechung am |
Musterlösung |
|
| blatt1.pdf | 26.10.15 | 30.10.15 | blatt1-lsg.pdf |
| blatt2.pdf | 02.11.15 | 13.11.15 | blatt2-lsg.pdf |
| blatt3.pdf | 09.11.15 | 13.11.15 | blatt3-lsg.pdf |
| blatt4.pdf | 16.11.15 | 27.11.15 | blatt4-lsg.pdf |
| blatt5.pdf | 23.11.15 | 27.11.15 | blatt5-lsg.pdf |
| blatt6.pdf | 30.11.15 | 11.12.15 | blatt6-lsg.pdf |
| blatt7.pdf | 07.12.15 | 11.12.15 | blatt7-lsg.pdf |
| blatt8.pdf | 14.12.15 | 18.12.15 | blatt8-lsg.pdf |
| blatt9.pdf | 21.12.15 | 08.01.16 | blatt9-lsg.pdf |
| blatt10.pdf | 11.01.16 | 22.01.16 | blatt10-lsg.pdf |
| blatt11.pdf | 18.01.16 | 22.01.16 | blatt11-lsg.pdf |
| blatt12.pdf | 27.01.16 | 05.02.16 | blatt12-lsg.pdf |
| blatt13.pdf | 02.02.16 | 05.02.16 | blatt13-lsg.pdf |
| blatt14.pdf | 09.02.16 | 12.02.16 | blatt14-lsg.pdf |
Praxisaufgaben
Sie können Ihre Lösungen zu Praxisaufgaben einreichen, um Bonuspunkte für den Übungsschein zu erzielen (s.u.).
Die Abgabe erfolgt im Ilias-Modul zur Vorlesung.
| Ausgabe am |
Abgabe bis |
||
| praxis1.pdf | 27.11.2015 | 06.01.2016 | Weitere Informationen |
| praxis2.pdf | 03.02.2016 | 29.02.2016 | Weitere Informationen |
Übungsschein
Im Laufe des Semesters finden 2 Zwischentests statt und es gibt 2 Praxisaufgaben (s.o.). Die Teilnahme an den Zwischentests und den Praxisaufgaben ist freiwillig. Die erzielten Übungspunkte werden mit den erzielten Punkten der bestandenen Abschlussklausur verrechnet.Abschlussklausur
Die Abschlussklausur findet am Freitag, dem 04.03.2016 um 11:00 Uhr statt.
Die Anmeldung zur Klausur geschieht über das Studierendenportal des KIT.
Eine weitere Klausur findet im Sommersemester 2016, am Freitag, 05.08.2016 um 11:00 statt. Zu dieser Klausur wird man sich ab dem 17.06. und bis zum 29.07. an- und abmelden können.
Termine
| 22.10.2015 |
Vorlesung |
| 23.10.2015 |
Vorlesung |
| 29.10.2015 |
Vorlesung |
| 30.10.2015 | Übung |
| 05.11.2015 |
Vorlesung |
| 06.11.2015 | Vorlesung |
| 12.11.2015 | Vorlesung |
| 13.11.2015 | Übung |
| 19.11.2015 | Vorlesung |
| 20.11.2015 | Vorlesung |
| 26.11.2015 | Vorlesung |
| 27.11.2015 | Übung / 1. Zwischentest |
| 03.12.2015 |
Vorlesung |
| 04.12.2015 | Vorlesung |
| 10.12.2015 | Vorlesung |
| 11.12.2015 |
Übung |
| 17.12.2015 | Vorlesung |
| 18.12.2015 | Vorlesung / Übung |
| 24.12.2015 - 06.01.2016 |
Vorlesungsfreie Zeit |
| 07.01.2016 |
Vorlesung |
| 08.01.2016 | Übung |
| 14.01.2016 | Vorlesung |
| 15.01.2016 | Vorlesung |
| 21.01.2016 | Vorlesung |
| 22.01.2016 | Übung / 2. Zwischentest |
| 28.01.2016 | Vorlesung |
| 29.01.2016 | Vorlesung |
| 04.02.2016 | Vorlesung |
| 05.02.2016 | Übung |
| 11.02.2016 | Vorlesung |
| 12.02.2016 | Vorlesung / Übung |
| 04.03.2016, 11 Uhr | Klausur |
| 05.08.2016, 11 Uhr | Nachklausur |
Inhaltsübersicht
- Aussagenlogik
- Syntax und Semantik
- Kalküle
- Anwendungen
- Prädikatenlogik
- Syntax und Semantik
- Kalküle
- Anwendungen
- Gleichheit
- Java Modeling Language (JML)
- Modale Aussagenlogik
- Temporale Logik (LTL)
- Endliche Automaten (Wiederholung)
- Büchi Automaten
- Modellprüfung
Link zur Webseite des vorigen Jahres