Lehrstuhl für Theoretische Informatik
Henning Fernau / Stefan Gulan
Proseminar: Alles Logo
Seminar: Exakte und approximative Algorithmen für Logik-Probleme
Ü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 TeilnehmerInnenanzahl 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:
Hornlogik und Logisches Programmieren Kapitel 3 aus KK
Prädikatenlogik und zugehöriger Resolutionskalkül: Kapitel 4 aus KK
Gleichungslogik und Knuth-Bendix-Vervollständigung: Kapitel 5 aus KK
Modallogik und Tableaukalkül: Kapitel 6 aus KK
Temporallogik: Kapitel 7 aus KK
Dynamische Logik und Prozesslogik: Kapitel 8 aus KK
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.
(Wir erwarten von den SeminarteilnehmerInnen, 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.)
Exakte Algorithmen für das Erfüllbarkeitsproblem (evtl. auch zwei Themen; Literatur beispielsweise von O. Kullmann)
Einführung in Parameterisierte Komplexitätstheorie (z.B.: Flum/Grohe: Parameterized Complexity Theory, Springer, 2006; Kap 1-2)
Logische Bezüge zur Parameterisierten Komplexitätstheorie (z.B.: Flum/Grohe, Kap. 3; evtl. auch zwei Themen (mit Kap. 4))
Parameterisierte Algorithmen für MaxSAT
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 E-Mail 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 H 413 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üsen 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 Nichtbestehen 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 TeilnehmerInnen verteilt. Dabei ist 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.
- LaTeX-Kochbuch
- Trierer LaTeX-Stammtisch, siehe auch LaTeX in Trier
Der Vortrag selbst sollte auf 50 Minuten ausgelegt sein. Abweichungen hiervon wirken sich auf die Note aus.