Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Wintersemester 2018/2019

Formale Systeme

Prof. Dr. Bernhard Beckert (BB)
Dr. Mattias Ulbrich, Mihai Herda, Alexander Weigl

Die Klausurergebnisse sind jetzt verfügbar.
Die Klausureinsicht findet am Montag, 06. Mai 2019, 14:00 Uhr im Raum 201 (Gebäude 50.34) statt.
Eine Musterlösung wurde bei den Altklausuren hinzugefügt.

Klausur-ID verloren? E-Mail von euer vorname.nachname@student.kit.edu Adresse an Mihai Herda schicken, Matrikelnummer angeben.

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 (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.


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 FolienRahmenwerkFolien SMT-LIB
3. Praxisaufgabe: JML und KeY 29.01.2019 24.02.2019 Selectionsort.java


Link zur Webseite des vorigen Jahres