Formale Systeme

Vorlesung im Wintersemester 2015/2016

Prof. Dr. Bernhard Beckert (BB)
Dr. Thorsten Bormer (TB), Dr. Vladimir Klebanov (VK), Dr. Mattias Ulbrich (MU)


Zielgruppe: Diplom Informatik, Bachelor Informatik, Master Informatik
Umfang: 4 SWS / 6 Leistungspunkte
Ort: Gaede-Hörsaal (Geb. 30.22)
Zeit: Donnerstag, 14:00-15:30 und Freitag, 11:30-13:00

Aktuelles

  • 29.08.16: Die vorläufigen Klausurergebnisse zur Nachklausur sind online.
  • 24.08.16: Die Klausureinsicht zur Nachklausur findet am 01.09. von 14:00-15:00 Uhr in Raum 201 (Geb. 50.34) statt.
  • 03.08.16: Änderungen in der Anmeldeliste: Durch einen Fehler war die bisher veröffentlichte Anmeldeliste zur Nachklausur fehlerhaft. Dieser Fehler ist mittlerweile in der aktuellen Liste korrigiert.
  • 02.08.16: Die Klausur am 05.08. um 11 Uhr findet im Gaede-Hörsaal statt. Anmeldeliste und weitere Informationen zur Klausur sind online.
  • 04.05.16: Bei der Berechnung der Gesamtpunktzahl zur Klausur wurden nicht in allen Fällen die Bonuspunkte des ersten Zwischentests berücksichtigt. Die korrigierten Klausurergebnisse sind nun online. Durch die Änderung hat sich die Note der Klausuren mit dem Code 110, 165, 169, 192 und 203 um 0,3 bzw. 0,4 verbessert.
  • 14.04.16: Die Klausureinsicht zur Hauptklausur findet am 29.04. von 13:30-16:00 Uhr in Raum 201 (Geb. 50.34) statt.
  • 04.04.16: Die vorläufigen Klausurergebnisse zur Hauptklausur sind online. Der Termin der Klausureinsicht wird noch bekannt gegeben.



Materialien

Skriptum

skriptum.pdf


Forum und Einreichung von Lösungen: ilias@kit

Bitte beachten Sie die Regeln. Insbesondere dürfen keine Lösungen gepostet werden.


Folien

Vorlesung am 22.10.15
Organisatorisches: bildschirm - druck
Syntax und Semantik der Aussagenlogik: bildschirm - druck

Vorlesung am 23.10.15
Syntax und Semantik der Aussagenlogik (Fortsetzung und Ende)
Craigsches Interpolationslemma: bildschirm - druck

Vorlesung am 29.10.15
Kurze Konjunktive Normalform: bildschirm - druck
Shannon-Graphen, OBBDs: bildschirm - druck

Vorlesung am 05.11.15
Shannon-Graphen, OBBDs (Fortsetzung und Ende)
Das Erfüllbarkeitsproblem der Aussagenlogik, DPLL-Verfahren: bildschirm - druck

Vorlesung am 06.11.15
Das Erfüllbarkeitsproblem der Aussagenlogik, DPLL-Verfahren (Fortsetzung und Ende)
Einführung in die Prädikatenlogik: bildschirm - druck

Vorlesung am 12.11.15
Einführung in die Prädikatenlogik (Fortsetzung und Ende)

Vorlesung am 19.11.15
Semantik der Prädikatenlogik: bildschirm - druck

Vorlesung am 20.11.15
Semantik der Prädikatenlogik (Fortsetzung und Ende)
Normalformen für Formeln der Prädikatenlogik: bildschirm - druck

Vorlesung am 26.11.15
Normalformen für Formeln der Prädikatenlogik (Fortsetzung und Ende)

Vorlesung am 03.12.15
Beweistheorie - Einführendes Beispiel: bildschirm - druck
Hilbertkalkül: bildschirm - druck

Vorlesung am 04.12.15
Resolutionskalkül für die Aussagenlogik: bildschirm - druck
Resolutionskalkül für die Prädikatenlogik (bis Folie 5): bildschirm - druck

Vorlesung am 10.12.15
Resolutionskalkül für die Aussagenlogik (Fortsetzung und Ende)
Tableaukalkül (bis Folie 13): bildschirm - druck

Vorlesung am 17.12.15
Tableaukalkül (Fortsetzung und Ende)

Vorlesung am 18.12.15
Sequenzenkalkül: bildschirm - druck

Vorlesung am 07.01.16
Peano-Arithmetik: bildschirm - druck
Java Modeling Language (bis Folie 9): bildschirm
(JML Homepage, JML Reference Manual, Theorembeweiser KeY)

Vorlesung am 14.01.16
Java Modeling Language (Fortsetzung und Ende)

Vorlesung am 21.01.16
Reduktionssysteme: bildschirm - druck
Termersetzungssysteme (bis Folie 4): bildschirm - druck

Vorlesung am 28.01.16
Termersetzungssysteme (Fortsetzung und Ende)
Modallogik (bis Folie 14): bildschirm - druck

Vorlesung am 29.01.16
Modallogik (Fortsetzung und Ende)

Vorlesung am 04.02.16
Modallogischer Hilbertkalkül, Beispielbeweis zur Logelei mit den drei Weisen: bildschirm
Endliche Automaten - kurze Wiederholung: bildschirm - druck
Büchi-Automaten (bis Folie 8): bildschirm - druck

Vorlesung am 11.02.16
Büchi-Automaten (Fortsetzung und Ende)
Lineare Temporale Logik (LTL): bildschirm - druck
LTL und Büchi-Automaten (bis Folie 8): bildschirm - druck

Vorlesung am 12.02.16
LTL und Büchi-Automaten (Fortsetzung und Ende)
LTL und Model Checking: bildschirm - druck
Wiederholung: bildschirm - druck


Übungsblätter

Jeden Montag wird hier ein neues Übungsblatt bereitgestellt. Die Lösungen von jeweils zwei Blättern werden dann in den 14-tägig stattfinden Übungen am Freitag besprochen.


Ausgabe am
Besprechung am
Musterlösung
blatt1.pdf 26.10.15 30.10.15 blatt1-lsg.pdf
blatt2.pdf 02.11.15 13.11.15 blatt2-lsg.pdf
blatt3.pdf 09.11.15 13.11.15 blatt3-lsg.pdf
blatt4.pdf 16.11.15 27.11.15 blatt4-lsg.pdf
blatt5.pdf 23.11.15 27.11.15 blatt5-lsg.pdf
blatt6.pdf 30.11.15 11.12.15 blatt6-lsg.pdf
blatt7.pdf 07.12.15 11.12.15 blatt7-lsg.pdf
blatt8.pdf 14.12.15 18.12.15 blatt8-lsg.pdf
blatt9.pdf 21.12.15 08.01.16 blatt9-lsg.pdf
blatt10.pdf 11.01.16 22.01.16 blatt10-lsg.pdf
blatt11.pdf 18.01.16 22.01.16 blatt11-lsg.pdf
blatt12.pdf 27.01.16 05.02.16 blatt12-lsg.pdf
blatt13.pdf 02.02.16 05.02.16 blatt13-lsg.pdf
blatt14.pdf 09.02.16 12.02.16 blatt14-lsg.pdf

 

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
praxis1.pdf 27.11.2015 06.01.2016 Weitere Informationen
praxis2.pdf 03.02.2016 29.02.2016 Weitere Informationen

Übungsschein

Im Laufe des Semesters finden 2 Zwischentests statt und es gibt 2 Praxisaufgaben (s.o.). Die Teilnahme an den Zwischentests und den Praxisaufgaben ist freiwillig. Die erzielten Übungspunkte werden mit den erzielten Punkten der bestandenen Abschlussklausur verrechnet.



Abschlussklausur

Die Abschlussklausur findet am Freitag, dem 04.03.2016 um 11:00 Uhr statt.

Die Anmeldung zur Klausur geschieht über das Studierendenportal des KIT.

Eine weitere Klausur findet im Sommersemester 2016, am Freitag, 05.08.2016 um 11:00 statt. Zu dieser Klausur wird man sich ab dem 17.06. und bis zum 29.07. an- und abmelden können.


Termine

22.10.2015
Vorlesung
23.10.2015
Vorlesung
29.10.2015
Vorlesung
30.10.2015 Übung
05.11.2015
Vorlesung
06.11.2015 Vorlesung
12.11.2015 Vorlesung
13.11.2015 Übung
19.11.2015 Vorlesung
20.11.2015 Vorlesung
26.11.2015 Vorlesung
27.11.2015 Übung / 1. Zwischentest
03.12.2015
Vorlesung
04.12.2015 Vorlesung
10.12.2015 Vorlesung
11.12.2015
Übung
17.12.2015 Vorlesung
18.12.2015 Vorlesung / Übung
24.12.2015 - 06.01.2016
Vorlesungsfreie Zeit
07.01.2016
Vorlesung
08.01.2016 Übung
14.01.2016 Vorlesung
15.01.2016 Vorlesung
21.01.2016 Vorlesung
22.01.2016 Übung / 2. Zwischentest
28.01.2016 Vorlesung
29.01.2016 Vorlesung
04.02.2016 Vorlesung
05.02.2016 Übung
11.02.2016 Vorlesung
12.02.2016 Vorlesung / Übung
04.03.2016, 11 Uhr Klausur
05.08.2016, 11 Uhr Nachklausur


Inhaltsübersicht

  • Aussagenlogik
    • Syntax und Semantik
    • Kalküle
    • Anwendungen
  • Prädikatenlogik
    • Syntax und Semantik
    • Kalküle
    • Anwendungen
  • Gleichheit
  • Java Modeling Language (JML)
  • Modale Aussagenlogik
  • Temporale Logik (LTL)
  • Endliche Automaten (Wiederholung)
  • Büchi Automaten
  • Modellprüfung


Link zur Webseite des vorigen Jahres