Vorlesung: Termersetzungssysteme

HDoz. Dr. A. Weiermann

Zeit:

Montag, Dienstag 13-15 Uhr c.t.

Ort:

SR8

Zuordnung:

Studierende im Hauptstudium mit Nebenfach Logik oder Informatik

Inhalt:

Die Theorie der Termersetzungssyteme bildet eine Grundlage für das maschinelle Beweisen und das Studium abstrakter Datentypen. Wir beginnen mit Standardthemen der termersetzung und behandeln abstrakte reduktionssysteme, Konfluenz, Temination und die Knuth-Bendix-Vervollständigung. Als algebraische Anwendung stellen wir den buchberger-Algorithmus vor. Zudem behandeln wir auch Querverbindungen von Logik und Termersetzung. Hier behandeln wir auf Termersetzung beruhende Charakterisierungen verschiedener Teilklassen rekursiver Funktionen.

Vorkenntnisse:

Prädikatenlogik, Rekursionstheorie

Literatur:

J. Avenhaus:

Reduktionssysteme, Springer Verlag (1995)

F. Baader, T. Nipkow:

Term rewriting and All That, Cambridge University Press (1998)

A. Weiermann:

Termination proofs for term rewriting systems with lexicographic path orderings imply multiply recursive derivation lengths, Theoretical Computer Science 139 (1995), 355-362

Leistungsnachweis:

Erfolgreiche Bearbeitung von Übungsaufgaben