HOME | IMPRESSUM | DATENSCHUTZ | SITEMAP | KIT

Formale Systeme

Diese Vorlesung wurde in den letzten Jahren mit dem Fakultätslehrpreis ausgezeichnet. Evaluationsergebnisse der letzten Veranstaltung finden sie hier

Vorlesung im Wintersemester 2010/2011

Prof. Dr. Bernhard Beckert (BB)
Thorsten Bormer (TB)


Zielgruppe: Diplom Informatik, Bachelor Informatik, Master Informatik
Umfang: 4 SWS / 6 Leistungspunkte
Ort: Gaede-Hörsaal (Geb. 30.22, Raum 130.1)
Zeit: Donnerstag, 14:00-15:30 und Freitag, 11:30-13:00
Erstmals: 21.10.10
LVNr.:: 24078
Mehr Informationen zu den Inhalten: aus dem Vorlesungsverzeichnis

Aktuelles

21.04.11: Die vorläufigen Klausurergebnisse zur Nachklausur sind online. Die Klausureinsicht findet am Mittwoch, dem 27.04. ab 15:45 Uhr in SR131 (Geb. 50.34) statt.
04.04.11: Die Klausur am 08.04.2011 (ab 14:00 Uhr) findet für alle Teilnehmer im Audimax statt.
14.03.11: Die Musterlösung der Klausur vom 17.02.2011 steht zur Verfügung.
14.03.11: Die Klausureinsicht findet am Dienstag, dem 15.03. in Raum SR236 (Geb. 50.34) in zwei Gruppen statt. Aufteilung der Gruppen nach dem ersten Buchstaben des Nachnamens: Gruppe 1: A-K ab 16:00 Uhr; Gruppe 2: L-Z ab 17:00 Uhr.
03.03.11: Die Anmeldung zur Nachklausur ist bis zum 03.04. im Studierendenportal des KIT möglich.
03.03.11: Die vorläufigen Klausurergebnisse zur Hauptklausur sind online. Die Klausureinsicht findet am Dienstag, dem 15.03. ab 16:00 Uhr statt. Der Raum wird noch bekannt gegeben.
16.02.11: Die fehlenden Bewertungen der 1. Praxisaufgabe sind nun in der Datenbank eingetragen und können im LOGIN-Bereich abgerufen werden.
16.02.11: Die Bewertungen der beiden Praxisaufgaben stehen im LOGIN-Bereich zur Verfügung.
16.02.11: Hörsaalverteilung für die Hauptklausur am 17.02.: Alle Teilnehmer schreiben im Gerthsen-Hörsaal
10.02.11: Die Musterlösung des 2. Zwischentests steht zur Verfügung.
07.02.11: Das 12. Übungsblatt steht zur Verfügung. Es wird in der Übung am 11.02.11 besprochen.
04.02.11: Die Einsicht in beide Zwischentests findet am Donnerstag, 10.02.11 in SR301 um 16 Uhr (Gruppe 1) bzw. 17 Uhr (Gruppe 2) statt. Gruppe 1: alle, die bei dem ersten Zwischentest in der Gruppe A mitgeschrieben haben; Gruppe 2: alle anderen.
25.01.11: Die Gruppenzuordnung zum 2. Zwischentest, sowie einige Hinweise zum Ablauf des Zwischentests stehen zur Verfügung.
25.01.11: Das 11. Übungsblatt steht zur Verfügung. Es wird in der Übung am 11.02.11 besprochen.
17.01.11: Die Anmeldung zur Hauptklausur ist ab sofort im Studierendenportal des KIT bis zum 13.02.11 möglich.
17.01.11: Das 10. Übungsblatt steht zur Verfügung. Es wird in der Übung am 21.01.11 besprochen.
10.01.11: Der Veranstaltungsplan hat sich geändert: die Vorlesung am 28.01.2011 findet nicht statt; die für den 04.02. vorgesehene Übung wird nun am 11.02. abgehalten.
10.01.11: Die 2. Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 06.02.11 im LOGIN-Bereich abgegeben werden.
10.01.11: Die Anmeldung zum 2. Zwischentest ist freigeschaltet. Anmeldefrist ist der 24.01.2010
10.01.11: Das 9. Übungsblatt steht zur Verfügung. Es wird in der Übung am 21.01.11 besprochen.
28.12.10: Die Lösungen des 7. und 8. Übungsblatts stehen zur Verfügung.
27.12.10: Die Ergebnisse des 1. Zwischentests stehen ab sofort im LOGIN Bereich zur Verfügung.
20.12.10: Das 8. Übungsblatt steht zur Verfügung. Es wird in der Übung am 23.12.10 besprochen.
15.12.10: Die Lösung des 6. Übungsblatts, sowie die Musterlösung des 1. Zwischentests stehen zur Verfügung.
13.12.10: Update des satromino Rahmenwerks (v1.0.1): Fehler in den Methoden FigureJ.rotationLeft und FigureL.rotationLeft in Figures.java behoben.
08.12.10: Die Gruppenzuordnung zum 1. Zwischentest steht zur Verfügung. Update: einige Hinweise zum Ablauf der Klausur.
07.12.10: Das 7. Übungsblatt steht zur Verfügung. Es wird in der Übung am 23.12.10 besprochen.
02.12.10: Korrektur: Im 6. Aufgabenblatt war ein Fehler im Hoare-Tripel in Aufgabe 4. Dieser ist nun korrigiert.
29.11.10: Die 1. Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 02.01.11 abgegeben werden. Die Webseite dafür wird bald freigeschaltet.
29.11.10: Das 6. Übungsblatt steht zur Verfügung. Es wird in der Übung am 10.12.10 besprochen.
26.11.10: Die Anmeldung zum 1. Zwischentest ist freigeschaltet. Anmeldefrist ist der 05.12.2010
22.11.10: Das 5. Übungsblatt steht zur Verfügung. Es wird in der Übung am 26.11.10 besprochen.
15.11.10: Das 4. Übungsblatt steht zur Verfügung. Es wird in der Übung am 26.11.10 besprochen.
15.11.10: Die Lösungen des 2. und 3. Übungsblatts stehen zur Verfügung.
08.11.10: Das 3. Übungsblatt steht zur Verfügung. Es wird in der Übung am 12.11.10 besprochen.
01.11.10: Das 2. Übungsblatt steht zur Verfügung. Es wird in der Übung am 12.11.10 besprochen.
29.10.10: Die Lösungen des 1. Übungsblatts stehen zur Verfügung.
29.10.10: Termine der Abschlussklausuren stehen fest. Der Beginn der Nachklausur ist nun Freitag, der 08.04.11 um 14:00 Uhr.
27.10.10: Die Termine für die Zwischentests sind Donnerstag, 09.12.2010 und Donnerstag, 27.01.2011.
25.10.10: Das 1. Übungsblatt steht zur Verfügung. Es wird in der Übung am 29.10.10 besprochen.
18.10.10: Die Termine für die Abschlussklausuren sind Donnerstag, der 17.02.11 (Hauptklausur), und Freitag, der 08.04.11 (Nachklausur).
14.10.10: Webseite angelegt.

Materialien

Vorlesungsfolien

Die Vorlesungsfolien werden hier jeweils nach der Vorlesung zur Verfügung gestellt.
  1. Organisatorisches: bildschirm - druck
    Vorlesung am 21.10.10
  2. Aussagenlogik, Syntax und Semantik: bildschirm - druck
    Vorlesungen am 21.10.10 (Folien 1-21) und 22.10.10 (Folien 22-24)
  3. Aussagenlogik, Normalformen: bildschirm - druck
    Vorlesung am 22.10.10
  4. Binary Decision Diagrams: bildschirm - druck
    Vorlesung am 22.10.10 (Folien 1-26), Vorlesung am 28.10.10 (Folien 27-28)
  5. Aussagenlogik, Erfüllbarkeitsproblem spezieller Formelklassen: bildschirm - druck
    Vorlesung am 28.10.10
  6. Hilbert-Kalkül: bildschirm - druck
    Vorlesung am 28.10.10
  7. Aussagenlogik, Resolution: bildschirm - druck
    Vorlesung am 04.11.10
  8. Aussagenlogik, Tableaukalkül: bildschirm - druck
    Vorlesung am 05.11.10 (bis Folie 16), Vorlesung am 11.11.10 (ab Folie 17)
  9. Aussagenlogik, Sequenzenkalkül: bildschirm - druck
    Vorlesung am 11.11.10
  10. Aussagenlogik, Sonstige Kalküle: bildschirm - druck
    Vorlesung am 18.11.10
  11. Prädikatenlogik, Syntax: bildschirm - druck
    Vorlesung am 18.11.10 (bis Folie 12), Vorlesung am 19.11.10 (ab Folie 13)
  12. Prädikatenlogik, Semantik: bildschirm - druck
    Vorlesung am 25.11.10 (bis Folie 38), Vorlesung am 02.12.10 (ab Folien 39)
  13. Prädikatenlogik, Normalformen: bildschirm - druck
    Vorlesung am 02.12.10
  14. Prädikatenlogik, Kompaktheitssatz: bildschirm - druck
    Vorlesung am 02.12.10
  15. Prädikatenlogik, Resolution: bildschirm - druck
    Vorlesung am 03.12.10 (bis Folie 14), Vorlesung am 16.12.10 (ab Folie 15)
  16. Prädikatenlogik, Tableaukalkül: bildschirm - druck
    Vorlesung am 16.12.10 (Folien 1 bis 11 und 36 bis 38), Vorlesung am 17.12.10 (Folien 12 bis 35)
  17. Prädikatenlogik, Sequenzenkül: bildschirm - druck
    Vorlesung am 17.12.10
  18. Reduktionssysteme: bildschirm - druck
    Vorlesung am 07.01.11
  19. Termersetzungssysteme: bildschirm - druck
    Vorlesung am 07.01.11
  20. Prädikatenlogik 2. Stufe: bildschirm - druck
    Vorlesung am 13.01.11
  21. Modallogik: bildschirm - druck
    Vorlesung am 13.01.11 (Folien 1 bis 23), Vorlesung am 14.01.11 (Folien 24 bis 39)
  22. Object Constraint Language: bildschirm - druck
    Vorlesung am 20.01.11
  23. Endliche Automaten (Wiederholung): bildschirm - druck
  24. Büchi-Automaten: bildschirm - druck
    Vorlesung am 03.02.11 (Folien 1 bis 11), Vorlesung am 04.02.11 (Folien 12 bis 22)
  25. Die Beschreibungssprache PROMELA für Büchi-Automaten: bildschirm - druck
    Vorlesung am 04.02.11
  26. Lineare Temporale Logik (LTL): bildschirm - druck
    Vorlesung am 04.02.11
  27. LTL, Übersetzung in Büchi-Automaten: bildschirm - druck
    Vorlesung am 04.02.11 (Folien 1-7), Vorlesung am 10.02.11 (Folien 8-14)
  28. LTL, Model Checking: bildschirm - druck
    Vorlesung am 10.02.11

Übungsblätter

Jeden Montag wird hier ein Übungsblatt bereitgestellt. Die Lösungen zu jeweils zwei Blaettern werden dann alle zwei Wochen in der Übung am Freitag besprochen.

Übungsblatt
Ausgabe am
Besprechung am
Lösung
blatt1.pdf 25.10.10 29.10.10 loesung1.pdf
blatt2.pdf 01.11.10 12.11.10 loesung2.pdf
blatt3.pdf 08.11.10 12.11.10 loesung3.pdf
blatt4.pdf 15.11.10 26.11.10 loesung4.pdf
blatt5.pdf 22.11.10 26.11.10 loesung5.pdf
blatt6.pdf 29.11.10 10.12.10 loesung6.pdf
blatt7.pdf 07.12.10 23.12.10 loesung7.pdf
blatt8.pdf 20.12.10 23.12.10 loesung8.pdf
blatt9.pdf, blatt9-aufg2.key, KeYIntro.pdf 10.01.11 21.01.11 loesung9.pdf, blatt9-aufg2.key.proof
blatt10.pdf 17.01.11 21.01.11 loesung10.pdf
blatt11.pdf 25.01.11 11.02.11 loesung11.pdf
blatt12.pdf 07.02.11 11.02.11 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.


Twitter

Über den Twitter-Benutzer @formaleSysteme werden Ankündigungen und Informationen zu Vorlesung und Übung gepostet.
(Diese Informationen befinden sich aber auch weiterhin auf dieser Website.)

Inhaltliche Fragen zur Vorlesung können als Tweet unter Angabe des Hashtags #FSysKIT gestellt werden; ebenso sind Rückmeldungen während der Vorlesung (als "Backchannel") erwünscht.

Skriptum

  • skriptum.pdf (in der Version des WS 07/08, diese kann sich im Laufe des Semesters geringfügig ändern)


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
Bemerkungen
praxis1.pdf / satrominoSrc-1.0.1.zip / minisat2-070721.zip 29.11.10 02.01.11
praxis2.pdf / removeDuplicates.key / KeYIntro.pdf 10.01.11 06.02.11

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

Abschlussklausuren

Die Endnote (Modulnote) ist die Note der Abschlussklausur unter Berücksichtigung der für die Zwischentests und Praxisaufgaben vergebenen Bonuspunkte (s.u.).

Zwischentests

Im Laufe des Semesters werden zwei Zwischentests angeboten. Die Teilnahme daran ist freiwillig. Bei erfolgreicher Teilnahme werden pro Zwischentest bis zu drei Bonuspunkte für die Abschlussklausur vergeben (s.u.).

Aufgaben und Musterlösungen

Zwischentest am
Aufgabenstellung
Musterlösung
09.12.2010 Aufgaben Lösungen
27.01.2011 Aufgaben Lösungen

Klausur am
Aufgabenstellung
Musterlösung
17.02.2011 Aufgaben Lösungen
08.04.2011 Aufgaben Lösungen

An- und Abmeldung zu den Zwischentests

Die An-/Abmeldung zum 2. Zwischentest kann im LOGIN-Bereich vorgenommen werden. An-/Abmeldefrist ist der 24.01.2011.

Bonuspunkte

Für die erfolgreiche Teilnahme an den beiden Zwischentests 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

Abschlussklausuren

  • 1. Abschlussklausur (Hauptklausur): Donnerstag, 17.02.2011, 11:00 Uhr, Gerthsen-Hösaal
  • 2. Abschlussklausur (Nachklausur): Freitag, 08.04.2011, 14:00 Uhr, Audimax

Zwischentests

  • 1. Zwischentest: Donnerstag, 09.12.2010
  • 2. Zwischentest: Donnerstag, 27.01.2011

Veranstaltungsplan


Datum
Art der Veranstaltung
21.10.2010
Vorlesung
22.10.2010
Vorlesung
28.10.2010
Vorlesung
29.10.2010 Übung
04.11.2010
Vorlesung
05.11.2010 Vorlesung
11.11.2010 Vorlesung
12.11.2010 Übung
18.11.2010 Vorlesung
19.11.2010 Vorlesung
25.11.2010 Vorlesung
26.11.2010 Übung
02.12.2010
Vorlesung
03.12.2010 Vorlesung
09.12.2010
1. Zwischentest
10.12.2010
Übung
16.12.2010 Vorlesung
17.12.2010 Vorlesung
23.12.2010 Übung
24.12.2010-06.01.2011
Vorlesungsfreie Zeit
07.01.2011
Vorlesung
13.01.2011 Vorlesung
14.01.2011 Vorlesung
20.01.2011 Vorlesung
21.01.2011 Übung
27.01.2011 2. Zwischentest
28.01.2011 fällt aus
03.02.2011
Vorlesung
04.02.2011 Vorlesung
10.02.2011 Vorlesung
11.02.2011 Übung
17.02.2011
Hauptklausur



Inhaltsübersicht

  • Aussagenlogik
    • Syntax und Semantik
    • Kalküle
    • 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


Link zur Webseite des vorigen Jahres


Bernhard Beckert