Formale Systeme

Wahlpflichtvorlesung/Stammmodul im Wintersemester 2011/2012

Prof. Dr. Peter H. Schmitt
David Farago, Christoph Scheben, Mattias Ulbrich


Forum http://i12www.ira.uka.de/~farago/fsforum

Aktuelles

Datum: Nachricht
02.05.2012: Die Ergebnisse der Nachklausur sind jetzt verfügbar.
26.04.2012: Die Einsicht der Klausur vom 12.04 findet am 07. Mai von 11:30 bis 12:30 Uhr im Seminarraum 301 im Informatikgebäude (50.34) statt.
11.04.2012: Zur Seite der Klausur: Bitte stellen Sie sicher, dass Sie angemeldet sind.
04.04.2012: Die Nachklausur findet am 12.4. um 14.00 Uhr im Hertzhörsaal statt.
29.03.2012: Die Freischaltung der Anmeldung für die Klausur am 12.04. erfolgte Anfang des Monats. Die Anmeldefrist endete am 5. April.
28.02.2012: Die Einsicht der Klausur vom 14.02 findet am 08. März von 10 bis 12 Uhr im Seminarraum 301 im Informatikgebäude (50.34) statt. Die Ergebnisse wurden im EG des Informatikgebäudes ausgehängt.
10.02.2012: Zur Seite der Klausur: Bitte stellen Sie sicher, dass Sie angemeldet sind.
08.02.2012: Die Ergebnisse der zweiten Praxisaufgabe sind im Login-Bereich verfübar.
07.02.2012: Wegen administrativer Schwierigkeiten erfolgte die Freischaltung der Anmeldung für die Klausur am 14.2. erst heute. Die Anmeldefrist wird daher bis Donnerstag verlängert.
25.01.2012: Die Ergebnisse des Zwischentests sind im Login-Bereich verfübar.
17.01.2012: Neue Version des Skriptums jetzt verfügbar.
12.12.2011: An-/Abmeldung zur Zwischenklausur ab jetzt bis 10.1.12 im Login-Bereich möglich

Materialien

Vorlesungsfolien

Die Vorlesungsfolien werden hier jeweils nach der Vorlesung zur Verfügung gestellt.
  1. Organisatorisches: bildschirm - druck
    Syntax und Semantik der Ausagenlogik bildschirm - druck
    Vorlesung am 20.10.11
  2. Aussagenlogische Normalformen: bildschirm - druck
    Binary Decision Diagrams: bildschirm - druck
    Vorlesung am 21.10.11
  3. Erfüllbarkeitsprobleme für spezielle Formelklassen: bildschirm - druck
    Hilbert Kalkül für Aussagenlogik: bildschirm - druck
    Vorlesung am 27.10.11
  4. Übung am 28.10.11
  5. Resolutionskalkül für Aussagenlogik: bildschirm - druck
    Vorlesung am 03.11.11
  6. Tableaukalkül für Aussagenlogik: bildschirm - druck
    Vorlesung am 04.11.11
  7. Tableaukalkül für Aussagenlogik (Forts.)
    Sequenzenkül für Aussagenlogik: bildschirm - druck
    Vorlesung am 10.11.11
  8. Übung am 11.11.11
  9. Aussagenlogik: Sonstige Kalküle: bildschirm - druck
    Anwendungen der Aussagenlogik: bildschirm - druck
    Vorlesung am 17.11.11
  10. Prädikatenlogik: Syntax, Unifikation nach Robinson: bildschirm - druck
    Vorlesung am 18.11.11
  11. Prädikatenlogik: Semantik: bildschirm - druck
    Vorlesung am 24.11.11
  12. Übung am 25.11.11
  13. Prädikatenlogik: Normalformen: bildschirm - druck
    Vorlesung am 01.12.11
  14. Prädikatenlogik: Resolutionskalkül: bildschirm - druck
    Vorlesung am 02.12.11
  15. Prädikatenlogik: Tableaukalkül: bildschirm - druck
    Vorlesung am 08.12.11
  16. Übung am 09.12.11
  17. Prädikatenlogik: Tableaukalkül Fortsetzung
    Prädikatenlogik: Sequenzenkül bildschirm - druck
    Peano Arithmetik bildschirm - druck
    KeY Beweisdateien
    Vorlesung am 15.12.11
  18. Einführung in JML bildschirm - druck
    Vorlesung am 16.12.11
  19. Reduktionssysteme bildschirm - druck
    Termersetzungssysteme bildschirm - druck
    Vorlesung am 12.01.12
  20. Klausurtest
    Musterlösung zur Klausur
  21. Modale Logik bildschirm - druck
    Vorlesung am 19.01.12
  22. Modale Logik (Forts.)
    Vorlesungsevaluierung
    Vorlesung am 20.01.12
  23. Endliche Automaten (Wiederholung) bildschirm - druck
    Büchi Automaten bildschirm - druck
    Vorlesung am 26.01.12
  24. Büchi Automaten Fortsetzung
    Lineare Temporale Logik, LTL bildschirm - druck
    Vorlesung am 02.02.12
  25. Lineare Logik und Büchi Automaten bildschirm - druck
    Modellprüfung für LTL bildschirm - druck
    Vorlesung am 03.02.12
  26. Wiederholung bildschirm - druck
    Prädikatenlogik 2. Stufe bildschirm - druck
    Vorlesung am 09.02.12
  27. Klausur vom 14.02.2012
    Musterlösung zur Klausur
  28. Klausur vom 12.04.2012
    Musterlösung zur Klausur

Ü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.

Übungsblatt
Ausgabe am
Besprechung am
Lösung
blatt1.pdf 24.10.11 28.10.11 loesung1.pdf
blatt2.pdf 27.10.11 11.11.11 loesung2.pdf
blatt3.pdf 04.11.11 11.11.11 loesung3.pdf
blatt4.pdf 14.11.11 25.11.11 loesung4.pdf
blatt5.pdf 18.11.11 25.11.11 loesung5.pdf
blatt6.pdf 28.11.11 9.12.11 loesung6.pdf
blatt7.pdf 2.12.11 9.12.11 loesung7.pdf
blatt8.pdf 9.12.11 online loesung8.pdf
blatt9.pdf 19.12.11 online loesung9.pdf
blatt10.pdf 18.01.12 27.01.12 loesung10.pdf
blatt11.pdf 26.01.12 10.02.12 loesung11.pdf
blatt12.pdf 02.02.12 10.02.12 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.

Skriptum


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.

Praxisaufgabe
Ausgabe am
Abgabe am
 
praxis1.pdf 11.11.11 20.12.11 Weitere Infos ...
praxis2.pdf 17.1.12 6.2.12 Weitere Infos ...

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 den Zwischentest und Praxisaufgaben vergebenen Bonuspunkte (s.u.).

Die 1. Abschlussklausur (Hauptklausur) findet am Dienstag, dem 14.02.12, 14:00 Uhr im Hörsaal am Fasanengarten statt.

Die 2. Abschlussklausur (Nachklausur) findet am Donnerstag, dem

12.04.2012 um 14:00 Uhr im Hertz-Hörsaal
statt.

Zur Nachklausur kann man sich bis zum 5.4.2012 anmelden. Die Anmeldung erfolgt dabei über das Studierendenportal des KIT.

Zwischentest ("Zwischenklausur")

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

Der Zwischentest findet am 13.01.2012 um 11:30 Uhr statt. Die An- und Abmeldung erfolgt vom 12.12.11 bis zum 10.01.12 über die Login-Seite. Beachten Sie bitte: Nur wer sich angemeldet hat, kann am Zwischentest teilnehmen.

Bonuspunkte

Für die erfolgreiche Teilnahme an dem Zwischentest werden 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

Details zu den Terminen
   


Inhaltsübersicht


Peter H. Schmitt