Home | english  | Impressum | Sitemap | KIT

Termersetzungssysteme

Termersetzungssysteme
Typ: Vorlesung
Lehrstuhl: Fakultät für Informatik
Semester: Sommersemester 2010
Ort:

Seminarraum 131 (50.34)

Zeit:

Mo 09:45-11:15 (14-tägig)

Beginn: 19.04.2010
Dozent: Stephan Falke
Carsten Sinz
SWS: 1
LVNr.: 24663
rewriting

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

19.04. 03.05. 17.05. 31.05. 14.06. 28.06. 05.07.

Folien

Übungsblätter

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