SoSe 2007

Lehrstuhl Theoretische Informatik

Henning Fernau; Stefan Gulan

Logik für Informatiker, von Martin Kreuzer, Stefan Kühling

Proseminar: Alles Logo

Seminar: Exakte und approximative Algorithmen für Logik-Probleme

[Zusammenfassung] [Themenliste] [Termine] [Hinweise]



Überblick

Das Verständnis logischer Grundlagen ist für Informatiker ein unerlässliches Hilfsmittel. Im Proseminar werden wir neue, für Informatiker wichtige Facetten der Logik kennenlernen mit Hilfe des Buches Logik für Informatiker von Martin Kreuzer und Stefan Kühling, Pearson Studium, 2006, kurz (KK). Außerdem werden wir uns mit Zusammenhängen zwischen Logik und regulären Sprachen beschäftigen.

Das Hauptseminar dient dazu, Problemstellungen aus der Logik unter algorithmischen und komplexitätstheoretischen Blickwinkeln zu beleuchten.

Um eine vernünftige Teilnehmeranzahl zu erreichen, werden wir das Proseminar und das Hauptseminar höchstwahrscheinlich zusammen stattfinden lassen. Der Vorteil für Sie ist: Sie erhalten die Gelegenheit, mehrere unterschiedliche Vorträge (und Vortragstechniken) zu sehen und sich dadurch noch mehr in den betreffenden Techniken zu schulen.


Die folgenden Themen können im Proseminarteil bearbeitet werden:

  1. Hornlogik und Logisches Programmieren Kapitel 3 aus KK

  2. Prädikatenlogik und zugehöriger Resolutionskalkül: Kapitel 4 aus KK

  3. Gleichungslogik und Knuth-Bendix-Vervollständigung: Kapitel 5 aus KK

  4. Modallogik und Tableaukalkül: Kapitel 6 aus KK

  5. Temporallogik: Kapitel 7 aus KK

  6. Dynamische Logik und Prozesslogik: Kapitel 8 aus KK

  7. Monadische Logik zweiter Stufe und Zusammenhänge mit regulären Sprachen (Kap. II/III aus Howard Straubing. Finite automata, formal logic, and circuit complexity. Birkhäuser, Boston, MA, 1994)


Weitere Themen werden wir gerne bei Bedarf bereitstellen.


Die folgenden Themen können im Seminarteil bearbeitet werden:

(Wir erwarten von den Seminarteilnehmern, dass sie sich nach Durcharbeiten der angegebenen Artikel selbständig in einen sie besonders interessierenden Aspekt vertiefen und entsprechende Literatur in Absprache mit dem Betreuer studieren und für den Vortrag aufbereiten.)

  1. Exakte Algorithmen für das Erfüllbarkeitsproblem (evtl. auch zwei Themen; Literatur beispielsweise von O. Kullmann)

  2. Einführung in Parameterisierte Komplexitätstheorie (z.B.: Flum/Grohe: Parameterized Complexity Theory, Springer, 2006; Kap 1-2)

  3. Logische Bezüge zur Parameterisierten Komplexitätstheorie (z.B.: Flum/Grohe, Kap. 3; evtl. auch zwei Themen (mit Kap. 4))

  4. Parameterisierte Algorithmen für MaxSAT

  5. Approximationsalgorithmen


Weitere Themen werden wir gerne bei Bedarf bereitstellen.


Termine

Das (Pro-)Seminar wird in Blockform abgehalten, und zwar in der Vorlesungswoche dieses Sommer-Semesters nach Pfingsten.

Genaueres wird noch auf dieser Seite bekanntgegeben.

Anmelden können sich Interessierte durch eine Email an Henning Fernau (fernau AT...) oder Stefan Gulan (gulan AT ...); zu ergänzen ist immer: informatik.uni-trier.de.

Es wird allerdings dringend empfohlen, an der allgemeinen Vorbesprechung des (Pro-)Seminars teilzunehmen, die am Mittwoch, den 14.02.2007 um 13.30 Uhr im H413 stattfinden wird.

Es werden aber auch noch nachträgliche Meldungen angenommen.

Scheinkriterien: Es gibt einen benoteten Schein.

Die Note setzt sich wie folgt zusammen: Vortrag 50%, Ausarbeitung 40%, aktive Teilnahme an Vortragsdiskussion 10%.

Ablauf der Vorbereitung:

*

Der Vortrag und die Ausarbeitung müssen mit dem Betreuer abgesprochen werden. Hierzu sind nachfolgende Terminvorgaben bindend (soweit nicht anders mit dem Betreuer abgestimmt). Werden die Termine nicht eingehalten, führt dies zur Streichung des Vortrags und zum Nichtbestehens des Seminars.

bis 8 Wochen vor dem Vortrag

erstes Treffen mit dem Betreuer (vor dem Treffen ist die Literatur bereits zu lesen);

bis 4 Wochen vor dem Vortrag

Gliederung des Vortrags und der Ausarbeitung mit dem Betreuer besprechen;

bis 1 Woche vor dem Vortrag

fertige Folien und vollständige erste Version der Ausarbeitung mit dem Betreuer abstimmen;

bis 1 Woche nach dem Vortrag

fertige Ausarbeitung abgeben.

Anfertigung der Ausarbeitung:

*

Alle fertigen Ausarbeitungen werden nach dem Seminar gedruckt und an alle Teilnehmer verteilt. Damit eine einheitliche Form erzielt wird, müssen alle Ausarbeitungen mit dem Textsatzsystem LaTeX erstellt werden. Hierzu sind folgende Konventionen zu beachten:

  • Es sollte 10-Punkt-Schrift in Standard-Latex eingestellt sein.

  • Die Ausarbeitung sollte nicht länger als 10 Seiten sein.

  • Bei der Einbindung von Bildern oder Graphiken ist darauf zu achten, dass sie lesbar ausgedruckt werden können.

  • Ein kleines Beispiel (von einem Mitarbeiter der TU München) sollte die Benutzung von LaTeX erläutern; Sie können dies gerne als Template für Ihre Ausarbeitung nehmen.

*

Bei Fragen zu LaTeX sei einerseits auf den folgenden Link hingewiesen, ferner kann auch der Betreuer um Hilfestellungen bzw. Literaturangaben gebeten werden.

Der Vortrag selbst sollte auf 50 Minuten angelegt sein. Abweichungen hiervon wirken sich auf die Note aus.