Formale Systeme
Wahlpflichtvorlesung/Stammmodul im Wintersemester 2013/2014
Prof. Dr.
Peter H. Schmitt
Christoph Scheben, Mattias Ulbrich, Dr. Vladimir Klebanov
Aktuelles
Datum: Nachricht
26.08.2013:
Vorlesungsbeginn ist der 21. Oktober 2013
13.12.2013:
Die Veranstaltung am 20.12.2013 wird sowohl Vorlesung als auch Übung sein.
Neben abschließendem Stoff zur Prädikatenlogik werden die Lösungen zu den Aufgaben des
8. Übungsblattes vorgestellt.
16.12.2013:
Die Anmeldung zum Zwischentest ist offen.
Nur angemeldete Teilnehmer können am Zwischentest teilnehmen!
17.1.2014:
Die Anmeldung zur Klausur ist ab sofort möglich.
Bitte benutzen Sie dazu das Studierendenportal (https://studium.kit.edu/).
Für Studierende anderer Fakultäten und Austauschstudierende
können andere Anmeldemodalitäten gelten.
24.1.2014:
Die Ergebnisse und die erzielten Bonuspunkte der ersten Praxisaufgabe und
des Zwischentests können nun im
Login-Bereich
eingesehen werden.
12.2.2014:
Die Ergebnisse und die erzielten Bonuspunkte der zweiten Praxisaufgabe können nun auch im
Login-Bereich
eingesehen werden.
14.2.2014:
Klausur 1: Die erste Klausur wird am 17.02.14 um 14:00 im
Hörsaal am Fasanengarten 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.
03.03.2014:
Klausureinsicht: Die Klausureinsicht zur ersten Klausur wird
am 17.03.14 von 10:00 bis 11:00 in Raum R236 (Geb. 50.34) stattfinden.
13.03.2014:
Die Ergebnisse der Klausur sind nun veröffentlicht.
17.03.2014:
Die Musterlösung der Klausur 1 ist nun veröffentlicht.
09.04.2014:
Klausur 2: Die zweite Klausur wird am Freitag, 11.04.14, 11:00 im
Hörsaal am Fasanengarten 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.
14.05.2014:
Die Ergebnisse der zweiten Klausur
sind nun veröffentlicht.
Der Einsichtstermin (in ca. 2 Wochen)
wird in Bälde hier bekannt gegeben.
15.05.2014:
Die Einsicht für die zweite Klausur Formale Systeme findet am 28.5. von
12:30-13:30 in Raum -118 statt.
Materialien
Vorlesungsfolien
Die Vorlesungsfolien werden hier jeweils nach der Vorlesung zur
Verfügung gestellt.
-
Organisatorisches:
bildschirm -
druck
Syntax und Semantik der Aussagenlogik:
bildschirm -
druck
Vorlesung am 24.10.13
-
Syntax und Semantik der Aussagenlogik (Fortsetzung und Ende)
Craigsches Interpolationslemma
bildschirm -
druck
Kurze Konjunktive Normalform
bildschirm -
druck
Vorlesung am 25.10.13
-
Shannon Graphen (OBBD)
bildschirm -
druck
Vorlesung am 31.10.13
-
Übungen am 07.11.13
-
Erfüllbarkeitstest (SAT solver)
bildschirm -
druck
Einführung in die Prädikatenlogik
bildschirm -
druck
Vorlesung am 08.11.13
-
Einführung in die Prädikatenlogik (Fortsetzung und Ende)
Vorlesung am 14.11.13
-
Übungen am 15.11.13
-
Semantik der Prädikatenlogik
bildschirm -
druck
Vorlesung am 21.11.13
-
Prädikatenlogik: Normalformen
bildschirm -
druck
Vorlesung am 22.11.13
-
Informelle Einführung in die Beweistheorie
bildschirm -
druck
Hilbertkalkül
bildschirm -
druck
Vorlesung am 28.11.13
-
Übungen am 29.11.13
Blatt 4 ganz, Blatt 5 teilweise besprochen.
-
Aussagenlogischer Resolutionskalkül
bildschirm -
druck
Prädikatenlogischer Resolutionskalkül
bildschirm -
druck
Vorlesung am 05.12.13
-
Prädikatenlogischer Resolutionskalkül
(Fortsetzung und Ende)
Tableaukalkül
bildschirm -
druck
Vorlesung am 06.12.13
-
Tableaukalkül (Fortsetzung und Ende)
Sequenzenkalkül
bildschirm -
druck
Vorlesung am 12.12.13
-
Übungen am 13.12.13
-
Peano-Arithmetik
bildschirm -
druck
KeY Demo
EA->AE Beispiel -
Relationen Beispiel -
Beispiel vom reichen Grossvater
JML
bildschirm -
druck
Vorlesung am 19.12.13
-
JML , Fortsetzung und Ende
Übungsblatt 8
Vorlesung am 20.12.13
- Reduktionssysteme
bildschirm -
druck
Termersetzungssysteme
bildschirm -
druck
Vorlesung am 09.01.14
- Klausurprobe
Musterlösung
Veranstaltung am 10.01.14
- Modale Logik
bildschirm -
druck
Vorlesung am 16.01.14
- Modale Logik
(Fortsetzung und Ende)
Evaluierung
Vorlesung am 17.01.14
-
Endliche Automaten (wiederholung
bildschirm -
druck
Büchi Automaten
bildschirm -
druck
Vorlesung am 23.01.14
-
Übungen am 24.01.14
-
Büchi Automaten, Forts. und Ende
Lineare Temporale Logik
bildschirm -
druck
Vorlesung am 30.01.14
-
Von LTL zu Büchi Automaten
bildschirm -
druck
Vorlesung am 31.01.14
-
LTL Modellprüfung LTL (model checking)
bildschirm -
druck
Vorlesung am 06.02.14
-
Übungen am 07.02.14
Blätter 11 und 12 besprochen.
-
Wiederholung
bildschirm
Vorlesung am 13.02.14
-
Übungen am 14.02.14
Praxisblatt 2 besprochen / noch ein wenig Wiederholung
bildschirm
Ü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.
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.
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
Montag, dem 17.02.14, 14:00 Uhr statt im Hörsaal am Fasanengarten statt.
Die Ergebnisse der Klausur sind
online einsehbar. Die Veröffentlichung erfolgt unter der
Codenummer, die auf dem Deckblatt Ihrer Klausur abgedruckt war.
Sollte Ihre Klausur keine Codenummer gehabt haben, setzen Sie sich
bitte persönlich mit uns in Verbindung.
Die 2. Abschlussklausur
(Nachklausur) findet statt am Freitag, 11.04.14, 11:00 im Hörsaal am Fasanengarten.
Die Ergebnisse der zweiten Klausur (Nachklausur) sind
online einsehbar. Die Veröffentlichung erfolgt unter der
Codenummer, die auf dem Deckblatt Ihrer Klausur abgedruckt war.
Sollte Ihre Klausur keine Codenummer gehabt haben, setzen Sie sich
bitte persönlich mit uns in Verbindung.
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 10.01.2014 um 11.30 Uhr
statt.
Aufgaben und Musterlösungen
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
- Donnerstags, 14:00 - 15:30 Uhr, Gaede-Hörsaal (Geb. 30.22,
Raum 130.1)
- Freitags, 11:30 - 13:00 Uhr, Gaede-Hörsaal (Geb. 30.22, Raum
130.1)
Details zu den Terminen
Inhaltsübersicht
- Aussagenlogik
- Syntax und Semantik
- Kalküle
- Anwendungen
- Prädikatenlogik
- Syntax und Semantik
- Kalküle
- Anwendungen
- Gleichheit
- Java Modeling Language (JML)
- Modale Aussagenlogik
- Temporale Logik (LTL)
- Endliche Automaten (Wiederholung)
- Büchi Automaten
- Modellprüfung
Peter H. Schmitt