Formale Systeme

Wahlpflichtvorlesung/Stammmodul im Wintersemester 2012/2013

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


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

Aktuelles

Datum: Nachricht
30.4.2013: Die Klausureinsicht zur zweiten Klausur findet am 24.05.13, 11:30-12:00, in Raum -101 (Minus 101) statt.
30.4.2013: Die Ergebnisse der zweiten Klausur sind jetzt verfügbar.
08.4.2013: Klausur 2: Die zweite Klausur wird am 12.04.13 um 08:00 im Audimax stattfinden. Falls Sie sich für die Klausur angemeldet haben, überprüfen Sie bitte, ob Ihre Matrikelnummer in der Anmeldungsliste tatsächlich aufgeführt ist.
28.3.2013: Eine neue, überarbeitete, umstrukturierte, bequemere Version des Skriptums ist jetzt verfügbar, siehe weiter unten.
04.3.2013:Diese Liste entält alle Klausurergebnisse, anonymisiert aufgelistet nach Klausurnummern.
13.2.2013: Diese Liste enthält alle angemeldeten Teilnehmer der Klausur. Bitte überprüfen Sie, ob Ihre Matrikelnummer auch gelistet wird!
13.2.2013: Die Klausur findet morgen für alle Teilnehmer im Hörsaal am Fasanengarten statt.
10.12.2012: Ab sofort ist es möglich, sich über die Login-Vorlesungshomepage für den Zwischentest am 11.01.13 anzumelden (oder ggf. auch wieder abzumelden). Bitte beachten Sie, dass nur mitschreiben kann, wer sich angemeldet hat!
30.11.2012: Wegen eines technischen Problems war Übungsblatt 6 in den letzten Tagen zeitweilig nicht verfügbar. Verzeihung dafür.
19.11.2012: Die Login-Seite zur Abgabe der Praxisaufgaben (später auch zur Anmeldung zum Zwischentest) ist online.
20.10.2012: Das erste Übungsblatt ist jetzt verfügbar
02.10.2012: Vorlesungsbeginn ist der 18.Oktober

Materialien

Vorlesungsfolien

Die Vorlesungsfolien werden hier jeweils nach der Vorlesung zur Verfügung gestellt.
  1. Organisatorisches: bildschirm - druck
    Syntax und Semantik der Aussagenlogik: bildschirm - druck
    Vorlesung am 18.10.12
  2. Syntax und Semantik der Aussagenlogik: (Fortsetzung und Ende)
    Normalformen: bildschirm - druck
    Geordnete binäre Entscheidungsdiagramme (BDD) bildschirm - druck
    Vorlesung am 19.10.12
  3. Geordnete binäre Entscheidungsdiagramme (BDD) (Fortsetzung und Ende)
    Spezielle aussagenlogische Formelklassen bildschirm - druck
    Hilbertkalkül bildschirm - druck
    Vorlesung am 25.10.12
  4. Übung am 26.10.12
  5. Hilbertkalkül (Fortsetzung und Ende)
    Resolutionskalkül bildschirm - druck
    Vorlesung am 02.11.12
  6. Aussagenlogischer Tableaukalkül bildschirm - druck
    Vorlesung am 08.11.12
  7. Übung am 09.11.12
  8. Aussagenlogischer Sequenzenkalkül bildschirm - druck
    Sonstige aussagenlogische Kalküle bildschirm - druck
    Anwendungen der Aussagenlogik bildschirm - druck
    Vorlesung am 15.11.12
  9. Einführung in die Prädikatenlogik, Syntax bildschirm - druck
    Vorlesung am 16.11.12
  10. Einführung in die Prädikatenlogik, Syntax, Fortsetzung und Ende
    Semantik der Prädikatenlogik bildschirm - druck
    Vorlesung am 22.11.12
  11. Übung am 23.11.12
  12. Semantik der Prädikatenlogik, Fortsetzung und Ende
    Normalformal der Prädikatenlogik bildschirm - druck
    Vorlesung am 29.11.12
  13. Resolutionskalkül für Prädikatenlogik bildschirm - druck
    Tableaukalkül für Prädikatenlogik bildschirm - druck
    Vorlesung am 30.11.12
  14. Tableaukalkül für Prädikatenlogik, Fortsetzung und Ende
    Vorlesung am 06.12.12
  15. Übung am 07.12.12
  16. Übung Fortsetzung und Ende
    Sequenzenkül für Prädikatenlogik bildschirm - druck
    KeY Demo
    Vorlesung am 13.12.12
  17. Peano Arithmetik bildschirm - druck
    Java Modeling Language (JML) bildschirm - druck
    Vorlesung am 14.12.12
  18. Übung am 20.12.12
  19. Reduktionssysteme bildschirm - druck
    Termersetzungssysteme bildschirm - druck
    Vorlesung am 10.01.13
  20. Zwischentest und Übung am 11.01.13
  21. Einführung in die Modale Logik bildschirm - druck
    Vorlesung am 17.01.13
  22. Modale Logik, Fortsetzung und Ende
    Vorlesung am 18.01.13
  23. Endliche Automaten, Wiederholung bildschirm - druck
    Büchi Automaten bildschirm - druck
    Vorlesung am 24.01.13
  24. Übung am 25.01.13
  25. Büchi Automaten, Forts. und Ende
    Einführung in lineare temporale Logik, LTL bildschirm - druck
    Vorlesung am 31.01.13
  26. Büchi Automaten und LTL bildschirm - druck
    Modellprüfung für LTL Formeln bildschirm - druck
    Vorlesung am 1.02.13
  27. Wiederholung bildschirm - druck
    Exkurs: Prädikatenlogik 2.Stufe bildschirm - druck
    Vorlesung am 7.02.13
  28. Übung am 8.02.13

Ü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 20.10.12 26.10.12 blatt1-lsg.pdf
blatt2.pdf 29.10.12 09.11.12 blatt2-lsg.pdf
blatt3.pdf 31.10.12 09.11.12 blatt3-lsg.pdf
blatt4.pdf 12.11.12 23.11.12 blatt4-lsg.pdf
blatt5.pdf 16.11.12 23.11.12 blatt5-lsg.pdf
blatt6.pdf 23.11.12 6.12.12 blatt6-lsg.pdf
blatt7.pdf
30.11.12 6.12.12 blatt7-lsg.pdf
blatt8.pdf
10.12.12 20.12.12 blatt8-lsg.pdf
blatt9.pdf
14.12.12 20.12.12 blatt9-lsg.pdf
blatt10.pdf
11.01.13 25.01.13 blatt10-lsg.pdf
blatt11.pdf
18.01.13 25.01.13 loesung11.pdf
blatt12.pdf
25.01.13 08.02.13 blatt12-lsg.pdf
blatt13.pdf
01.02.13 08.02.13 blatt13-lsg.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 8.11.12 21.12.12 Weitere Infos ...
praxis2.pdf 16.01.13 06.02.13 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.).

Die Abgabe der Lösungen zu den Praxisaufgaben erfolgt über die LOGIN-Abgabe-Seite. Auf dieser Seite müssen Sie sich beim ersten Betreten mit Ihrer Matrikelnummer registrieren.


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 Donnerstag, dem 14.02.13, 11:00 Uhr im Hörsaal am Fasanengarten statt.
Diese Liste enthält alle angemeldeten Teilnehmer der Klausur. Bitte überprüfen Sie, ob Ihre Matrikelnummer auch gelistet wird!

Die 2. Abschlussklausur (Nachklausur) findet statt am Freitag, 12.04.13, 08:00 im Audimax.

Zwischentest ("Zwischenklausur")

Im Laufe des Semesters wird ein Klausurtest 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 11.01.2013 um 11.30 Uhr statt.

Aufgaben und Musterlösungen

Zwischentest vom 11.1.2013  Musterlösung
Klausur 1 vom 14.2.2013  Musterlösung
Klausur 2 vom 12.4.2013  Musterlösung

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