Inhalt

Das Rechnen und Beweisen mit Gleichungen ist eine der wichtigsten mathematischen Techniken. Termersetzungssysteme sind Mengen von gerichteten Gleichungen die als Reduktionsregeln benutzt werden und das automatische Rechnen und Beweisen mit Gleichungen ermöglichen. Außerdem können Termersetzungssysteme als eine einfache funktionale Programmiersprachen interpretiert werden. Termersetzungssysteme werden daher in Bereichen wie der Programmverifikation, der Spezifikation von Programmen und der deklarativen Programmierung eingesetzt.

In der Vorlesung werden Verfahren vorgestellt, um die folgenden Fragestellungen rechnergestützt zu untersuchen:

• Ist das Resultat einer Berechnung eindeutig (Konfluenz)?
• Hält eine Berechnung immer nach endlich vielen Schritten an (Terminierung)?
• In welchen Fällen sind Termersetzungssysteme ein Entscheidungsverfahren?

Termine

Folien

• Vorlesung 1 (19.04.)
• Vorlesung 2 (03.05.)
• Vorlesung 3 (14.06.)
• Vorlesung 4 (28.06.)
• Vorlesung 5 (05.07.)

Übungsblätter

• Übungsblatt 1 (19.04.)
• Übungsblatt 2 (03.05.)
• Übungsblatt 3 (14.06.)
• Übungsblatt 4 (28.06.)

Literatur

•       F. Baader/T. Nipkow: Term Rewriting and All That. Cambridge University Press, 1998
•       N. Dershowitz/D. Plaisted: Rewriting. Handbook of Automated Reasoning, Volume 1, Seiten 535-610. Elsevier, 2001
•       E. Ohlebusch: Advanced Topics in Term Rewriting. Springer-Verlag, 2002