Reduktionssysteme

0 Einleitung.- 0.1 Motivation.- 0.2 Termersetzungssysteme und abstrakte Datentypen.- 1 Abstrakte Reduktionssysteme.- 1.1 Definitionen und erste Ergebnisse.- 1.2 Konfluenz und die Church-Rosser-Eigenschaft.- 1.3 Konstruktion von Noetherschen Partialordnungen.- 1.4 Konstruktion von konvergenten Reduktionssystemen.- 2 Wortersetzungssysteme.- 2.1 Motivation.- 2.2 Termination und Konfluenz.- 2.2.1 Termination.- 2.2.2 Konfluenz.- 2.3 Die Vervollständigung nach Knuth-Bendix.- 2.3.1 Ein einfacher Algorithmus.- 2.3.2 Ein verbesserter Algorithmus.- 2.3.3 Das Verhalten des Vervollständigungsverfahrens.- 2.4 Entscheidbarkeitsfragen.- 2.4.1 Entscheidbare Probleme.- 2.4.2 Unentscheidbare Probleme.- 3 Termersetzungssysteme.- 3.1 Motivation.- 3.2 Spezifikation von Datentypen.- 3.2.1 Syntax und Semantik von Spezifikationen.- 3.2.2 Konstruktion von Modellen und der Satz von Birkhoff.- 3.3 Termersetzungssysteme.- 3.3.1 Regelsysteme und ihre Reduktionsrelation.- 3.3.2 Entscheidbarkeitsfragen.- 3.4 Matching und Unifikation.- 3.4.1 Matching.- 3.4.2 Unifikation.- 3.5 Konfluenz und Termination.- 3.5.1 Konfluenz.- 3.5.2 Einfache Terminationskriterien.- 3.6 Die Vervollständigung nach Knuth-Bendix.- 3.6.1 Ein einfacher Algorithmus.- 3.6.2 Das Inferenzsystem P.- 3.6.3 Ein effizienter Algorithmus.- 3.6.4 Normierung und Existenz von Regelsystemen zu (E, >).- 3.7 Reduktionsordnungen.- 3.7.1 Simplifikationsordnungen.- 3.7.2 Semantische Reduktionsordnungen.- 3.7.3 Syntaktische Reduktionsordnungen.- 3.8 Modularität.- 4 Termersetzung modulo einer Kongruenz.- 4.1 Die Church-Rosser-Eigenschaft modulo A.- 4.1.1 Motivation und einige Reduktionsrelationen.- 4.1.2 Termination und Konfluenzeigenschaften modulo A.- 4.2 A-Vervollständigung für links-lineare Regeln.- 4.2.1 Lokale Konfluenzkriterien für ? r.- 4.2.2 Das Inferenzsystem L.- 4.3 A-Vervollständigung für beliebige Regeln.- 4.3.1 Lokale Konffuenzkritereien für ? r.a.- 4.3.2 Das Inferenzsystem A.- 4.4 A-verträgliche Reduktionsordnungen.- 4.4.1 Semantische Reduktionsordnungen.- 4.4.2 Die assoziative Pfadordnung.- 5 Ausblick.- Wegweiser zur Originalliteratur.