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.3 Die Vervollst?ndigung nach Knuth-Bendix.- 2.4 Entscheidbarkeitsfragen.- 3 Termersetzungssysteme.- 3.1 Motivation.- 3.2 Spezifikation von Datentypen.- 3.3 Termersetzungssysteme.- 3.4 Matching und Unifikation.- 3.5 Konfluenz und Termination.- 3.6 Die Vervollst?ndigung nach Knuth-Bendix.- 3.7 Reduktionsordnungen.- 3.8 Modularit?t.- 4 Termersetzung modulo einer Kongruenz.- 4.1 Die Church-Rosser-Eigenschaft modulo A.- 4.2 A-Vervollst?ndigung f?r links-lineare Regeln.- 4.3 A-Vervollst?ndigung f?r beliebige Regeln.- 4.4 A-vertr?gliche Reduktionsordnungen.- 5 Ausblick.- Wegweiser zur Originalliteratur.Reduktions- und Vervollst?ndigungstechniken dienen zum Rechnen und Schlie?en in gleichungsdefinierten algebraischen Strukturen wie Abstrakten Datentypen. In dieser ersten systematischen Einf?hrung in das Gebiet der Reduktionssysteme werden die Grundlagen entwickelt und auf unterschiedliche Ersetzungssysteme angewandt. Themenschwerpunkte sind: 1. denotationale, operationale und rewrite-basierte Semantik, 2. effiziente und nachweisbar korrekte Vervollst?ndigungsalgorithmen, 3. Inferenzsysteme, die auf Beweistransformation und Beweisordnung basieren und 4. prinzipielle Entscheidbarkeit von grundlegenden Eigenschaften. Das Buch eignet sich f?r eine Vorlesung im Informatik-Hauptstudium. Durch Beispiele und ?bungsaufgaben wird die anschauliche und ?bersichtliche Darstellung abgerundet. F?r Studenten und Wissenschaftler auf dem Gebiet der Mathematischen Logik und formalen Sprachen, der Logik und Semantik von Programmiersprachen und der k?nstlichen Intelligenz.