Reduktionssysteme: Rechnen Und Schließen in Gleichungsdefinierten Strukturen

ISBN-13: 9783540585596 / Niemiecki / Miękka / 1995 / 261 str.

Ja1/4rgen Avenhaus

Opis

Reduktions- und Vervollstandigungstechniken dienen zum Rechnen und Schliessen in gleichungsdefinierten algebraischen Strukturen wie Abstrakten Datentypen. In dieser ersten systematischen Einfuhrung 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 Vervollstandigungsalgorithmen, 3. Inferenzsysteme, die auf Beweistransformation und Beweisordnung basieren, und 4. prinzipielle Entscheidbarkeit grundlegender Eigenschaften.
Das Buch eignet sich fur eine Vorlesung im Informatik-Hauptstudium. Durch Beispiele und Ubungsaufgaben wird die anschauliche, ubersichtliche Darstellung abgerundet."

Spis treści

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.