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
Two lectures hours each week are taught in English.

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:

Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press.

Weitere Literatur:

Sprechstunde: 2550, nach Vereinbarung.


Tobias Nipkow, 3.11.99