Veranstaltungs-Nr.:   18.221

Titel:                             Reduktionssysteme

Veranstalter:                Matthias Jantzen

Zeit / Ort:                      Mi 12-14,   C-221

Lernziel:                      Kennenlernen von Reduktions- und anderen Ersetzungssystemen, deren Eigenschaften und Anwendungen in Deduktionssystemen, von automatischen Beweisern und in anderen Gebieten. Erlernen der Benutzung theoretisch fundierter Methoden, um damit die Ausdruckskraft dieser und neuer Konstruktionen in diesem Bereich schnell und sicher feststellen zu können.

Inhalt:                           Reduktionssysteme  tauchen in der Informatik an vielen wichtigen Stellen auf: Als Termersetzungssysteme in jenem Bereich der künstlichen Intelligenz, der  sich mit der Konstruktion und Programmierung von automatischen Beweisern beschäftig, als Ersetzungssysteme mit Hilfe von Polynomen im weiten Bereich der Computer-Algebra, bei Graphgrammatiken und auch als  Wortersetzungssysteme. DieGrundbegriffe zur Beschreibung und Klassifikation aller Ersetzungssysteme werden erläutert und an Beispielen verdeutlicht. Besprochen werden Systeme zur Transformation und Ersetzung von Zeichenketten, Termen oder Bäumen, Polynomen und speziell Vektoren. Verschiedene Möglichkeiten zum Beweis und  Prüfung der Termination werden untersucht.

Stell. im Studienplan:Hauptstudium,

                                      [SP:BV, SV, WV, SEM, eigenes Theorie-Profil C;
VG: Th2, Th3, P1, P6, P8, P10]

Voraussetzungen:     Grundstudium

Vorgehen:                   Vorlesung mit integrierter Übung

Literatur:                      G. Huet: Confluent reductions: abstract properties and applications to term rewriting systems, JCSS 27(1980) 797-821.

                                      G. Huet / D.Oppen: Equations and rewrite rules, in: Formal Language Theory: Perspectives and Open Problems, R. V. Book (Ed.), Academic Press (1980) 349-405.

                                      B. Buchberger / R. Loos, Algebraic Simplification, in: Computer Algebra, Buchberger, Collins und Loos (Ed.), Computing supplement 4, Springer-Verlag( 1982), 11-43.

                                      M. Jantzen, Thue congruences and complete string rewriting Systems, EATCS Monograph 14,

                                      J. Avenhaus & K. Madlener: Term Rewriting und Equational Reasoning (in: Formal Techn. in AI),

                                      J. Avenhaus: Reduktionssysteme, Springer-Verlag (1995),

                                      R. Bündgen: Termersetzungssysteme, Vieweg (1998),

                                      M. Jantzen: Basics of Termrewriting, (in: Handbook of Formal Languages, vol 3), Springer-Verlag (1997) sowie weitere Originalarbeiten.

Periodizität:                unregelmäßig

Für LehrerInnen nicht / für Nebenfächler(innen) geeignet.

Stichworte:                 Ableitung, Deduktion, Church-Rosser Eigenschaft, Konfluenz,
                                     Termination, Knuth-Bendix Vervollständigung,
                                     Termersetzung, Reduktionsordnungen,