Wintersemester 2018/2019
Formale Systeme
Prof. Dr. Bernhard Beckert (BB)
Dr. Mattias Ulbrich, Mihai Herda,
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 |
Aktuelles
- 15.01.19: Die Ergebnisse des Zwischentests sind jetzt online.
- 26.09.18: ILIAS-Kurs ist jetzt online.
Materialien
Skriptum
skriptum.pdfAufgabensammlung
aufgaben.pdf (08.02.2016)loesungen.pdf (08.02.2016)
Altklausuren
AltklausurenÜbungsaufgaben
Folgende Aufgaben werden/wurden besprochen:
- 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
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 18/19 -> Formale Systeme
Folien
Organisatorisches: bildschirm - druck
Syntax und Semantik der Aussagenlogik: bildschirm - druck
Craigsches Interpolationslemma: bildschirm - druck
Kurze Konjunktive Normalform: 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
Peano-Arithmetik: bildschirm - druck
Satisfiability Modulo Theories (vorläufige Version der Folien, korrigierte Folien werden bald hochgeladen): bildschirm
Java Modeling Language: bildschirm
(JML Homepage, JML Reference Manual,
Theorembeweiser KeY)
Reduktionssysteme: bildschirm - druck
Termersetzungssysteme: bildschirm - druck
Modallogik: Drei Weise - bildschirm - druck
Lineare Temporale Logik (LTL): bildschirm - druck
Büchi-Automaten: 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: Kuromasu | 15.11.2018 | 06.01.2019 | Benötigte Dateien: Kuromasu-1.3.zip | Javadoc |
| 2. Praxisaufgabe: Auftragsplanung mit SMT | 10.01.2019 | 10.02.2019 | Folien ∣ Rahmenwerk ∣ Folien SMT-LIB |
| 3. Praxisaufgabe: JML und KeY | 29.01.2019 | 24.02.2019 | Selectionsort.java |
Link zur Webseite des vorigen Jahres