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.2010
LVNr.::	24078
Mehr Informationen zu den Inhalten:	aus dem Vorlesungsverzeichnis

Aktuelles

21.04.2011: 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.2011: Die Klausur am 08.04.2011 (ab 14:00 Uhr) findet für alle Teilnehmer im Audimax statt.
14.03.2011: Die Musterlösung der Klausur vom 17.02.2011 steht zur Verfügung.
14.03.2011: 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.2011: Die Anmeldung zur Nachklausur ist bis zum 03.04. im Studierendenportal des KIT möglich.
03.03.2011: 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.2011: Die fehlenden Bewertungen der 1. Praxisaufgabe sind nun in der Datenbank eingetragen und können im LOGIN-Bereich abgerufen werden.
16.02.2011: Die Bewertungen der beiden Praxisaufgaben stehen im LOGIN-Bereich zur Verfügung.
16.02.2011: Hörsaalverteilung für die Hauptklausur am 17.02.: Alle Teilnehmer schreiben im Gerthsen-Hörsaal
10.02.2011: Die Musterlösung des 2. Zwischentests steht zur Verfügung.
07.02.2011: Das 12. Übungsblatt steht zur Verfügung. Es wird in der Übung am 11.02.2011 besprochen.
04.02.2011: Die Einsicht in beide Zwischentests findet am Donnerstag, 10.02.2011 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.2011: Die Gruppenzuordnung zum 2. Zwischentest, sowie einige Hinweise zum Ablauf des Zwischentests stehen zur Verfügung.
25.01.2011: Das 11. Übungsblatt steht zur Verfügung. Es wird in der Übung am 11.02.2011 besprochen.
17.01.2011: Die Anmeldung zur Hauptklausur ist ab sofort im Studierendenportal des KIT bis zum 13.02.2011 möglich.
17.01.2011: Das 10. Übungsblatt steht zur Verfügung. Es wird in der Übung am 21.01.2011 besprochen.
10.01.2011: 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.2011: Die 2. Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 06.02.2011 im LOGIN-Bereich abgegeben werden.
10.01.2011: Die Anmeldung zum 2. Zwischentest ist freigeschaltet. Anmeldefrist ist der 24.01.2010
10.01.2011: Das 9. Übungsblatt steht zur Verfügung. Es wird in der Übung am 21.01.2011 besprochen.
28.12.2010: Die Lösungen des 7. und 8. Übungsblatts stehen zur Verfügung.
27.12.2010: Die Ergebnisse des 1. Zwischentests stehen ab sofort im LOGIN Bereich zur Verfügung.
20.12.2010: Das 8. Übungsblatt steht zur Verfügung. Es wird in der Übung am 23.12.2010 besprochen.
15.12.2010: Die Lösung des 6. Übungsblatts, sowie die Musterlösung des 1. Zwischentests stehen zur Verfügung.
13.12.2010: Update des satromino Rahmenwerks (v1.0.1): Fehler in den Methoden FigureJ.rotationLeft und FigureL.rotationLeft in Figures.java behoben.
08.12.2010: Die Gruppenzuordnung zum 1. Zwischentest steht zur Verfügung. Update: einige Hinweise zum Ablauf der Klausur.
07.12.2010: Das 7. Übungsblatt steht zur Verfügung. Es wird in der Übung am 23.12.2010 besprochen.
02.12.2010: Korrektur: Im 6. Aufgabenblatt war ein Fehler im Hoare-Tripel in Aufgabe 4. Dieser ist nun korrigiert.
29.11.2010: Die 1. Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 02.01.2011 abgegeben werden. Die Webseite dafür wird bald freigeschaltet.
29.11.2010: Das 6. Übungsblatt steht zur Verfügung. Es wird in der Übung am 10.12.2010 besprochen.
26.11.2010: Die Anmeldung zum 1. Zwischentest ist freigeschaltet. Anmeldefrist ist der 05.12.2010
22.11.2010: Das 5. Übungsblatt steht zur Verfügung. Es wird in der Übung am 26.11.2010 besprochen.
15.11.2010: Das 4. Übungsblatt steht zur Verfügung. Es wird in der Übung am 26.11.2010 besprochen.
15.11.2010: Die Lösungen des 2. und 3. Übungsblatts stehen zur Verfügung.
08.11.2010: Das 3. Übungsblatt steht zur Verfügung. Es wird in der Übung am 12.11.2010 besprochen.
01.11.2010: Das 2. Übungsblatt steht zur Verfügung. Es wird in der Übung am 12.11.2010 besprochen.
29.10.2010: Die Lösungen des 1. Übungsblatts stehen zur Verfügung.
29.10.2010: Termine der Abschlussklausuren stehen fest. Der Beginn der Nachklausur ist nun Freitag, der 08.04.2011 um 14:00 Uhr.
27.10.2010: Die Termine für die Zwischentests sind Donnerstag, 09.12.2010 und Donnerstag, 27.01.2011.
25.10.2010: Das 1. Übungsblatt steht zur Verfügung. Es wird in der Übung am 29.10.2010 besprochen.
18.10.2010: Die Termine für die Abschlussklausuren sind Donnerstag, der 17.02.2011 (Hauptklausur), und Freitag, der 08.04.2011 (Nachklausur).
14.10.2010: Webseite angelegt.

Materialien

Vorlesungsfolien

Die Vorlesungsfolien werden hier jeweils nach der Vorlesung zur Verfügung gestellt.

1. Organisatorisches: bildschirm - druck
   Vorlesung am 21.10.2010
2. Aussagenlogik, Syntax und Semantik: bildschirm - druck
   Vorlesungen am 21.10.2010 (Folien 1-21) und 22.10.2010 (Folien 22-24)
3. Aussagenlogik, Normalformen: bildschirm - druck
   Vorlesung am 22.10.2010
4. Binary Decision Diagrams: bildschirm - druck
   Vorlesung am 22.10.2010 (Folien 1-26), Vorlesung am 28.10.2010 (Folien 27-28)
5. Aussagenlogik, Erfüllbarkeitsproblem spezieller Formelklassen: bildschirm - druck
   Vorlesung am 28.10.2010
6. Hilbert-Kalkül: bildschirm - druck
   Vorlesung am 28.10.2010
7. Aussagenlogik, Resolution: bildschirm - druck
   Vorlesung am 04.11.2010
8. Aussagenlogik, Tableaukalkül: bildschirm - druck
   Vorlesung am 05.11.2010 (bis Folie 16), Vorlesung am 11.11.2010 (ab Folie 17)
9. Aussagenlogik, Sequenzenkalkül: bildschirm - druck
   Vorlesung am 11.11.2010
10. Aussagenlogik, Sonstige Kalküle: bildschirm - druck
    Vorlesung am 18.11.2010
11. Prädikatenlogik, Syntax: bildschirm - druck
    Vorlesung am 18.11.2010 (bis Folie 12), Vorlesung am 19.11.2010 (ab Folie 13)
12. Prädikatenlogik, Semantik: bildschirm - druck
    Vorlesung am 25.11.2010 (bis Folie 38), Vorlesung am 02.12.2010 (ab Folien 39)
13. Prädikatenlogik, Normalformen: bildschirm - druck
    Vorlesung am 02.12.2010
14. Prädikatenlogik, Kompaktheitssatz: bildschirm - druck
    Vorlesung am 02.12.2010
15. Prädikatenlogik, Resolution: bildschirm - druck
    Vorlesung am 03.12.2010 (bis Folie 14), Vorlesung am 16.12.2010 (ab Folie 15)
16. Prädikatenlogik, Tableaukalkül: bildschirm - druck
    Vorlesung am 16.12.2010 (Folien 1 bis 11 und 36 bis 38), Vorlesung am 17.12.2010 (Folien 12 bis 35)
17. Prädikatenlogik, Sequenzenkül: bildschirm - druck
    Vorlesung am 17.12.2010
18. Reduktionssysteme: bildschirm - druck
    Vorlesung am 07.01.2011
19. Termersetzungssysteme: bildschirm - druck
    Vorlesung am 07.01.2011
20. Prädikatenlogik 2. Stufe: bildschirm - druck
    Vorlesung am 13.01.2011
21. Modallogik: bildschirm - druck
    Vorlesung am 13.01.2011 (Folien 1 bis 23), Vorlesung am 14.01.2011 (Folien 24 bis 39)
22. Object Constraint Language: bildschirm - druck
    Vorlesung am 20.01.2011
23. Endliche Automaten (Wiederholung): bildschirm - druck
    
24. Büchi-Automaten: bildschirm - druck
    Vorlesung am 03.02.2011 (Folien 1 bis 11), Vorlesung am 04.02.2011 (Folien 12 bis 22)
25. Die Beschreibungssprache PROMELA für Büchi-Automaten: bildschirm - druck
    Vorlesung am 04.02.2011
26. Lineare Temporale Logik (LTL): bildschirm - druck
    Vorlesung am 04.02.2011
27. LTL, Übersetzung in Büchi-Automaten: bildschirm - druck
    Vorlesung am 04.02.2011 (Folien 1-7), Vorlesung am 10.02.2011 (Folien 8-14)
28. LTL, Model Checking: bildschirm - druck
    Vorlesung am 10.02.2011

Ü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.2010	29.10.2010	loesung1.pdf
blatt2.pdf	01.11.2010	12.11.2010	loesung2.pdf
blatt3.pdf	08.11.2010	12.11.2010	loesung3.pdf
blatt4.pdf	15.11.2010	26.11.2010	loesung4.pdf
blatt5.pdf	22.11.2010	26.11.2010	loesung5.pdf
blatt6.pdf	29.11.2010	10.12.2010	loesung6.pdf
blatt7.pdf	07.12.2010	23.12.2010	loesung7.pdf
blatt8.pdf	20.12.2010	23.12.2010	loesung8.pdf
blatt9.pdf, blatt9-aufg2.key, KeYIntro.pdf	10.01.2011	21.01.2011	loesung9.pdf, blatt9-aufg2.key.proof
blatt10.pdf	17.01.2011	21.01.2011	loesung10.pdf
blatt11.pdf	25.01.2011	11.02.2011	loesung11.pdf
blatt12.pdf	07.02.2011	11.02.2011	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.2010	02.01.2011
praxis2.pdf / removeDuplicates.key / KeYIntro.pdf	10.01.2011	06.02.2011

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