Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Wintersemester 2019/2020

Formale Systeme

Prof. Dr. Bernhard Beckert
Dr. Mattias Ulbrich, Mihai Herda, Jonas Schiffl, Alexander Weigl

Freitag, 28.02.2020, um 10:00 Uhr, findet die Formale Systeme Klausur statt.

Die Einteilung in Hörsälen ist wie folgt:
Studierende mit Nachnamen A-K: Hörsaal "Neue Chemie"
Studierende mit Nachnamen L-Z: Hörsaal am Fasanengarten


Alle erzielte Bonuspunkte sind jetzt verfügbar.

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


Materialien

Skriptum

skriptum.pdf

Aufgabensammlung

aufgaben.pdf (06.02.2020)
loesungen.pdf (06.02.2020)


Altklausuren

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.


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