Termersetzungssysteme

Prof. Tobias Nipkow

Achtung: Vorlesung fällt wegen Mangel an Studenten aus, wird aber im Sommersemester 2000 als Bestandteil von Logik angeboten.

Bereich: III, Vorlesung: 3 Std.

Zeit & Ort: Mi 12:15-13:00 in N1090, Do 8:30-10:00 in 2770

Beginn: 3.11.99

Inhalt: Das Rechnen mit Gleichungen ist eine der wichtigsten mathematischen Techniken. In der Informatik bauen zum Beispiel ganze Gebiete wie höhere Programmiersprachen und -umgebungen, Programmspezifikation und -verifikation, Theorembeweisen und Symbolische Algebra direkt auf Gleichungskalkülen auf. Termersetzungssysteme sind Mengen von gerichteten Gleichungen, die als Reduktionsregeln interpretiert werden. Ziel der Vorlesung ist es, sowohl die Grundlagen der Gleichungslogik als auch die wichtigsten Algorithmen zur Manipulation von Termen, Gleichungen und Ersetzungsregeln einzuführen.

1. Abstrakte Reduktionssysteme
2. Termersetzung
3. Gleichungsprobleme
   
4. Termination von Termersetzungssystemen
5. Konfluenz von Termersetzungssystemen
   
6. Kombinationsprobleme
7. E-Unifikation

Hörerkreis: Studierende der Informatik und Mathematik

Voraussetzungen: Vordiplom. Hilfreich aber nicht notwendig: Logik.

Empfehlenswert für: alle Studierenden, die sich für die logischen Grundlagen der Informatik und Mathematik interessieren. Daher besonders als Ergänzung zu den Vorlesungen Logik und Semantik zu empfehlen.

Die Vorlesung orientiert sich sehr stark an folgendem Buch:

Weitere Literatur:

• Übersichtsartikel:
  • N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuven (editor), Formal Models and Semantics, Handbook of Theoretical Computer Science, Vol. B, pages 243-320. Elsevier - The MIT Press, 1990.
  • J. W. Klop. Term Rewriting Systems. In S. Abramsky and D.M. Gabbay and T.S.E. Maibaum (editors), Handbook of Logic in Computer Science, Vol. 2, pages 2-116. Oxford University Press, 1992.
• Weitere Lehrbücher:
  • J. Avenhaus. Reduktionssysteme. Springer-Verlag, 1995.
• Rewriting Home Page

Sprechstunde: 2550, nach Vereinbarung.