HOME | IMPRESSUM | SITEMAP | KIT

Formale Systeme

Vorlesung im Wintersemester 2014/2015

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


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

Aktuelles

  • 14.09.15: Die Klausureinsicht zur 2. Hauptklausur findet am Dienstag, dem 22.09. von 14:00-15:30 Uhr in Raum 201 (Geb. 50.34) statt.
  • 04.09.15: Die vorläufigen Klausurergebnisse zur 2. Hauptklausur sind online. Der Termin der Klausureinsicht wird noch bekannt gegeben.
  • 27.07.15: Abschlussklausur im Sommersemester findet statt am 31.07.15. Wichtig: Bitte informieren Sie sich hier über die Details.
  • 23.06.15: Die Aufgaben zur Abschlussklausur vom 06.03.2015 sind online.
  • 07.05.15: Die Klausureinsicht findet am Mittwoch, dem 20.05. in Raum 201 (Geb. 50.34) in zwei Gruppen statt. Aufteilung der Gruppen nach dem ersten Buchstaben des Nachnamens: Gruppe 1: A-L ab 11:00 Uhr; Gruppe 2: M-Z ab 15:00 Uhr.
  • 02.05.15: Fehler in der Zuordnung der Punktzahlen zu Klausurnoten korrigiert: statt einer 1.0 ab 58.5 Punkten wurde irrtümlich die Note 1.3 in der ursprünglich veröffentlichen Liste ausgewiesen.
  • 01.05.15: Die vorläufigen Klausurergebnisse zur Hauptklausur sind online. Der Termin der Klausureinsicht wird noch bekannt gegeben.
  • 02.03.15: Am Freitag, 06.03.2015 findet die Abschlussklausur zur Vorlesung statt.
  • 18.12.14: Der Termin für die 2. Hauptklausur, die im Sommersemester 2015 stattfindet, steht nun fest. Sie findet Freitag, den 31.07.15, 11 Uhr, statt.



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 23.10.14
Organisatorisches: bildschirm - druck
Syntax und Semantik der Aussagenlogik: bildschirm - druck

Vorlesung am 24.10.14
Syntax und Semantik der Aussagenlogik (Fortsetzung und Ende)
Craigsches Interpolationslemma: bildschirm - druck
Kurze Konjunktive Normalform: bildschirm - druck (aktualisiert am 06.11.14)

Vorlesung am 30.10.14
Kurze Konjunktive Normalform (Fortsetzung und Ende)
Shannon-Graphen (OBBD): bildschirm - druck

Vorlesung am 06.11.14
Das Erfüllbarkeitsproblem der Aussagenlogik, DPLL-Verfahren: bildschirm - druck (aktualisiert am 12.11.14)

Vorlesung am 07.11.14
Einführung in die Prädikatenlogik (bis Folie 23): bildschirm - druck

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

Vorlesung am 20.11.14
Semantik der Prädikatenlogik (bis Folie 34): bildschirm - druck

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

Vorlesung am 04.12.14
Normalformen für Formeln der Prädikatenlogik (Fortsetzung und Ende)
Beweistheorie - Einführendes Beispiel: bildschirm - druck
Hilbertkalkül bildschirm - druck

Vorlesung am 05.12.14
Resolutionskalkül für die Aussagenlogik: bildschirm - druck

Vorlesung am 11.12.14
Resolutionskalkül für die Prädikatenlogik: bildschirm - druck
Tableaukalkül (bis Folie 17): bildschirm - druck

Vorlesung am 18.12.14
Tableaukalkül (Fortsetzung und Ende)

Vorlesung am 19.12.14
Sequenzenkalkül: bildschirm - druck

Vorlesung am 08.01.15
Peano-Arithmetik: bildschirm - druck
Java Modeling Language (bis Folie 11): bildschirm

Vorlesung am 15.01.15
Java Modeling Language (Fortsetzung und Ende)
Reduktionssysteme (bis Folie 17): bildschirm - druck

Vorlesung am 16.01.15
Demo KeY-System
Reduktionssysteme (Fortsetzung und Ende)
Termersetzungssysteme bildschirm - druck

Vorlesung am 22.01.15
Modallogik (bis Folie 27): bildschirm - druck

Vorlesung am 29.01.15
Modallogik (Fortsetzung und Ende)
Modallogischer Hilbertkalkül, Beispielbeweis zur Logelei mit den drei Weisen: bildschirm
Endliche Automaten - kurze Wiederholung: bildschirm - druck

Vorlesung am 30.01.15
Büchi-Automaten (bis Folie 14): bildschirm - druck

Vorlesung am 05.02.15
Büchi-Automaten (Fortsetzung und Ende)
Lineare Temporale Logik (LTL): bildschirm - druck
LTL und Büchi-Automaten: bildschirm - druck

Vorlesung am 12.02.15
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 27.10.14 31.10.14 blatt1-lsg.pdf
blatt2.pdf 03.11.14 14.11.14 blatt2-lsg.pdf
blatt3.pdf 10.11.14 14.11.14 blatt3-lsg.pdf
blatt4.pdf 17.11.14 21.11.14 blatt4-lsg.pdf
blatt5.pdf 24.11.14 28.11.14 blatt5-lsg.pdf
blatt6.pdf 01.12.14 12.12.14 blatt6-lsg.pdf
blatt7.pdf 08.12.14 12.12.14 blatt7-lsg.pdf
blatt8.pdf 16.12.14 19.12.14 blatt8-lsg.pdf
blatt9.pdf 23.12.14 09.01.15 blatt9-lsg.pdf
blatt10.pdf 12.01.15 23.01.15 blatt10-lsg.pdf
blatt11.pdf 19.01.15 23.01.15 blatt11-lsg.pdf
blatt12.pdf 26.01.15 06.02.15 blatt12-lsg.pdf
blatt13.pdf 02.02.15 12.02.15 blatt13-lsg.pdf
blatt14.pdf 09.02.15 13.02.15 blatt14-lsg.pdf

 

Praxisaufgaben

Siehe Abschnitt Übungsschein.

 


Termine

23.10.2014
Vorlesung
24.10.2014
Vorlesung
30.10.2014
Vorlesung
31.10.2014 Übung
06.11.2014
Vorlesung
07.11.2014 Vorlesung
13.11.2014 Vorlesung
14.11.2014 Übung / 1. Zwischentest
20.11.2014 Vorlesung
21.11.2014 Übung     (neu!)
27.11.2014 Vorlesung
28.11.2014 Übung
04.12.2014
Vorlesung
05.12.2014 Vorlesung
11.12.2014 Vorlesung
12.12.2014
Übung / 2. Zwischentest
18.12.2014 Vorlesung
19.12.2014 Vorlesung / Übung (neu!)
24.12.2014 - 06.01.2015
Vorlesungsfreie Zeit
08.01.2015
Vorlesung
09.01.2015 Übung / 3. Zwischentest
15.01.2015 Vorlesung
16.01.2015 Vorlesung
22.01.2015 Vorlesung
23.01.2015 Übung
29.01.2015 Vorlesung
30.01.2015 Vorlesung
05.02.2015 Vorlesung
06.02.2015 Übung / 4. Zwischentest
12.02.2015 Vorlesung / Übung
13.02.2015 Übung
06.03.2015, 11 Uhr Klausur


Übungsschein

Im Laufe des Semesters finden 4 Zwischentests statt (je 10 Übungspunkte) und es gibt 2 Praxisaufgaben (je 20 Übungspunkte). Die Teilnahme an den Zwischentests und den Praxisaufgaben ist freiwillig. Die erzielten Übungspunkte werden im Verhältnis 1:10 als Bonuspunkte auf die bestandene Abschlussklausur angerechnet.


Zwischentests

  • Jeweils am Anfang der Übungen am 14.11.14, 12.12.14, 09.01.15, 06.02.15
  • Dauer: 20min
  • Es sind keine Hilfsmittel zugelassen
  • Eine Anmeldung ist nicht erforderlich

Aufgaben und Musterlösungen
Zwischentest am
Aufgabenstellung
Musterlösung
14.11.2014
Aufgaben
Lösungen
12.12.2014
Aufgaben
Lösungen
09.01.2015
Aufgaben
Lösungen
06.02.2015
Aufgaben
Lösungen

 

Praxisaufgaben


Ausgabe am
Abgabe am
 
praxis1.pdf
19.11.2014
19.12.2014
weitere Informationen ...
praxis2.pdf
21.01.2015
12.02.2015
weitere Informationen ...
Bitte verwenden Sie in jedem Fall die KeY-Version von der Vorlesungshomepage und nicht die Versionen auf den Seiten des Tools.

 

Die Bearbeitung der Praxisaufgaben ist freiwillig. Jedoch können und sollen Sie Ihre Lösungen zu den Praxisaufgaben abgeben. Für die erfolgreiche Bearbeitung der beiden Praxisaufgaben werden jeweils bis zu 20 Übungspunkte vergeben.

Die Abgabe der Lösungen zu den Praxisaufgaben erfolgt über die ILIAS-Seite.


Abschlussklausur

Weitere Informationen zur Klausur am 06.03.2015...

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

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

Eine weitere Klausur findet im Sommersemesters 2015, am Freitag, dem 31.07.2015, 11:00, statt. Zu dieser wird man sich bis zum 24.07.15 an- und abmelden können.


Aufgaben und Musterlösungen

Klausur am 06.03.2015 Aufgaben Lösungen
Klausur am 31.07.2015 Aufgaben Lösungen


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