Wintersemester 2019/2020
Formale Systeme
Prof. Dr. Bernhard Beckert
Dr. Mattias Ulbrich, Mihai Herda,
Jonas Schiffl, Alexander Weigl
| Typ: | Vorlesung |
|---|---|
| Zielgruppe: | Bachelor Informatik, Master Informatik |
| Umfang: | 4 SWS / 6 Leistungspunkte |
| Ort: | Gaede-Hörsaal (Geb. 30.22) |
| Zeit: | Donnerstag, 14:00 - 15:30 Uhr Freitag, 11:30 - 13:00 Uhr |
| Veranstaltungs-Nr.: | 24086 |
| ILIAS-Kurs: | Link |
Aktuelles
-
Klausureinsicht: Wir planen mit der Klausureinsicht im November für die beiden Klausuren WS19/20 und SS20.
Um besser planen zu kommen bitten wir um eine unverbindliche Voranmeldung bis zum 30. Oktober 2020.
Dazu genügt eine E-Mail an weigl@kit.edu mit dem Betreff "Klausureinsicht". -
17.09.2020: Die Ergebnisse der Nachklausur vom 31.07.2020 sind jetzt verfügbar.
Wenn Sie Ihre Klausur-ID vergessen haben, können Sie diese per E-Mail von Ihrer @student.kit.edu-Adresse bei Michael Kirsten erfragen.
Geben Sie dabei unbedingt Ihre Matrikelnummer an! Die Klausureinsicht (zusammen mit der Einsicht zur Klausur vom Februar) wird zu Beginn
der Vorlesungszeit stattfinden. Den konkreten Termin werden wir vor Vorlesungsbeginn hier bekanntgeben. -
07.05.2020: Die Klausurergebnisse sind jetzt verfügbar.
Bei vergessener Klausur-ID eine E-Mail an Mihai Herda von der @student.kit.edu-Adresse, Matrikelnummer angeben. - 06.02.2020: Aktualisierte Aufgabensammlung ist im ILIAS verfügbar.
- 01.10.2019: ILIAS-Kurs ist jetzt online.
Materialien
Skriptum
Aufgabensammlung
aufgaben.pdf (06.02.2020)
loesungen.pdf (06.02.2020)
Altklausuren
Übungsaufgaben
Folgende Aufgaben möchten wir besprechen:
- Einleitende Beispiele: Aufgabe 2
- Interpolaten: Aufgaben 8, 9
- Normalformen: Aufgaben 11, 12, 13
- Shannongraphen: Aufgaben 20, 21, 22
- DPLL: Aufgabe 28
- Substitutionen: Aufgaben 30, 31, 34
- Semantik der Prädikatenlogik: Aufgaben 39, 43, 44
- Normalformen (PL1): Aufgaben 47, 48
- Hilbertkalkül: Aufgabe 51
- Resolutionskalkül: Aufgaben 60, 62
- Tableaukalkül: Aufgaben 64, 66, 67, 69
- Java Modeling Language: Aufgaben 72, 73, 74
- Theorieschließen: Aufgaben 101, 102, 103
- LTL, Büchi-Automaten: Aufgabe 82a-d, 85, 92, 96
Forum und Einreichung von Lösungen der Praxisaufgaben
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 19/20 -> Formale Systeme
Folien
Organisatorisches: bildschirm - druck
Syntax und Semantik der Aussagenlogik: bildschirm - druck
Craigsches Interpolationslemma: bildschirm - druck
Normalformen: bildschirm - druck
Shannon-Graphen, OBBDs: bildschirm - druck
Das Erfüllbarkeitsproblem der Aussagenlogik, DPLL-Verfahren: bildschirm - druck
Einführung in die Prädikatenlogik: bildschirm - druck
Semantik der Prädikatenlogik: bildschirm - druck
Normalformen für Formeln der Prädikatenlogik: bildschirm - druck
Beweistheorie - Einführendes Beispiel: bildschirm - druck
Hilbertkalkül: bildschirm - druck
Resolutionskalkül für die Aussagenlogik: bildschirm - druck
Resolutionskalkül für die Prädikatenlogik: bildschirm - druck
Tableaukalkül: bildschirm - druck
Sequenzenkalkül: bildschirm - druck
Java Modeling Language: bildschirm
(JML Homepage, JML Reference Manual,
Theorembeweiser KeY)
Peano-Arithmetik: bildschirm - druck
Satisfiability Modulo Theories: siehe ILIAS
Reduktionssysteme: bildschirm - druck
Termersetzungssysteme: bildschirm - druck
Modallogik: Drei Weise - bildschirm - druck
Automaten (Wiederholung): bildschirm - druck
Büchi-Automaten: bildschirm - druck
Lineare Temporale Logik (LTL): bildschirm - druck
LTL und Büchi-Automaten: bildschirm - druck
LTL und Model Checking: bildschirm - druck
Wiederholung: bildschirm - druck
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 |
||
| 1. Praxisaufgabe: LightUp | 14.11.2019 | 06.01.2020 | Benötigte Dateien: lightup-1.0.zip |
| 2. Praxisaufgabe: Blockchain-Modellierung in SMT | 13.12.2019 | 31.01.2020 | Folien zur Aufgabe |
| 3. Praxisaufgabe: JML und KeY | 16.01.2020 | 14.02.2020 | InsertionSort.java |
Link zur Webseite des vorigen Jahres