Formale Systeme

Wahlpflichtvorlesung/Stammmodul im Wintersemester 2011/2012

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

Forum http://i12www.iti.kit.edu/~farago/fsforum

Aktuelles

Datum Nachricht
17.01.2012 Neue Version des Skriptums jetzt verfügbar.
12.12.11: 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

Ü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

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, statt (Hösäle werden noch bekanntgegeben).
Die 2. Abschlussklausur (Nachklausur) findet am Donnerstag, dem 12.04.2012, 14:00 Uhr, statt.

Die Anmeldung ist im Studierendenportal des KIT möglich.

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