Formale Systeme
Wahlpflichtvorlesung im Wintersemester 2008/2009
Prof. Dr. Bernhard Beckert (im WS 08/09 Universität Karlsruhe und Universität Koblenz-Landau), Mattias Ulbrich
LOGIN
Aktuelles
21.04.09: Die Ergebnisse der Klausur vom 8.4. liegen vor.
03.04.09: Die Hörsaalbelegung zur Klausur am 8.4. liegt vor.
20.03.09: Die Aufgabenstellung und die Musterlösung zur Abschlussklausur am 19.02. stehen zur Verfügung.
09.03.09: Die Ergebnisse der Klausur vom 19.2. liegen vor.
17.02.09: Die Hörsaalbelegung zur Klausur am 19.2. liegt vor.
13.02.09: Die Musterlösungen zum 10., 11. und 12. Übungsblatt stehen zur Verfügung.
09.02.09: Das 12. Übungsblatt steht zur Verfügung. Es wird in der Übung am 13.02.09 besprochen.
06.02.09: Die Folien zur gestrigen und zur heutigen Vorlesung und die Musterlösung zur 2. Zwischenklausur stehen zur Verfügung.
03.02.09: Das 11. Übungsblatt steht zur Verfügung. Es wird in der Übung am 13.02.09 besprochen.
31.01.09: Die Folien zur gestrigen Vorlesung stehen zur Verfügung.
28.01.09: Die letzte Übung findet erst in der letzten Vorlesungswoche, am 13.02.09, statt, so dass dann noch Gelegenheit ist, alle verbliebenen Übungsblätter zu besprechen.
Dafür findet am Freitag, dem 06.02.09, eine Vorlesung statt.
28.01.09: Das 10. Übungsblatt steht zur Verfügung. Es wird in der Übung am 13.02.09 besprochen.
27.01.09: Die Folien zum Thema "Prädikatenlogik 2. Stufe" fehlten. Sie sind nun online.
27.01.09: Die Einteilung der Gruppen der zweiten Zwischenklausur ist fertig. Alle Teilnehmer erhalten auch eine E-Mail.
26.01.09: Die erste Praxisaufgabe ist bewertet. Eine Beispiellösung dafür steht zur Verfügung (s.u. bei Praxisaufgaben)
23.01.09: Die Folien zur gestrigen Vorlesung stehen zur Verfügung.
23.01.09: Die Musterlösungen zum 8. und zum 9. Übungsblatt stehen zur Verfügung.
20.01.09: Die Einsicht in die beiden Zwischenklausuren findet am 12.02.09, um 16 Uhr (Gruppe 1) bzw. 17 Uhr (Gruppe 2), in SR131 statt.
Um den Andrang etwas zu koordinieren, ist die Einsicht in zwei Gruppen geteilt. Gruppe 1: alle, die bei der erste Zwischenklausur in der 1. Gruppe mitgeschrieben haben; Gruppe 2: alle anderen.
19.01.09: Das 9. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 8. in der Übung am 23.01.09 besprochen.
18.01.09: In der nächsten Vorlesung am Donnerstag, dem 22.01.09, wird die Vorlesungbefragung (Lehrevaluation) durchgeführt.
16.01.09: Die Folien zur gestrigen und zur heutigen Vorlesung stehen zur Verfügung.
16.01.09: Die Folien zur gestrigen und zur heutigen Vorlesung stehen zur Verfügung.
16.01.09: Im Login-Bereich der Webseite können Sie nun sehen, wieviele Bonuspunkte Sie erzielt haben (insbesondere in der ersten Zwischenklausur): LOGIN
15.01.09: Die zweite Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 15.02.08 abgegeben werden. Für die erfolgreiche Bearbeitung gibt es bis zu 1,5 Bonuspunkte.
12.01.09: Das 8. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 9. in der Übung am 23.01.09 besprochen.
10.01.09: Die Musterlösungen zum 6. und 7. Übungsblatt stehen zur Verfügung.
10.01.09: Die Folien zur Vorlesung am 08.01.09 stehen zur Verfügung.
08.01.09: Die Anmeldung zur 2. Zwischenklausur am 29.01.09 ist nun möglich, und zwar bis zum 26.01.09 (bis dahin kann man sich auch wieder abmelden).
02.01.09: Die Musterlösung zur 1. Zwischenklausur steht zur Verfügung.
23.12.08: Die erste Vorlesung nach der Weihnachtspause ist am Donnerstag, dem 08.01.09. Allen Hörern der Vorlesung ein frohes Weihnachstfest und ein glückliches Neues Jahr!
23.12.08: Informationen zum KeY-System stehen zur Verfügung, das in der Vorlesung am 19.12.08 vorgestellt wurde und in der 2. Praxisaufgabe zum Einsatz kommen wird.
23.12.08: Das 7. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 6. in der Übung am 09.01.09 besprochen.
16.12.08: Die zweite Zwischenklausur findet am Donnerstag, dem 29.01.09, 14 Uhr, statt. Das Prozedere ist das gleiche wie bei der ersten Zwischenklausur.
Die Anmeldung wird ab spätestens Anfang Januar '09 möglich sein.
16.12.08: Das 6. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 7. in der Übung am 09.01.09 besprochen.
15.12.08: Die Aufgaben der ersten Zwischenklausur stehen zur Verfügung.
12.12.08: Die Musterlösungen zum 4. und zum 5. Übungsblatt stehen zur Verfügung.
11.12.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
09.12.08: Das 5. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 4. in der Übung am 12.12.08 besprochen.
07.12.08: Die Folien zur Vorlesung am Freitag (05.12.) stehen zur Verfügung.
02.12.08: Das 4. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 5. in der Übung am 12.12.08 besprochen.
01.12.08: Die Einteilung der Gruppen zur ersten Zwischenklausur liegt vor.
28.11.08: Bitte beachten Sie die unten stehenden Hinweise zum Ablauf der 1. Zwischenklausur.
27.11.08: Die Nachklausur (2. Abschlussklausur) findet am Mittwoch, dem 8. April 2009, 10 Uhr, statt.
27.11.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
24.11.08: Das 3. Übungsblatt steht zur Verfügung. Es wird in der Übung am 28.11.08 besprochen.
21.11.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
20.11.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
18.11.08: Die Webseite zur Anmeldung zu den Zwischenklausuren und zur Abgabe der Lösung der Praxisaufgaben ist freigeschaltet: LOGIN
(beim ersten Login Registrierung mit der Matrikelnummer). Die Anmeldung zur 1. Zwischenklausur ist möglich bis zum 30.11.08 (bis dahin kann man sich auch wieder abmelden).
Die Lösung zur 1. Praxisaufgabe kann bis 31.12.08 abgegeben werden.
15.11.08: Die erste Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 31.12.08 abgegeben werden. Für die erfolgreiche Bearbeitung gibt es bis zu 1,5 Bonuspunkte.
15.11.08: Die Musterlösung zum 2. Übungsblatt steht zur Verfügung.
13.11.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
10.11.08: Das 2. Übungsblatt steht zur Verfügung. Es wird in der Übung am 14.11.08 besprochen.
07.11.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
06.11.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
31.10.08: Der News-Server, auf dem die Newsgroup zur Vorlesung (uka.formsys) liegt, ist news.scc.kit.edu (nicht news.informatik.kit.edu).
31.10.08: Die Musterlösung zum 1. Übungsblatt steht zur Verfügung.
30.10.08: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
26.10.08: Das 1. Übungsblatt steht zur Verfügung. Es wird in der Übung am 31.10.08 besprochen.
25.10.08: Die Folien zu den Vorlesungen am 23.10.08 und 24.10.08 stehen zur Verfügung.
25.10.08: Newsgroup zur Vorlesung: uka.formsys
25.10.08: Weitere organisatorische Informationen auf der Webseite.
24.09.08: Webseite angelegt.
Materialien
Vorlesungsfolien
-
Einführung (Organisatorischen, Inhaltsübersicht, Literatur): bildschirm - druck - 4on1
Vorlesung am 23.10.08 -
Aussagenlogik, Syntax und Semantik: bildschirm - druck - 4on1
Vorlesung am 23.10.08 -
Aussagenlogik, konjuntive Normalform: bildschirm - druck - 4on1
Vorlesung am 23.10.08 -
Binary Decision Diagrams (BDDs): bildschirm - druck - 4on1
Vorlesung am 24.10.08 -
Aussagenlogik, Erfüllbarkeitsproblem für spezielle Formelklassen: bildschirm - druck - 4on1
Vorlesung am 30.10.08 -
Aussagenlogik, Hilbert-Kalkül: bildschirm - druck - 4on1
Vorlesung am 30.10.08 (bis Folie 8), Vorlesung am 06.11.08 (ab Folie 9) -
Aussagenlogik, Resolution: bildschirm - druck - 4on1
Vorlesung am 06.11.08 (bis Folie 9), Vorlesung am 07.11.08 (ab Folie 10) -
Aussagenlogik, Tableaukalkül: bildschirm - druck - 4on1
Vorlesung am 07.11.08 -
Aussagenlogik, Sequenzenkalkül: bildschirm - druck - 4on1
Vorlesung am 13.11.08 -
Aussagenlogik, sonstige Kalküle: bildschirm - druck - 4on1
Vorlesung am 13.11.08 -
Prädikatenlogik, Syntax: bildschirm - druck - 4on1
Vorlesung am 20.11.08 (bis Folie 36), Vorlesung am 21.11.08 (ab Folie 37) -
Prädikatenlogik, Semantik: bildschirm - druck - 4on1
Vorlesung am 21.11.08 (bis Folie 30), Vorlesung am 27.11.08 (ab Folie 31) -
Prädikatenlogik, Normalform: bildschirm - druck - 4on1
Vorlesung am 27.11.08 (bis Folie 18), Vorlesung am 05.12.08 (ab Folie 19) -
Prädikatenlogik, Hilbert-Kalkül, Kompaktheitssatz: bildschirm - druck
- 4on1
Vorlesung am 05.12.08 -
Prädikatenlogik, Resolution: bildschirm - druck - 4on1
Vorlesung am 05.12.08 -
Prädikatenlogik, Tableaukalkül: bildschirm - druck - 4on1
Vorlesung am 11.12.08 (bis Folie 12), Vorlesung am 18.12.08 (Folien 13 bis 25 und Folien 38 und 39), Vorlesung am 19.12.08 (Folien 26 bis 37) -
Gleichheitsbehandlung, Reduktionssysteme: bildschirm - druck - 4on1
Vorlesung am 08.01.09 -
Gleichheitsbehandlung, Termersetzung: bildschirm - druck - 4on1
Vorlesung am 08.01.09 -
Prädikatenlogik zweiter Stufe: bildschirm - druck - 4on1
Vorlesung am 15.01.09 -
Modallogik: bildschirm - druck - 4on1
Vorlesung am 15.01.09 (bis Folie 20), Vorlesung am 16.01.09 (ab Folie 21) -
Object Constraint Language: bildschirm - druck - 4on1
Vorlesung am 22.01.09 -
Endliche Automaten (Wiederholung): bildschirm - druck - 4on1
Vorlesung am 30.01.09 -
Büchi-Automaten: bildschirm - druck - 4on1
Vorlesung am 30.01.09 (bis Folie 6), Vorlesung am 05.02.09 (ab Folie 7) -
Lineare Temporale Logik (LTL): bildschirm - druck - 4on1
Vorlesung am 06.02.09 -
Beschreibungssprache PROMELA für Büchi-Automaten: bildschirm - druck - 4on1
Vorlesung am 06.02.09 -
LTL, Übersetzung in Büchi-Automaten: bildschirm - druck - 4on1
Vorlesung am 06.02.09 (bis Folie 8), Vorlesung am 12.02.09 (ab Folie 9) -
LTL, Model Checking: bildschirm - druck - 4on1
Vorlesung am 12.02.09
Übungsblätter
Alle zwei Wochen wird hier ein Übungsblatt bereitgestellt, und zwar immer am Montag derjenigen Wochen, in denen am Freitag eine Übung stattfindet. Die Lösungen werden dann in der Übung am Freitag besprochen.| Übungsblatt |
Ausgabe am |
Besprechung am |
Lösung |
| blatt1.pdf | 26.10.08 | 31.10.08 | loesung1.pdf |
| blatt2.pdf | 10.11.08 | 14.11.08 | loesung2.pdf |
| blatt3.pdf | 24.11.08 | 28.11.08 | loesung3.pdf |
| blatt4.pdf | 02.12.08 | 12.12.08 | loesung4.pdf |
| blatt5.pdf | 08.12.08 | 12.12.08 | loesung5.pdf |
| blatt6.pdf | 16.12.08 | 09.01.09 | loesung6.pdf |
| blatt7.pdf (aufg3.key) | 23.12.08 | 09.01.09 | loesung7.pdf (aufg3.key.proof) |
| blatt8.pdf | 12.01.09 | 23.01.09 | loesung8.pdf |
| blatt9.pdf | 19.01.09 | 23.01.09 | loesung9.pdf |
| blatt10.pdf | 28.01.09 | 13.02.09 | loesung10.pdf |
| blatt11.pdf | 03.02.09 | 13.02.09 | loesung11.pdf |
| blatt12.pdf | 09.02.09 | 13.02.09 | loesung12.pdf |
Die Lösungen müssen nicht abgegeben werden. Das birgt die Gefahr in sich, dass man sich nicht hinreichend mit den Aufgaben beschäftigt, sondern im schlimmsten Falle lediglich in der nächsten Übung die Lösungen unverstanden abschreibt. Das führt nicht zum Erfolg! Bitte lösen Sie die Aufgaben selbständig, am besten in kleinen(!) Lerngruppen von zwei, allenfalls drei Teilnehmern. So sind Sie für die Klausuren gut vorbereitet.
Newsgroup
In der Newsgroup uka.formsys
- werden Ankündigungen und Informationen zu Vorlesung und Übung gepostet,
- können inhaltliche Fragen gestellt werden, die dann in der Newsgroup beantwortet werden.
Skriptum
- skriptum.pdf (in der Version des WS 07/08, diese kann sich im Laufe des Semesters geringfügig ändern)
Sonstiges
KeY-System
Für die zweite Praxisaufgabe wird das KeY-System verwendet, das in der Vorlesung am 19.12.08 vorgestellt wurde. Informationen dazu:
- Webseite des KeY-Projektes: www.key-project.org
- Eine kurze Einführung mit Informationen zur Installation: KeYIntro.pdf
- KeY-Input-Datei mit dem Beispiel aus KeYIntro.pdf: example.key
- KeY-Input-Datei mit Aufgabe 3 des 7. Übungsblattes: blatt7-aufg3.key
- Einige weitere Beispiele (wie in der Vorlesung am 19.12.08 vorgeführt): prop2.key, pred1.key, pred4.key, p17_2.key
Tableau-Applet
Applet zur Visualisierung des Tableaukalküs
Praxisaufgaben
Im Laufe des Semesters werden zwei Praxisaufgaben mit längerer Bearbeitungszeit angeboten. Ihre Bearbeitung gibt Ihnen Gelegenheit, sich mit Implementierungen formaler Verfahren vertraut zu machen.
| Aufgabenstellung |
Ausgabe am |
Abgabe bis zum |
|
| Praxisaufgabe 1 | 15.11.08 | 31.12.08 (zur Abgabe: LOGIN) | Beispiellösung |
| Praxisaufgabe 2 (dazu: list.key) | 15.01.09 | 15.02.09 (zur Abgabe: LOGIN) |
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 1,5 Bonuspunkte vergeben (s.u.).
Erfolgskontrolle und Notenvergabe
Abschlussklausur
Die Endnote (Modulnote) ist die Note der Abschlussklausur unter Berücksichtigung der für die Zwischenklausuren und Praxisaufgaben vergebenen Bonuspunkte (s.u.).
Die 1. Abschlussklausur (Hauptklausur) findet am Donnerstag, dem 19.02.2009, 9:00 Uhr, statt.
Die 2. Abschlussklausur (Nachklausur) findet am Mittwoch, dem 08.04.2009, 10:00 Uhr, statt.
Die Anmeldung zu den Abschlussklausuren erfolgt über das QISPOS-Studierendenportal (für die Diplomstudiengänge) bzw. blaue Scheine (für die Bachelor-/Master-Studiengänge). Zur Hauptklausur kann man sich vom 19.01.09 bis zum 15.02.09 anmelden; zur Nachklausur vom 01.03.09 bis zum 01.04.09.
Aufgaben und Musterlösungen
| Abschlussklausur am |
Aufgabenstellung |
Musterlösung |
|
| 19.02.09 | Aufgaben | Lösungen | |
| 08.04.09 | Aufgaben | Lösungen |
Zwischenklausuren
Im Laufe des Semesters werden zwei Zwischenklausuren angeboten. Die Teilnahme daran ist freiwillig. Bei erfolgreicher Teilnahme werden pro Zwischenklausur bis zu drei Bonuspunkte für die Abschlussklausur vergeben (s.u.).
Aufgaben und Musterlösungen
| Zwischenklausur am |
Aufgabenstellung |
Musterlösung |
|
| 04.12.08 | Aufgaben | Lösungen | |
| 29.01.09 | Aufgaben | Lösungen |
Termine und Anmeldung
Die erste Zwischenklausur findet am Donnerstag, dem 04.12.2008, 14:00 Uhr, im Gaede-Hörsaal statt. Die Anmeldung zur 1. Zwischenklausur erfolgt vom 18.11. bis zum 30.11.2008. In diesem Zeitraum können Sie sich an- und auch wieder abmelden. Nur angemeldete Teilnehmer können an der Zwischenklausur teilnehmen.
Die zweite Zwischenklausur findet am Donnerstag, dem 29.01.09, 14:00 Uhr, im Gaede-Hörsaal statt. Die Anmeldung zur 2. Zwischenklausur erfolgt vom 08.01. bis zum 26.01.2009. In diesem Zeitraum können Sie sich an- und auch wieder abmelden. Nur angemeldete Teilnehmer können an der Zwischenklausur teilnehmen.
Anmeldung hier: LOGIN (beim ersten Login Registrierung mit der Matrikelnummer).
Hinweise zur Durchführung der Zwischenklausuren
- Uhrzeit und Dauer: Die Klausur wird in zwei Gruppen geschrieben. Die erste Gruppe beginnt um 14:00 Uhr und die zweite Gruppe um 14:45. Die Bearbeitungszeit beträgt jeweils 30 Minuten (plus 5 Minuten Einlesezeit).
- Gruppeneinteilung: In welcher Gruppe Sie sind, entnehmen Sie bitte der Liste, die nach Anmeldeschluss hier auf der Webseite zur Verfügung steht und zudem an alle, die angemeldet sind, per Email verschickt wird. Alle, die sich angemeldet haben, werden zufällig auf die beiden Gruppen verteilt.
- 1. Gruppe: Finden Sie sich bitte pünktlich um 14:00 Uhr im Hörsaal ein. Nach Ausgabe der Klausur darf niemand vorzeitig abgeben. Nach Ende der Klausur verlassen alle zusammen um 14:45 den Hörsaal durch den unteren Ausgang neben der Bühne (der ins 1. OG des Gebäudes führt).
- 2. Gruppe: Finden Sie sich bitte pünktlich um 14:40 Uhr vor dem Hörsaal im 2. OG des Gebäudes ein. Nachdem die 1. Gruppe den Hörsaal verlassen hat, betreten alle zusammen den Saal durch die oberen Türen. Wer zu spät kommt, wird nicht mehr zur Klausur zugelassen, da er oder sie jemandem aus der 1. Gruppe begegnet sein könnte.
- Aus Fairness-Gründen gilt die Regel, dass, wer zu spät kommt, nicht mehr zugelassen wird, für beide Gruppen gleichermaßen.
- Es sind keine Hilfsmittel zugelassen.
- Bringen Sie bitte Ihren Studierendenausweis mit.
Bonuspunkte
Für die erfolgreiche Teilnahme an den beiden Zwischenklausuren werden jeweils bis zu drei Bonuspunkte und für die erfolgreiche Bearbeitung der beiden Praxisaufgaben jeweils bis zu 1,5 Bonuspunkte vergeben.
Diese Bonuspunkte werden bei der Abschlussklausur zur Notenverbesserung angerechnet. Sie können allerdings nur zur Notenverbesserung eingesetzt werden, wenn die Abschlussklausur auch ohne sie schon bestanden wäre. Das heißt, es ist nicht möglich, eine nicht bestandene Abschlussklausur mit Hilfe der Bonuspunkte zu bestehen.
Termine
Vorlesung/Übung
- Donnerstags, 14:00 - 15:30 Uhr, Gaede-Hörsaal (Geb. 30.22, Raum 130.1)
- Freitags, 11:30 - 13:00 Uhr, Gaede-Hörsaal (Geb. 30.22, Raum 130.1)
Abschlussklausuren
- Anmeldung zur 1. Abschlussklausur: 19.01.09 bis 15.02.09 üer das QISPOS-Studierendenportal
- 1. Abschlussklausur (Hauptklausur): Donnerstag, 19.02.2009, 9:00 Uhr, Gerthsen/HSaF/Audi
- Einsicht 1. Abschlussklausur: Freitag, 13.03.09 ab 15.30 Uhr, Seminarraum 301
- Anmeldung zur 2. Abschlussklausur: 01.03.09 bis 01.04.09 über das QISPOS-Studierendenportal
- 2. Abschlussklausur (Nachklausur): Mittwoch, 08.04.2009, 10:00 Uhr, HSaF/Audi
Zwischenklausuren
- Anmeldung zur 1. Zwischenklausur: 18.11. bis 30.11.2008 über diese Webseite
- 1. Zwischenklausur: Donnerstag, 04.12.08, 14:00 Uhr, Gaede
- Anmeldung zur 2. Zwischenklausur: 08.01. bis 26.01.2009 über diese Webseite
- 2. Zwischenklausur: Donnerstag, 29.01.09, 14:00 Uhr, Gaede
- Einsicht: Donnerstag, 12.02.09, 16 Uhr (Gruppe 1) bzw. 17 Uhr (Gruppe 2), SR131
Gruppe 1: alle, die bei der erste Zwischenklausur in der 1. Gruppe mitgeschrieben haben;
Gruppe 2: alle anderen
Praxisaufgaben
- Abgabe der 1. Praxisaufgabe bis: 31.12.2008
- Abgabe der 2. Praxisaufgabe bis: 15.02.2009
Inhaltsübersicht
- Aussagenlogik
- Syntax und Semantik
- Kalküe
- Anwendungen
- Prädikatenlogik
- Syntax und Semantik
- Kalküle
- Anwendungen
- Gleichheit
- Object Constraint Language (OCL)
- Modale Aussagenlogik
- Temporale Logik (LTL)
- Endliche Automaten (Wiederholung)
- Büchi Automaten
- Modellprüfung