Logik (Sommersemester 2017)
Some Information in English with translations of the exercise sheets are available.
Neuigkeiten
Die Ergebnisse der 2. Abschlussklausur sind nun im Stat-System veröffentlicht. Die Einsichtnahme zur Klausur findet am Dienstag, 17. Oktober um 14:00 Uhr in Raum 34-420 statt. Falls Sie diesen Termin nicht wahrnehmen können, vereinbaren Sie bitte einen gesonderten Termin mit Peter Zeller.
Die Ergebnisse der Abschlussklausur sind nun im Stat-System veröffentlicht. Die Einsichtnahme zur Klausur findet am Dienstag, 19. September von 14:00 bis 15:00 Uhr (bei Bedarf auch länger) in Raum 34-420 statt. Falls Sie diesen Termin nicht wahrnehmen können, vereinbaren Sie bitte einen gesonderten Termin mit Peter Zeller.
Falls es nach der Einsicht noch Einwände gibt, die nicht geklärt werden konnten, können Sie sich eine Kopie der Klausur anfertigen lassen. Füllen Sie dazu bitte den “Antrag auf Ablichtung einer bewerteten Prüfungsleistung” aus und geben ihn in unserem Sekretariat ab.
Zur Klausurvorbereitung ist in den zwei Wochen vor der Klausur (also vom 28.08. bis zum 08.09.) der Raum 48-453 als Lernraum reserviert. Wir werden dort auch zu den folgenden Zeiten anwesend sein um Fragen zu beantworten, die bei der Vorbereitung eventuell auftreten:
- Donnerstag, 31.08. 14:00-15:00 Uhr
- Dienstag, 05.09. 15:00-16:00 Uhr
- Donnerstag, 07.09. 14:00-15:00 Uhr
- Freitag, 08.09. 14:00-15:00 Uhr
Diese Zeiten werden sich eventuell noch ändern.
Die Fragestunde am 17. Juli findet nicht statt. Sollten Sie noch offene Fragen haben, wenden Sie sich bitte an Peter Zeller.
Die Ergebnisse der Zwischenklausur sind nun im Stat-System veröffentlicht. Die Zwischenklausur ist bestanden, genau dann wenn 26 oder mehr Punkte erreicht wurden. Bitte beachten Sie, dass die Punktegrenze für das Bestehen bei der Abschlussklausur in der Regel höher liegt. Falls Sie weniger als die Hälfte der Punktzahl erreicht haben, sollten Sie auf jeden Fall noch mehr Arbeit in die Vorlesung investieren als bisher. Wir möchten an dieser Stelle auch noch einmal auf die wöchentliche Fragestunde hinweisen, die Ihnen helfen kann den Stoff zu verstehen und anzuwenden.
Die Klausuren werden nächste Woche in den Übungen zurückgegeben. Falls Sie nicht bestanden haben, können Sie außerdem einen Termin zur Einsicht mit Peter Zeller vereinbaren. Dieser Termin soll vor der Rückgabe der Klausur liegen.
Sie haben die Möglichkeit die Zwischenklausur zum Termin der ersten Abschlussklausur zu wiederholen, falls Sie die Klausur nicht bestanden oder nicht mitgeschrieben haben. Bitte melden Sie sich dafür bei Peter Zeller an.
Am 15.06. (Fronleichnam) fällt die Donnerstagsübung aus. Statt dessen bieten wir die folgenden Ersatztermine an (jeweils in Raum 34-420):
- Gruppe 1: Montag, 19.06. 11:45 Uhr
- Gruppe 2: Montag, 19.06. 10:00 Uhr
- Gruppe 3: Dienstag, 13.06. 11:45 Uhr (Achtung: Diesmal schon vor dem Feiertag!)
Es gelten ansonsten die gleichen Regelungen wie zu Christi Himmelfahrt (siehe unten).
Am 25.05. (Christi Himmelfahrt) fällt die Donnerstagsübung aus. Statt dessen bieten wir die folgenden Ersatztermine an (in der Woche nach dem Feiertag, in Raum 34-420):
- Gruppe 1: Montag 11:45
- Gruppe 2: Dienstag 10:00
- Gruppe 3: Dienstag 11:45
Unabhängig davon, ob Sie in einer Donnerstags- oder Freitags-Gruppe sind, können Sie sich für die betroffenen Wochen jeweils einen Übungstermin aussuchen, der Ihnen passt. Im Stats finden Sie die Übung “Logik (Ersatzübung) SS17”, in der Sie sich für eine andere Gruppe eintragen können, falls genügend Plätze vorhanden sind. Wenn Sie in einer Donnerstags-Gruppe sind entfällt die Anwesenheitspflicht, falls Sie sich rechtzeitig im Stats von der Ersatzübung abmelden. Wir empfehlen aber auf jeden Fall eine Übung zu besuchen, wenn es zeitlich möglich ist.
Am 24.05. findet keine Vorlesung statt (der Vorlesungsraum ist für den Studien-Informationstages reserviert).
Material
Vorlesungsmaterial
| Folien | Vorlesung | Themen |
|---|---|---|
| Foliensatz 1 | 19.04. | Einleitung, Literaturempfehlungen, Syntax und Semantik der Aussagenlogik, Strukturelle Induktion |
| Kompaktheitssatz | 26.04. | Beweis des Kompaktheitssatzes |
| Foliensatz 2 | 26.04. und 03.05. | Kompaktheitssatz, Deduktive Systeme Aktualisierte Version (02.05.): Definition von abgekürzten Beweisen in deduktiven Systemen ist geändert |
| Foliensatz 3 | 10.05. | Vollständigkeit von F0 und Sequenzenkalkül Aktualisierte Version (31.05.): Bessere Formulierung für Satz 2.18 |
| Beweise zu F0 | 10.05. | Beweis des Deduktionstheorems und der Vollständigkeit von F0 |
| Foliensatz 4 | 17.05. und 31.05. | Algorithmische Verfahren für die Aussagenlogik: Tableaus, Normalformen, Davis-Putnam, Resolution Aktualisierte Version (31.05.): Kleinere Verbesserungen |
| Foliensatz 5 | 31.05. und 07.06. | Prädikatenlogik (Syntax, Semantik, Normalformen) Aktualisierte Version (06.06.): Folien zur Semantik Aktualisierte Version (13.06.): Korrigierte Definition der Substitution (Folie 133) |
| Foliensatz 6 | 14.06. und 21.06. | Das deduktive System F, Theorien Aktualisierte Version (21.06.): Korrekturen und weitere Folie zu Theorien Aktualisierte Version (28.06.): Gleichheit aus Signatur in Beispielen entfernt. |
| Foliensatz 7 | 21.06., 28.06., 05.07., 12.07 | Algorithmische Verfahren für die Prädikatenlogik Aktualisierte Version (28.06.): weitere Folien Aktualisierte Version (05.07.): weitere Folien |
| Foliensatz 8 | 19.07. | Anwendungen von Logik: SMT, Programmverifikation Aktualisierte Version (17.07.): Folien ohne Animationen, Tippfehler in Korrektheits-Definition korrigiert |
Alle Folien: Bis Folie 195
Es gibt außerdem ältere Skripte zur Vorlesung. Beachten Sie, dass die Notationen und Definitionen sich teilweise unterscheiden.
- Skript von Prof. Madlener (2002)
- Skript von Prof. Madlener und Prof. Meyer (2013)
- Zusatzmaterial zu Nichtstandardmodellen von Prof. Meyer (2016)
- Auf der Seite von letztem Jahr finden Sie hanschriftliche Notizen zur Vorlesung vom Prof. Meyer (2016).
Übungsmaterial
| Übungsblatt | Datum | Themen |
|---|---|---|
| 01 - Präsenz | am 20./21.04. | Beschreiben von Problemen mit Logik, Strukturelle Induktion |
| 02 - Abgabe | bis 28.04. | Strukturelle Induktion, Definitionen zur Semantik von Formeln, Anwendung von Logik |
| 03 - Präsenz | am 27./28.04. | Vollständige Operatormengen, Strukturelle Induktion, Induktive Definitionen |
| 04 - Abgabe | bis 12.05. | Vollständige Operatormengen, Kompaktheitssatz, disjunktive Normalform, Deduktives System F0. Zusatzmaterial: Isabelle Tutorial Lösung zu Aufgabe 4 in Isabelle |
| 05 - Präsenz | am 11./12.05. | Deduktives System F0 |
| 06 - Abgabe | bis 26.05. | Gentzen-Sequentzkalkül, Tableaux. Zu Aufgabe 4: tableaux_java.zip 22.05. Weitere Hinweise und mehr Testfälle für Aufgabe 4 Lösung zu Aufgabe 4 |
| 07 - Präsenz | am 26./29./30.05. | Tableaux, Normalformen (DNF, NNF) Update 26.05: In Aufgabe 3b steht jetzt korrekt die logische Äquivalenz und nicht die syntaktische. Lösungsvorschlag |
| 08 - Abgabe | bis 9. Juni | Davis-Putnam-Verfahren, Resolventenmethode, Modellierung mit Prädikatenlogik |
| 09 - Präsenz | am 8./9. Juni | Semantik der Prädikatenlogik |
| 10 - Abgabe | bis 23. Juni | Prädikatenlogik: Semantik, Substitution, Normalformen |
| Zwischenklausur | am 19. Juni | |
| 11 - Präsenz | am 22./23. Juni | Prädikatenlogik: Das deduktive System F Lösungsvorschlag (aktualisiert am 27.06.: Generalisierungstheorem ist nur in eine Richtung definiert, deshalb sollte in der Lösung nicht “gdw.” stehen) Lösung in Isabelle |
| 12 - Abgabe | bis 07. Juli | Das deduktive System F, Nicht-Standardmodelle, Herbrand-Modelle |
| 13 - Präsenz | am 06./07. Juli | Presburger Arithmetik mit System F, Herbrand-Expansionen, Theorien |
| 14 - Abgabe | am Montag 17. Juli | Tableaus und Resolution mit Prädikatenlogik, Programmieren mit Prolog Lösung zu Aufgabe 4 (Prolog) |
Organisation
Die erste Vorlesung findet am Mittwoch, 19.04.2017, 11:45 in Raum 52-207 statt.
Die Übungen starten ebenfalls in der ersten Vorlesungswoche.
Anmeldung
Die Anmeldung zu den Übungen ist nun geschlossen. Sie können Ihre Übungsgruppe im Stat/Optimus-System sehen.
Sollten Sie die Anmeldefrist verpasst haben, melden Sie sich bitte per Mail bei Peter Zeller an. Geben Sie bitte in der Mail an, welche Übungstermine (siehe unten) für Sie möglich sind.
Theoretical Computer Science Amendment
If you are taking the “Logik” lecture as part of the “Theoretical Computer Science Amendment” (see Module 89-5021), please contact Peter Zeller as early as possible. We will provide more information on request.
You can find more information here.
Klausurzulassung
Die erfolgreiche Teilnahme an den Übungen ist notwendig, um zur Abschlussklausur zugelassen zu werden. Alte Klausur-Zulassungen bleiben bestehen, wir empfehlen aber, Vorlesung und Übungen erneut zu besuchen.
Konkret sind folgende Vorraussetzungen zu erfüllen:
Bestehen der Zwischenklausur.
Anwesenheit und aktive Teilnahme an den Übungen. Maximal zwei unentschuldigte Fehlzeiten sind erlaubt.
Es müssen 50% der Gesamt-Punkte für die Einreichaufgaben (Abgabe-Blätter) erreicht werden. Jede Einreichaufgabe wird dabei mit 0-4 Punkten bewertet (0 Punkte für unbearbeitete Aufgaben und ungenügende Lösungen, 1 Punkt für Lösungen mit sinnvollem Ansatz, 2 Punkt für Aufgbaben, die in der Klausur 50% der Punkte oder mehr gegeben hätten, 3 Punkte für Lösungen mit kleineren Fehlern und 4 Punkte für korrekte Lösungen).
Präsenz-Blätter werden in der Übung bearbeitet und sind nicht Teil der Klausurzulassung.
Übungstermine
| # | Tag | Zeit | Raum | Tutor |
|---|---|---|---|---|
| 1 | Donnerstag | 8:15 - 9:45 | 48-379 | Lea Plückebaum <plueckeb@rhrk.uni-kl.de> |
| 2 | Donnerstag | 10:00 - 11:30 | 44-336 | Kathrin Thomas <k_thomas14@cs.uni-kl.de> |
| 3 | Donnerstag | 13:45 - 15:15 | 48-379 | Albert Schimpf <a_schimpf12@cs.uni-kl.de> |
| 4 | Freitag | 11:45 - 13:15 | 52-204 | Kathrin Thomas <k_thomas14@cs.uni-kl.de> |
| 5 | Freitag | 13:45 - 15:15 | 32-439 | Albert Schimpf <a_schimpf12@cs.uni-kl.de> |
| 6 | Freitag | 15:30 - 17:00 | 13-370 | Lea Plückebaum <plueckeb@rhrk.uni-kl.de> |
Zu den Feiertagen wird es entsprechnde Ersatztermine geben, die hier bekannt gegeben werden.
Zwischenklausur
Die Zwischenklausur findet am Montag, 19.06.2017 um 19:00 Uhr in Raum 46-220 statt.
Wenn Sie für die Übung angemeldet sind, sind Sie auch automatisch für die Zwischenklausur angemeldet. Falls Sie mitschreiben wollen, aber nicht für die Übungen angemeldet sind, melden Sie sich bitte bei Peter Zeller für die Klausur an. Falls Sie nicht mitschreiben wollen, melden Sie sich bitte bei Peter Zeller ab.
Sie können die Zwischenklausur auch mitschreiben, wenn Sie die Zulassung bereits aus dem letzten Jahr haben.
Die Zwischenklausur kann zum Termin der ersten Abschlussklausur wiederholt werden.
Details
Dauer: 100 Minuten
Stoff: Alles bis einschließlich der Vorlesung am 14. Juni und Übungsblatt 9.
Ausgenommen ist die frewillige Aufgabe zu Isablle auf Blatt 4.
Das deduktive System F der Prädikatenlogik ist nicht Teil der Zwischenklausur.
Die Axiome und Regeln der deduktiven Systeme werden in der Klausur angegeben, falls es eine entsprechende Aufgabe geben sollte.
Zugelassene Hilfsmittel:
- Ein DIN A4 Blatt mit eigenen, handschriftlichen Notizen (beidseitig)
- Sprachwörterbücher
Abschlussklausur
Die erste Abschlussklausur findet am 11.09.2017 um 8:30 Uhr in Raum 42-115 statt.
Die zweite Abschlussklausur findet am 13.10.2017 um 8:15 Uhr in der Mensa statt.
Die Anmeldung zur Klausur erfolgt über das Prüfungsamt. Nachklausuren müssen schriftlich in der Abteilung für Prüfungsangelegenheiten angemeldet werden. Die Anmeldung für eine Nachklausur muss spätestens zwei Wochen vor dem Prüfungstermin erfolgen. Anmeldevordrucke finden Sie hier.
Fragestunde
Immer Montags um 13:45 findet in Raum 48-379 eine freiwillige Fragestunde statt. Diese richtet sich vor allem an Studenten, welche Probleme haben den Stoff zu verstehen oder in den Übungen anzuwenden. Es können aber auch Fragen gestellt werden, die über den Stoff der Vorlesung hinaus gehen.
Wenn Sie Fragen oder Wünsche für die Fragestunde haben, schreiben Sie bitte eine Mail an Kathrin Thomas k_thomas14(at)cs.uni-kl.de, so dass sie sich darauf vorbereiten kann.
Falls Sie Interesse an der Fragestunde haben, aber der Termin unpassend ist, schreiben Sie uns bitte auch eine Mail.
Kontakt
Die Vorlesung wird von Prof. Arnd Poetzsch-Heffter gehalten. Die Übungen werden von Peter Zeller organisiert.
Bei Fragen wenden Sie sich bitte an Peter Zeller.