Bernhard Gramlich | AG Theoretische Informatik und Logik | Fakultät für Informatik | TU Wien
Lehrveranstaltungsleiter: Bernhard Gramlich, gramlich@logic.at
Die VU "Termersetzungssysteme" ist eine Wahllehrveranstaltung in den Informatik-Masterstudiengängen Computational Intelligence (Wahlfachkatalog "Theoretische Informatik und Logik") und Software Engineering & Internet Computing (Wahlfachkatalog "Theoretische Informatik") sowie Prüfungsfach im Rahmen des European Masters Program in Computational Logic (Advanced Modules / Inference in Classical and Non-Classical Logic).
Wenn Sie die Vorlesung besuchen wollen, melden Sie sich bitte über TUWIS++ dafür an.
Die Lehrveranstaltung wird - je nach Bedarf - auf englisch abgehalten werden.
Ergebnisse der Prüfung vom 21.01.10 + Gesamtergebnisse (WS 2009/2010):
Montag, 05.10.09, 13:15-15:00, Zemanek Seminarraum
Regelmäßiger Termin
Donnerstag, 11:00-13:00, Seminarraum 185/2 / Laborraum 185/2 (HA0302), Favoritenstraße 9-11, Stiege I, 3. Obergeschoß, gelber BereichBeginn (Einführung und Überblick)
Donnerstag, 08.10.09, 11:00-13:00, Seminarraum 185/2 / Laborraum 185/2 (HA0302), Favoritenstraße 9-11, Stiege I, 3. Obergeschoß, gelber Bereich
Termgleichungs- und Termersetzungssysteme sind von grundlegender Bedeutung in vielen Bereichen der Informatik (als auch der Mathematik). Sie spielen beispielsweise eine wichtige Rolle als logisches Beschreibungsmittel für formale (algebraische) Spezifikationen und Korrektheitseigenschaften von Programmen als auch als Beweismethodik für derartige Verifikationsaufgaben. Termersetzungssysteme stellen einen sehr einfachen und zugleich sehr mächtigen Formalismus zum Modellieren indeterministischer symbolischer Berechnungen dar. In der Vorlesung werden grundlegende Kenntnisse zu Theorie, Methoden und Anwendungen von Termersetzungssystemen vermittelt. Behandelt werden u.a. folgende Themen:
Als Voraussetzung hilfreich (aber nicht unbedingt notwendig) sind Grundkenntnisse aus den Vorlesungen Theoretische Informatik und Logik und Unifikationstheorie.
Die Lehrveranstaltung bietet gleichzeitig gute Voraussetzungen für und einen Einstieg in diverse Vertiefungsmölichkeiten im Gebiet der Computational (Equational) Logic. Dies betrifft sowohl Spezial-Lehrveranstaltungen wie etwa Computational Equational Logic als auch eigenständige Arbeiten im Rahmen von Praktika, Seminaren, Diplom-/Magisterarbeiten - speziell auch im Kontext eines in unserer Arbeitsgruppe entwickelten modularen Software-Tools für automatische Terminerungsbeweise von Termersetzungssystemen (VMTL - Vienna Modular Termination Laboratory), bis hin zu möglichen Dissertationsthemen im Rahmen eines Doktoratsstudiums.
Kopien der Vorlesungsfolien werden zur Verfügung gestellt. Inhaltlich orientiert sich die Vorlesung vor allem am Lehrbuch
sowie an diversen Übersichtsartikeln. Für weitere Bücher zum Thema siehe hier. Für umfassende Informationen über Termersetzungssysteme, insbesondere über weiterführende Literatur und verfügbare Implementierungen / Software-Tools, sei auf die Rewriting Home Page verwiesen.
Der Übungsteil der Lehrveranstaltung ist in die Vorlesung integriert und wird in Form von zu bearbeitenden Hausaufgaben stattfinden. Am Ende der Vorlesung gibt es eine schriftliche Prüfung. In die Gesamtbewertung fließen neben dem Prüfungsergebnis auch der Übungsanteil sowie die Mitarbeit bei der Lehrveranstaltung mit ein.
Vorlesungsprüfung: Donnerstag 21.1.2010, 11:00-13:00,
Seminarraum 185/2
Anmeldung über TUWIS++!
Bernhard Gramlich