Logik (Sommersemester 2017)

  1. Neuigkeiten
  2. Material
  3. Organisation

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.

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