Organisatorisches

Proseminar
für das Modul Wissenschaftliches Arbeiten in der Informatik, 5 ECTS
Termin
Dienstags 10-12, Raum SR140 in der Arnimallee 7
Zeitraum
14.04.2015 - 14.07.2015
Zielgruppe
Bachelorstudiengang Informatik (alte und neue Studienordnung)
Voraussetzungen
Erfolgreiche Teilnahme an "Logik und Diskrete Mathematik" (oder einer ähnlichen Veranstaltung) wird empfohlen
Mailingsliste
PSLogik15@lists.fu-berlin.de

Die Modulnote ergibt sich aus einem Vortrag (ca. 30 Minuten) mit anschließender Diskussion. Zur aktiven Teilnahme soll eine ca. 4-5 seitige schriftliche Ausarbeitung über das eigene Vortragsthema angefertigt werden. Aktive Beteiligung in den Diskussionen ist stärkstens erwünscht! Diese vorangegangene Erklärung orientiert sich am Modul Wissenschaftliches Arbeiten aus dem neuen Bachelorstudiengang. Falls Sie noch im alten Studiengang immatrikuliert sein, prüfen Sie bitte inwiefern dies auch für Sie gilt!.

Die Veranstaltung ist für max. 20 Studierende ausgelegt.

Das erste Treffen findet am ersten regulären Termin statt, d.h. am Dienstags, den 14.04. um 10 Uhr.

Inhalt

In diesem Proseminar sollen grundlegende Inhalte über Propositionallogik und Logik erster Stufe, besonders aber über deren Automatisierung, erarbeitet und diskutiert werden. Dabei werden wir uns zu Beginn der Veranstaltung mit einfacher Propositionallogik (d.h. Logik ohne Quantoren und Funktionen) auseinandersetzen und einige formale Begrifflichkeiten und mathematische Resultate, z.B. über Entscheidbarkeit und Komplexität, kennenlernen.

Im weiteren Verlauf der Veranstaltung wird dann die Automatisierung der Logiken, vor allem von Logik erster Stufe, im Fokus stehen. Hierbei werden formale Resultate und praktische Techniken vorgestellt, die in automatischen Theorembeweisern zum Einsatz kommen. Einige Entscheidungskomponenten von Theorembeweisern werden implementiert (wahrscheinlich in Haskell) und mit formalen Hintergrund vorgestellt und diskutiert.

Wenn genug Zeit bleibt, können nicht-klassische Erweiterungen wie z.B. propositionale Modallogik oder Beschreibungslogik diskutiert werden. Es können, je nach Situation, auch geschichtliche Entwicklungen und philosophische Relevanz der Logiken (bzw. Aspekte davon) thematisiert werden.

Ablauf

Das Proseminar wird als "Symposium" organisiert: Gegen Ende der Vorlesungszeit treffen wir uns zu einem Zwei-Tage-Block bei dem die Vorträge gehalten werden. Im Laufe der Vorlesungszeit werden wir uns regelmäßig treffen um in entspannter Atmosphäre Fragen zu klären und Probleme zu adressieren.
  • 14.04.: Vorbesprechung
    Klärung von Fragen, erste Vergaberunde von Vortragsthemen
  • 21.04.: Kurze Einführung in Logik, math. Notationen, Begriffe, ... Mitschrift
    Besprechung des weiteres Vorgehens, evtl. Vergabe von restlichen Vortragsthemen
    Vorstellung des Rahmenwerkes für die Implementierung von kleinen Funktionen/Programmen
  • 12.05.: 1. Zwischenbesprechung (Pflichttermin!)
    Informelle Besprechung des Zwischenstandes, Klären von Fragen und Problemen
  • 02.06.: 2. Zwischenbesprechung (Pflichttermin!)
  • Ende Juni/Anfang Juli: Individuelle Termine zur Präsentations- und Ausarbeitungsberatung (Freiwillig, aber stark empfohlen!).
  • 06.07 und 10.07: Symposium
    Zwei Tage Block von Vorträgen und anschließenden Diskussionen, jeweils von 12 Uhr bis ca. 15 Uhr.
    Raum (06.07): Seminarrraum 2.2059 (Fabeckstr. 23-25),
    Raum (10.07): SR E.31/A7 (Arnimallee 7)
  • 30.09: Abgabefrist für die Ausarbeitung

Vortragsthemen

(vorläufige Vorschläge)

  • Einführung Logiken: Beweiskalküle, syntaktisches Schliessen, Widerspruchsfreiheit, Vollständigkeit
    • Decision Procedures [1] Kapitel 1
    • Fitting [2] Kapitel 4
    • Classical Logic [3]
    • Handbook [4] Kaptiel 1
  • Einführung / Entscheidbarkeit von Propositionallogik, Automatisierung
    • Fitting [2] Kapitel 2.1-2.6
    • Fitting [2] Kapitel 3
    • Decision Procedures [1] Kapitel 2
  • Einführung Logik erster Stufe, Syntax und Semantik (vergeben)
    • Classical Logic [3]
    • Fitting [2] Kapitel 5.1-5.4
  • Logik erster Stufe: Entscheidbarkeit (vergeben)
    • Fitting [2] Kapitel 5.5 - 5.11
  • Logik erster Stufe: Automatisierung I (Normalformen) (vergeben)
    • Fitting [2] Kapitel 7.11-7.12
    • Handbook [4] Kapitel 5
    • Handbook [4] Kaptiel 6
  • Logik erster Stufe: Automatisierung II (Kalküle) (vergeben)
    • Fitting [2] Kapitel 6
    • Handbook [4] Kapitel 2-3
    • Handbook [4] Kapitel 7
  • Automatische Theorem Beweiser
    • TPTP [8]
    • Freie Wahl eines Beweiser (Literatur empfehlen wir dann)
  • Logik erster Stufe: Automatisierung III (Unifikation) (vergeben)
    • Fitting [2] Kapitel 7.2-7.3
    • Handbook [4] Kapitel 8
  • Logik erster Stufe: Technische Details (Indexing, Termdarstellung, o.Ä.)
    • Literatur nach Bedarf für ein spezielles Thema
  • Logik erster Stufe: Gleichheit (Equality)
    • Fitting [2] Kapitel 8
  • Beschreibungslogiken (vergeben)
    • Handbook [4] Kapitel 23
    • weitere Literatur folgt
  • Modallogik: Motivation (vergeben)
    • Fitting [5] Kapitel 1
    • Modal Logic [6]
  • Modallogik: Syntax und Semantik (vergeben)
    • Modal Logic [6]
    • Popkorn [7]
  • ...

Es können auch gerne selbstständig Vortragsthemen vorgeschlagen werden!

Literatur

  1. Danial Kroening, Ofer Strichman, Decision Procedures, Springer
  2. Melvin Fitting, First-Order Logic and Automated Theorem Proving, Springer-Verlag
  3. SEP -- Classical Logic
  4. Alan Robinson, Andrej Voronkov, Handbook of Automated Reasoning, Elsevier B.V. (im Uninetz verfügbar)
  5. Melvin Fitting, Richard L. Mendelsohn, First-Order Modal Logic, Kluwer Academic Publishers
  6. SEP -- Modal Logic
  7. Sally Popkorn, First Steps in Modal Logic, Cambridge University Press
  8. TPTP
Weitere Literatur folgt.