Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

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