Bernhard Gramlich | AG Theoretische Informatik und Logik | Fakultät für Informatik | TU Wien


185.224 (English version)
Termersetzungssysteme / Term Rewriting Systems, VU 3.0/2.0, WS 2012/2013


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 TISS dafür an.

Die Lehrveranstaltung wird - je nach Bedarf - auf englisch abgehalten werden.


Aktuelles

Die Anmeldung zur Lehrveranstaltung erfolgt über TISS.

Beginn der (leicht geblockten) Lehrveranstaltung:
Dienstag 06.11.2012, 16:00-18:00, Seminarraum Gödel, Favoritenstr. 9, EG, Innenhof

Termine

Beginn der (leicht geblockten) Lehrveranstaltung:
Dienstag 06.11.2012, 16:00-18:00, Seminarraum Gödel, Favoritenstr. 9, EG, Innenhof
Regelmäßiger Termin (vorläufig):
Dienstag, 16:00-18:00, Seminarraum Gödel, Favoritenstr. 9, EG, Innenhof

Inhalt der Lehrveranstaltung

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.


Vertiefungsmöglichkeiten

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.


Vorlesungsunterlagen

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.


Beurteilung

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.


Prüfung


Bernhard Gramlich | AG Theoretische Informatik und Logik | Fakultät für Informatik | TU Wien
Last modified: Sun Nov 4 16:59:25 CET 2012
Valid HTML 4.01! Viewable With Any Browser Bernhard Gramlich