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 Verüfung.
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.rz.uni-karlsruhe.de (nicht news.ira.uka.de).
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

  1. Einführung (Organisatorischen, Inhaltsübersicht, Literatur): bildschirm - druck - 4on1
    Vorlesung am 23.10.08
  2. Aussagenlogik, Syntax und Semantik: bildschirm - druck - 4on1
    Vorlesung am 23.10.08
  3. Aussagenlogik, konjuntive Normalform: bildschirm - druck - 4on1
    Vorlesung am 23.10.08
  4. Binary Decision Diagrams (BDDs): bildschirm - druck - 4on1
    Vorlesung am 24.10.08
  5. Aussagenlogik, Erfüllbarkeitsproblem für spezielle Formelklassen: bildschirm - druck - 4on1
    Vorlesung am 30.10.08
  6. Aussagenlogik, Hilbert-Kalkül: bildschirm - druck - 4on1
    Vorlesung am 30.10.08 (bis Folie 8), Vorlesung am 06.11.08 (ab Folie 9)
  7. Aussagenlogik, Resolution: bildschirm - druck - 4on1
    Vorlesung am 06.11.08 (bis Folie 9), Vorlesung am 07.11.08 (ab Folie 10)
  8. Aussagenlogik, Tableaukalkül: bildschirm - druck - 4on1
    Vorlesung am 07.11.08
  9. Aussagenlogik, Sequenzenkalkül: bildschirm - druck - 4on1
    Vorlesung am 13.11.08
  10. Aussagenlogik, sonstige Kalküle: bildschirm - druck - 4on1
    Vorlesung am 13.11.08
  11. Prädikatenlogik, Syntax: bildschirm - druck - 4on1
    Vorlesung am 20.11.08 (bis Folie 36), Vorlesung am 21.11.08 (ab Folie 37)
  12. Prädikatenlogik, Semantik: bildschirm - druck - 4on1
    Vorlesung am 21.11.08 (bis Folie 30), Vorlesung am 27.11.08 (ab Folie 31)
  13. Prädikatenlogik, Normalform: bildschirm - druck - 4on1
    Vorlesung am 27.11.08 (bis Folie 18), Vorlesung am 05.12.08 (ab Folie 19)
  14. Prädikatenlogik, Hilbert-Kalkül, Kompaktheitssatz: bildschirm - druck - 4on1
    Vorlesung am 05.12.08
  15. Prädikatenlogik, Resolution: bildschirm - druck - 4on1
    Vorlesung am 05.12.08
  16. 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)
  17. Gleichheitsbehandlung, Reduktionssysteme: bildschirm - druck - 4on1
    Vorlesung am 08.01.09
  18. Gleichheitsbehandlung, Termersetzung: bildschirm - druck - 4on1
    Vorlesung am 08.01.09
  19. Prädikatenlogik zweiter Stufe: bildschirm - druck - 4on1
    Vorlesung am 15.01.09
  20. Modallogik: bildschirm - druck - 4on1
    Vorlesung am 15.01.09 (bis Folie 20), Vorlesung am 16.01.09 (ab Folie 21)
  21. Object Constraint Language: bildschirm - druck - 4on1
    Vorlesung am 22.01.09
  22. Endliche Automaten (Wiederholung): bildschirm - druck - 4on1
    Vorlesung am 30.01.09
  23. Büchi-Automaten: bildschirm - druck - 4on1
    Vorlesung am 30.01.09 (bis Folie 6), Vorlesung am 05.02.09 (ab Folie 7)
  24. Lineare Temporale Logik (LTL): bildschirm - druck - 4on1
    Vorlesung am 06.02.09
  25. Beschreibungssprache PROMELA für Büchi-Automaten: bildschirm - druck - 4on1
    Vorlesung am 06.02.09
  26. 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)
  27. 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

Skriptum

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:

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-Studentenportal (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

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 werden 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

Abschlussklausuren

Zwischenklausuren

Praxisaufgaben


Inhaltsübersicht


Bernhard Beckert