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

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