Reduktionssysteme

Rechnen und Schließen in gleichungsdefinierten Strukturen

Specificaties
Paperback, 251 blz. | Duits
Springer Berlin Heidelberg | e druk, 1995
ISBN13: 9783540585596
Rubricering
Springer Berlin Heidelberg e druk, 1995 9783540585596
Onderdeel van serie Springer-Lehrbuch
Verwachte levertijd ongeveer 9 werkdagen

Samenvatting

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 grundlegender Eigenschaften.
Das Buch eignet sich für eine Vorlesung im Informatik-Hauptstudium. Durch Beispiele und Übungsaufgaben wird die anschauliche, übersichtliche Darstellung abgerundet.

Specificaties

ISBN13:9783540585596
Taal:Duits
Bindwijze:paperback
Aantal pagina's:251
Uitgever:Springer Berlin Heidelberg

Inhoudsopgave

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.

Rubrieken

    Personen

      Trefwoorden

        Reduktionssysteme