Wintersemester 2018/2019

Formale Systeme

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

Die Ergebnisse der Nachklausur sind jetzt verfügbar.
Die Musterlösung zur Nachklausur ist hier verfügbar.
Die Klausureinsicht findet am Montag, 21.Oktober 2019, 10:00 Uhr im Raum 201 (Gebäude 50.34) statt.

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