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 / 6 Leistungspunkte |
| 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.pdfForum und Einreichung von Lösungen: ilias@kit
Bitte beachten Sie die Regeln. Insbesondere dürfen keine Lösungen gepostet werden.
- Direktlink zum Ilias-Server am KIT
- Wegweiser im Ilias-System: Magazin -> Organisationseinheiten -> Fakultät für Informatik -> WS 14/15 -> Formale Systeme
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